msatOrderH.c File Reference

#include "msatInt.h"

Include dependency graph for msatOrderH.c:

Go to the source code of this file.

Classes
struct	Msat_Order_t_
	DECLARATIONS ///. More...

Macros
#define	HLEFT(i)
#define	HRIGHT(i)
#define	HPARENT(i)
#define	HCOMPARE(p, i, j)
#define	HHEAP(p, i)
#define	HSIZE(p)
#define	HOKAY(p, i)
#define	HINHEAP(p, i)
#define	HEMPTY(p)

Functions
Msat_Order_t *	Msat_OrderAlloc (Msat_Solver_t *pSat)
	FUNCTION DEFINITIONS ///.
void	Msat_OrderSetBounds (Msat_Order_t *p, int nVarsMax)
void	Msat_OrderClean (Msat_Order_t *p, Msat_IntVec_t *vCone)
int	Msat_OrderCheck (Msat_Order_t *p)
void	Msat_OrderFree (Msat_Order_t *p)
int	Msat_OrderVarSelect (Msat_Order_t *p)
void	Msat_OrderVarAssigned (Msat_Order_t *p, int Var)
void	Msat_OrderVarUnassigned (Msat_Order_t *p, int Var)
void	Msat_OrderUpdate (Msat_Order_t *p, int Var)

Variables
abctime	timeSelect
	DECLARATIONS ///.

Macro Definition Documentation

HCOMPARE

#define HCOMPARE	(		p,
			i,
			j )

Value:

((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j])

Definition at line 47 of file msatOrderH.c.

HEMPTY

#define HEMPTY

(

p

)

Value:

(HSIZE(p) == 1)

Definition at line 52 of file msatOrderH.c.

HHEAP

#define HHEAP	(		p,
			i )

Value:

((p)->vHeap->pArray[i])

Definition at line 48 of file msatOrderH.c.

HINHEAP

#define HINHEAP	(		p,
			i )

Value:

(HOKAY(p, i) && (p)->vIndex->pArray[i] != 0)

Definition at line 51 of file msatOrderH.c.

HLEFT

#define HLEFT

(

i

)

Value:

((i)<<1)

Definition at line 44 of file msatOrderH.c.

HOKAY

#define HOKAY	(		p,
			i )

Value:

((i) >= 0 && (i) < (p)->vIndex->nSize)

Definition at line 50 of file msatOrderH.c.

HPARENT

#define HPARENT

(

i

)

Value:

((i)>>1)

Definition at line 46 of file msatOrderH.c.

HRIGHT

#define HRIGHT

(

i

)

Value:

(((i)<<1)+1)

Definition at line 45 of file msatOrderH.c.

HSIZE

#define HSIZE

(

p

)

Value:

((p)->vHeap->nSize)

Definition at line 49 of file msatOrderH.c.

Function Documentation

Msat_OrderAlloc()

Msat_Order_t * Msat_OrderAlloc

