diff options
Diffstat (limited to 'abc70930/src/sat/msat/msatOrderH.c')
| -rw-r--r-- | abc70930/src/sat/msat/msatOrderH.c | 405 |
1 files changed, 0 insertions, 405 deletions
diff --git a/abc70930/src/sat/msat/msatOrderH.c b/abc70930/src/sat/msat/msatOrderH.c deleted file mode 100644 index 956e7fc6..00000000 --- a/abc70930/src/sat/msat/msatOrderH.c +++ /dev/null @@ -1,405 +0,0 @@ -/**CFile**************************************************************** - - FileName [msatOrder.c] - - PackageName [A C version of SAT solver MINISAT, originally developed - in C++ by Niklas Een and Niklas Sorensson, Chalmers University of - Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.] - - Synopsis [The manager of variable assignment.] - - Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - January 1, 2004.] - - Revision [$Id: msatOrder.c,v 1.0 2005/05/30 1:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "msatInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// the variable package data structure -struct Msat_Order_t_ -{ - Msat_Solver_t * pSat; // the SAT solver - Msat_IntVec_t * vIndex; // the heap - Msat_IntVec_t * vHeap; // the mapping of var num into its heap num -}; - -//The solver can communicate to the variable order the following parts: -//- the array of current assignments (pSat->pAssigns) -//- the array of variable activities (pSat->pdActivity) -//- the array of variables currently in the cone (pSat->vConeVars) -//- the array of arrays of variables adjucent to each(pSat->vAdjacents) - -#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) - -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 ); - -extern int timeSelect; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Msat_Order_t * Msat_OrderAlloc( Msat_Solver_t * pSat ) -{ - Msat_Order_t * p; - p = 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; -} - -/**Function************************************************************* - - Synopsis [Sets the bound of the ordering structure.] - - Description [Should be called whenever the SAT solver is resized.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderSetBounds( Msat_Order_t * p, int nVarsMax ) -{ - Msat_IntVecGrow( p->vIndex, nVarsMax ); - Msat_IntVecGrow( p->vHeap, nVarsMax + 1 ); - p->vIndex->nSize = nVarsMax; - p->vHeap->nSize = 0; -} - -/**Function************************************************************* - - Synopsis [Cleans the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ) -{ - 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; -} - -/**Function************************************************************* - - Synopsis [Checks that the J-boundary is okay.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderCheck( Msat_Order_t * p ) -{ - return Msat_HeapCheck_rec( p, 1 ); -} - -/**Function************************************************************* - - Synopsis [Frees the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderFree( Msat_Order_t * p ) -{ - Msat_IntVecFree( p->vHeap ); - Msat_IntVecFree( p->vIndex ); - free( p ); -} - - - -/**Function************************************************************* - - Synopsis [Selects the next variable to assign.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderVarSelect( Msat_Order_t * p ) -{ - // Activity based decision: -// while (!heap.empty()){ -// Var next = heap.getmin(); -// if (toLbool(assigns[next]) == l_Undef) -// return next; -// } -// return var_Undef; - - int Var; - int clk = clock(); - - while ( !HEMPTY(p) ) - { - Var = Msat_HeapGetTop(p); - if ( (p)->pSat->pAssigns[Var] == MSAT_VAR_UNASSIGNED ) - { -//assert( Msat_OrderCheck(p) ); -timeSelect += clock() - clk; - return Var; - } - } - return MSAT_ORDER_UNKNOWN; -} - -/**Function************************************************************* - - Synopsis [Updates J-boundary when the variable is assigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ) -{ -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable is unassigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) -{ -// if (!heap.inHeap(x)) -// heap.insert(x); - - int clk = clock(); - if ( !HINHEAP(p,Var) ) - Msat_HeapInsert( p, Var ); -timeSelect += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable changed weight.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderUpdate( Msat_Order_t * p, int Var ) -{ -// if (heap.inHeap(x)) -// heap.increase(x); - - int clk = clock(); - if ( HINHEAP(p,Var) ) - Msat_HeapIncrease( p, Var ); -timeSelect += clock() - clk; -} - - - - -/**Function************************************************************* - - Synopsis [Checks the heap property recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_HeapCheck_rec( Msat_Order_t * p, int i ) -{ - 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) ); -} - -/**Function************************************************************* - - Synopsis [Retrieves the minimum element.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_HeapGetTop( Msat_Order_t * p ) -{ - 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; -} - -/**Function************************************************************* - - Synopsis [Inserts the new element.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapInsert( Msat_Order_t * p, int n ) -{ - assert( HOKAY(p, n) ); - p->vIndex->pArray[n] = HSIZE(p); - Msat_IntVecPush( p->vHeap, n ); - Msat_HeapPercolateUp( p, p->vIndex->pArray[n] ); -} - -/**Function************************************************************* - - Synopsis [Inserts the new element.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapIncrease( Msat_Order_t * p, int n ) -{ - Msat_HeapPercolateUp( p, p->vIndex->pArray[n] ); -} - -/**Function************************************************************* - - Synopsis [Moves the entry up.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapPercolateUp( Msat_Order_t * p, int i ) -{ - 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; -} - -/**Function************************************************************* - - Synopsis [Moves the entry down.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_HeapPercolateDown( Msat_Order_t * p, int i ) -{ - 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; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |