msatOrderH.c File Reference

#include "msatInt.h"

Go to the source code of this file.

Data Structures
struct	Msat_Order_t_
	DECLARATIONS ///. More...

Macros
#define	HLEFT(i)   ((i)<<1)
#define	HRIGHT(i)   (((i)<<1)+1)
#define	HPARENT(i)   ((i)>>1)
#define	HCOMPARE(p, i, j)   ((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j])
#define	HHEAP(p, i)   ((p)->vHeap->pArray[i])
#define	HSIZE(p)   ((p)->vHeap->nSize)
#define	HOKAY(p, i)   ((i) >= 0 && (i) < (p)->vIndex->nSize)
#define	HINHEAP(p, i)   (HOKAY(p, i) && (p)->vIndex->pArray[i] != 0)
#define	HEMPTY(p)   (HSIZE(p) == 1)

Functions
static int	Msat_HeapCheck_rec (Msat_Order_t *p, int i)
static int	Msat_HeapGetTop (Msat_Order_t *p)
static void	Msat_HeapInsert (Msat_Order_t *p, int n)
static void	Msat_HeapIncrease (Msat_Order_t *p, int n)
static void	Msat_HeapPercolateUp (Msat_Order_t *p, int i)
static void	Msat_HeapPercolateDown (Msat_Order_t *p, int i)
Msat_Order_t *	Msat_OrderAlloc (Msat_Solver_t *pSat)
	FUNCTION DEFINITIONS ///. More...
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 ///. More...

Macro Definition Documentation

#define HCOMPARE	(		p,
			i,
			j
	)		((p)->pSat->pdActivity[i] > (p)->pSat->pdActivity[j])

Definition at line 47 of file msatOrderH.c.

#define HEMPTY

(

p

)

(HSIZE(p) == 1)

Definition at line 52 of file msatOrderH.c.

#define HHEAP	(		p,
			i
	)		((p)->vHeap->pArray[i])

Definition at line 48 of file msatOrderH.c.

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

Definition at line 51 of file msatOrderH.c.

#define HLEFT

(

i

)

((i)<<1)

Definition at line 44 of file msatOrderH.c.

#define HOKAY	(		p,
			i
	)		((i) >= 0 && (i) < (p)->vIndex->nSize)

Definition at line 50 of file msatOrderH.c.

#define HPARENT

(

i

)

((i)>>1)

Definition at line 46 of file msatOrderH.c.

#define HRIGHT

(

i

)

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

Definition at line 45 of file msatOrderH.c.

#define HSIZE

(

p

)

((p)->vHeap->nSize)

Definition at line 49 of file msatOrderH.c.

Function Documentation

int Msat_HeapCheck_rec ( Msat_Order_t *  p, int  i  )

static

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

Synopsis [Checks the heap property recursively.]

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file msatOrderH.c.

{
    return i >= HSIZE(p) ||
        (
            ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&

            Msat_HeapCheck_rec( p, HLEFT(i) ) && 
            
            Msat_HeapCheck_rec( p, HRIGHT(i) )
        );
}

int Msat_HeapGetTop ( Msat_Order_t *  p )

static

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

Synopsis [Retrieves the minimum element.]

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file msatOrderH.c.

{
    int Result, NewTop;
    Result                    = HHEAP(p, 1);
    NewTop                    = Msat_IntVecPop( p->vHeap );
    p->vHeap->pArray[1]       = NewTop;
    p->vIndex->pArray[NewTop] = 1;
    p->vIndex->pArray[Result] = 0;
    if ( p->vHeap->nSize > 1 )
        Msat_HeapPercolateDown( p, 1 );
    return Result;
}

void Msat_HeapIncrease ( Msat_Order_t *  p, int  n  )

static

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

Synopsis [Inserts the new element.]

Description []

SideEffects []

SeeAlso []

Definition at line 348 of file msatOrderH.c.

{
    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
}

void Msat_HeapInsert ( Msat_Order_t *  p, int  n  )

static

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

Synopsis [Inserts the new element.]

Description []

SideEffects []

SeeAlso []

Definition at line 329 of file msatOrderH.c.

{
    assert( HOKAY(p, n) );
    p->vIndex->pArray[n] = HSIZE(p);
    Msat_IntVecPush( p->vHeap, n );
    Msat_HeapPercolateUp( p, p->vIndex->pArray[n] );
}

void Msat_HeapPercolateDown ( Msat_Order_t *  p, int  i  )

static

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

Synopsis [Moves the entry down.]

Description []

SideEffects []

SeeAlso []

Definition at line 388 of file msatOrderH.c.

{
    int x = HHEAP(p, i);
    int Child;
    while ( HLEFT(i) < HSIZE(p) )
    {
        if ( HRIGHT(i) < HSIZE(p) && HCOMPARE(p, HHEAP(p, HRIGHT(i)), HHEAP(p, HLEFT(i))) )
            Child = HRIGHT(i);
        else
            Child = HLEFT(i);
        if ( !HCOMPARE(p, HHEAP(p, Child), x) )
            break;
        p->vHeap->pArray[i]            = HHEAP(p, Child);
        p->vIndex->pArray[HHEAP(p, i)] = i;
        i                              = Child;
    }
    p->vHeap->pArray[i]  = x;
    p->vIndex->pArray[x] = i;
}

void Msat_HeapPercolateUp ( Msat_Order_t *  p, int  i  )

static

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

Synopsis [Moves the entry up.]

Description []

SideEffects []

SeeAlso []

Definition at line 364 of file msatOrderH.c.

{
    int x = HHEAP(p, i);
    while ( HPARENT(i) != 0 && HCOMPARE(p, x, HHEAP(p, HPARENT(i))) )
    {
        p->vHeap->pArray[i]            = HHEAP(p, HPARENT(i));
        p->vIndex->pArray[HHEAP(p, i)] = i;
        i                              = HPARENT(i);
    }
    p->vHeap->pArray[i]  = x;
    p->vIndex->pArray[x] = i;
}

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;
}

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 );
}

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;
}

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 );
}

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;
}

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;
}

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.

{
}

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;
}

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

abctime timeSelect

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.