(

Msat_Solver_t *

pSat

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Allocates the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file msatOrderH.c.

{
    Msat_Order_t * p;
    p = ABC_ALLOC( Msat_Order_t, 1 );
    memset( p, 0, sizeof(Msat_Order_t) );
    p->pSat   = pSat;
    p->vIndex = Msat_IntVecAlloc( 0 );
    p->vHeap  = Msat_IntVecAlloc( 0 );
    Msat_OrderSetBounds( p, pSat->nVarsAlloc );
    return p;
}

Msat_OrderCheck()

int Msat_OrderCheck

(

Msat_Order_t *

p

)

Function*************************************************************

Synopsis [Checks that the J-boundary is okay.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file msatOrderH.c.

{
    return Msat_HeapCheck_rec( p, 1 );
}

Msat_OrderClean()

void Msat_OrderClean	(	Msat_Order_t *	p,
		Msat_IntVec_t *	vCone )

Function*************************************************************

Synopsis [Cleans the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file msatOrderH.c.

{
    int i;
    for ( i = 0; i < p->vIndex->nSize; i++ )
        p->vIndex->pArray[i] = 0;
    for ( i = 0; i < vCone->nSize; i++ )
    {
        assert( i+1 < p->vHeap->nCap );
        p->vHeap->pArray[i+1] = vCone->pArray[i];
 
        assert( vCone->pArray[i] < p->vIndex->nSize );
        p->vIndex->pArray[vCone->pArray[i]] = i+1;
    }
    p->vHeap->nSize = vCone->nSize + 1;
}

Msat_OrderFree()

void Msat_OrderFree

(

Msat_Order_t *

p

)

Function*************************************************************

Synopsis [Frees the ordering structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file msatOrderH.c.

{
    Msat_IntVecFree( p->vHeap );
    Msat_IntVecFree( p->vIndex );
    ABC_FREE( p );
}

Msat_OrderSetBounds()

void Msat_OrderSetBounds	(	Msat_Order_t *	p,
		int	nVarsMax )

Function*************************************************************

Synopsis [Sets the bound of the ordering structure.]

Description [Should be called whenever the SAT solver is resized.]

SideEffects []

SeeAlso []

Definition at line 101 of file msatOrderH.c.

{
    Msat_IntVecGrow( p->vIndex, nVarsMax );
    Msat_IntVecGrow( p->vHeap, nVarsMax + 1 );
    p->vIndex->nSize = nVarsMax;
    p->vHeap->nSize = 0;
}

Here is the caller graph for this function:

Msat_OrderUpdate()

void Msat_OrderUpdate	(	Msat_Order_t *	p,
		int	Var )

Function*************************************************************

Synopsis [Updates the order after a variable changed weight.]

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file msatOrderH.c.

{
//    if (heap.inHeap(x))
//        heap.increase(x);
 
    abctime clk = Abc_Clock();
    if ( HINHEAP(p,Var) )
        Msat_HeapIncrease( p, Var );
timeSelect += Abc_Clock() - clk;
}

Msat_OrderVarAssigned()

void Msat_OrderVarAssigned	(	Msat_Order_t *	p,
		int	Var )

Function*************************************************************

Synopsis [Updates J-boundary when the variable is assigned.]

Description []

SideEffects []

SeeAlso []

Definition at line 220 of file msatOrderH.c.

{
}

Msat_OrderVarSelect()

int Msat_OrderVarSelect

(

Msat_Order_t *

p

)

Function*************************************************************

Synopsis [Selects the next variable to assign.]

Description []

SideEffects []

SeeAlso []

Definition at line 183 of file msatOrderH.c.

{
    // Activity based decision:
//    while (!heap.empty()){
//        Var next = heap.getmin();
//        if (toLbool(assigns[next]) == l_Undef)
//            return next;
//    }
//    return var_Undef;
 
    int Var;
    abctime clk = Abc_Clock();
 
    while ( !HEMPTY(p) )
    {
        Var = Msat_HeapGetTop(p);
        if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED )
        {
//assert( Msat_OrderCheck(p) );
timeSelect += Abc_Clock() - clk;
            return Var;
        }
    }
    return MSAT_ORDER_UNKNOWN;
}

Msat_OrderVarUnassigned()

void Msat_OrderVarUnassigned	(	Msat_Order_t *	p,
		int	Var )

Function*************************************************************

Synopsis [Updates the order after a variable is unassigned.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file msatOrderH.c.

{
//    if (!heap.inHeap(x))
//        heap.insert(x);
 
    abctime clk = Abc_Clock();
    if ( !HINHEAP(p,Var) )
        Msat_HeapInsert( p, Var );
timeSelect += Abc_Clock() - clk;
}

Variable Documentation

timeSelect

abctime timeSelect

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [fraigMan.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Implementation of the FRAIG manager.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id

fraigMan.c,v 1.11 2005/07/08 01:01:31 alanmi Exp

]

Definition at line 28 of file fraigMan.c.