diff options
Diffstat (limited to 'src/sat/msat/msatOrderJ.c')
| -rw-r--r-- | src/sat/msat/msatOrderJ.c | 472 |
1 files changed, 0 insertions, 472 deletions
diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c deleted file mode 100644 index 4db7ff7b..00000000 --- a/src/sat/msat/msatOrderJ.c +++ /dev/null @@ -1,472 +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" - -/* -The J-boundary (justification boundary) is defined as a set of unassigned -variables belonging to the cone of interest, such that for each of them, -there exist an adjacent assigned variable in the cone of interest. -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Msat_OrderVar_t_ Msat_OrderVar_t; -typedef struct Msat_OrderRing_t_ Msat_OrderRing_t; - -// the variable data structure -struct Msat_OrderVar_t_ -{ - Msat_OrderVar_t * pNext; - Msat_OrderVar_t * pPrev; - int Num; -}; - -// the ring of variables data structure (J-boundary) -struct Msat_OrderRing_t_ -{ - Msat_OrderVar_t * pRoot; - int nItems; -}; - -// the variable package data structure -struct Msat_Order_t_ -{ - Msat_Solver_t * pSat; // the SAT solver - Msat_OrderVar_t * pVars; // the storage for variables - int nVarsAlloc; // the number of variables allocated - Msat_OrderRing_t rVars; // the J-boundary as a ring of variables -}; - -//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 Msat_OrderVarIsInBoundary( p, i ) ((p)->pVars[i].pNext) -#define Msat_OrderVarIsAssigned( p, i ) ((p)->pSat->pAssigns[i] != MSAT_VAR_UNASSIGNED) -#define Msat_OrderVarIsUsedInCone( p, i ) ((p)->pSat->vVarsUsed->pArray[i]) - -// iterator through the entries in J-boundary -#define Msat_OrderRingForEachEntry( pRing, pVar, pNext ) \ - for ( pVar = pRing, \ - pNext = pVar? pVar->pNext : NULL; \ - pVar; \ - pVar = (pNext != pRing)? pNext : NULL, \ - pNext = pVar? pVar->pNext : NULL ) - -static void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); -static void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ); - -extern int timeSelect; -extern int timeAssign; - -//////////////////////////////////////////////////////////////////////// -/// 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; - 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 ) -{ - int i; - // add variables if they are missing - if ( p->nVarsAlloc < nVarsMax ) - { - p->pVars = REALLOC( Msat_OrderVar_t, p->pVars, nVarsMax ); - for ( i = p->nVarsAlloc; i < nVarsMax; i++ ) - { - p->pVars[i].pNext = p->pVars[i].pPrev = NULL; - p->pVars[i].Num = i; - } - p->nVarsAlloc = nVarsMax; - } -} - -/**Function************************************************************* - - Synopsis [Cleans the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderClean( Msat_Order_t * p, Msat_IntVec_t * vCone ) -{ - Msat_OrderVar_t * pVar, * pNext; - // quickly undo the ring - Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) - pVar->pNext = pVar->pPrev = NULL; - p->rVars.pRoot = NULL; - p->rVars.nItems = 0; -} - -/**Function************************************************************* - - Synopsis [Checks that the J-boundary is okay.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderCheck( Msat_Order_t * p ) -{ - Msat_OrderVar_t * pVar, * pNext; - Msat_IntVec_t * vRound; - int * pRound, nRound; - int * pVars, nVars, i, k; - int Counter = 0; - - // go through all the variables in the boundary - Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) - { - assert( !Msat_OrderVarIsAssigned(p, pVar->Num) ); - // go though all the variables in the neighborhood - // and check that it is true that there is least one assigned - vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVar->Num ); - nRound = Msat_IntVecReadSize( vRound ); - pRound = Msat_IntVecReadArray( vRound ); - for ( i = 0; i < nRound; i++ ) - { - if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) ) - continue; - if ( Msat_OrderVarIsAssigned(p, pRound[i]) ) - break; - } -// assert( i != nRound ); -// if ( i == nRound ) -// return 0; - if ( i == nRound ) - Counter++; - } - if ( Counter > 0 ) - printf( "%d(%d) ", Counter, p->rVars.nItems ); - - // we may also check other unassigned variables in the cone - // to make sure that if they are not in J-boundary, - // then they do not have an assigned neighbor - nVars = Msat_IntVecReadSize( p->pSat->vConeVars ); - pVars = Msat_IntVecReadArray( p->pSat->vConeVars ); - for ( i = 0; i < nVars; i++ ) - { - assert( Msat_OrderVarIsUsedInCone(p, pVars[i]) ); - // skip assigned vars, vars in the boundary, and vars not used in the cone - if ( Msat_OrderVarIsAssigned(p, pVars[i]) || - Msat_OrderVarIsInBoundary(p, pVars[i]) ) - continue; - // make sure, it does not have assigned neighbors - vRound = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( p->pSat->vAdjacents, pVars[i] ); - nRound = Msat_IntVecReadSize( vRound ); - pRound = Msat_IntVecReadArray( vRound ); - for ( k = 0; k < nRound; k++ ) - { - if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) ) - continue; - if ( Msat_OrderVarIsAssigned(p, pRound[k]) ) - break; - } -// assert( k == nRound ); -// if ( k != nRound ) -// return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Frees the ordering structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderFree( Msat_Order_t * p ) -{ - free( p->pVars ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Selects the next variable to assign.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Msat_OrderVarSelect( Msat_Order_t * p ) -{ - Msat_OrderVar_t * pVar, * pNext, * pVarBest; - double * pdActs = p->pSat->pdActivity; - double dfActBest; -// int clk = clock(); - - pVarBest = NULL; - dfActBest = -1.0; - Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) - { - if ( dfActBest < pdActs[pVar->Num] ) - { - dfActBest = pdActs[pVar->Num]; - pVarBest = pVar; - } - } -//timeSelect += clock() - clk; -//timeAssign += clock() - clk; - -//if ( pVarBest && pVarBest->Num % 1000 == 0 ) -//printf( "%d ", p->rVars.nItems ); - -// Msat_OrderCheck( p ); - if ( pVarBest ) - { - assert( Msat_OrderVarIsUsedInCone(p, pVarBest->Num) ); - return pVarBest->Num; - } - 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 ) -{ - Msat_IntVec_t * vRound; - int i;//, clk = clock(); - - // make sure the variable is in the boundary - assert( Var < p->nVarsAlloc ); - // if it is not in the boundary (initial decision, random decision), do not remove - if ( Msat_OrderVarIsInBoundary( p, Var ) ) - Msat_OrderRingRemove( &p->rVars, &p->pVars[Var] ); - // add to the boundary those neighbors that are (1) unassigned, (2) not in boundary - // because for them we know that there is a variable (Var) which is assigned - vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; - for ( i = 0; i < vRound->nSize; i++ ) - { - if ( !Msat_OrderVarIsUsedInCone(p, vRound->pArray[i]) ) - continue; - if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) - continue; - if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) ) - continue; - Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] ); - } -//timeSelect += clock() - clk; -// Msat_OrderCheck( p ); -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable is unassigned.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) -{ - Msat_IntVec_t * vRound, * vRound2; - int i, k;//, clk = clock(); - - // make sure the variable is not in the boundary - assert( Var < p->nVarsAlloc ); - assert( !Msat_OrderVarIsInBoundary( p, Var ) ); - // go through its neigbors - if one of them is assigned add this var - // add to the boundary those neighbors that are not there already - // this will also get rid of variable outside of the current cone - // because they are unassigned in Msat_SolverPrepare() - vRound = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[Var]; - for ( i = 0; i < vRound->nSize; i++ ) - if ( Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ) - break; - if ( i != vRound->nSize ) - Msat_OrderRingAddLast( &p->rVars, &p->pVars[Var] ); - - // unassigning a variable may lead to its adjacents dropping from the boundary - for ( i = 0; i < vRound->nSize; i++ ) - if ( Msat_OrderVarIsInBoundary(p, vRound->pArray[i]) ) - { // the neighbor is in the J-boundary (and unassigned) - assert( !Msat_OrderVarIsAssigned(p, vRound->pArray[i]) ); - vRound2 = (Msat_IntVec_t *)p->pSat->vAdjacents->pArray[vRound->pArray[i]]; - // go through its neighbors and determine if there is at least one assigned - for ( k = 0; k < vRound2->nSize; k++ ) - if ( Msat_OrderVarIsAssigned(p, vRound2->pArray[k]) ) - break; - if ( k == vRound2->nSize ) // there is no assigned vars, delete this one - Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] ); - } -//timeSelect += clock() - clk; -// Msat_OrderCheck( p ); -} - -/**Function************************************************************* - - Synopsis [Updates the order after a variable changed weight.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderUpdate( Msat_Order_t * p, int Var ) -{ -} - - -/**Function************************************************************* - - Synopsis [Adds node to the end of the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderRingAddLast( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ) -{ -//printf( "adding %d\n", pVar->Num ); - // check that the node is not in a ring - assert( pVar->pPrev == NULL ); - assert( pVar->pNext == NULL ); - // if the ring is empty, make the node point to itself - pRing->nItems++; - if ( pRing->pRoot == NULL ) - { - pRing->pRoot = pVar; - pVar->pPrev = pVar; - pVar->pNext = pVar; - return; - } - // if the ring is not empty, add it as the last entry - pVar->pPrev = pRing->pRoot->pPrev; - pVar->pNext = pRing->pRoot; - pVar->pPrev->pNext = pVar; - pVar->pNext->pPrev = pVar; - - // move the root so that it points to the new entry -// pRing->pRoot = pRing->pRoot->pPrev; -} - -/**Function************************************************************* - - Synopsis [Removes the node from the ring.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * pVar ) -{ -//printf( "removing %d\n", pVar->Num ); - // check that the var is in a ring - assert( pVar->pPrev ); - assert( pVar->pNext ); - pRing->nItems--; - if ( pRing->nItems == 0 ) - { - assert( pRing->pRoot == pVar ); - pVar->pPrev = NULL; - pVar->pNext = NULL; - pRing->pRoot = NULL; - return; - } - // move the root if needed - if ( pRing->pRoot == pVar ) - pRing->pRoot = pVar->pNext; - // move the root to the next entry after pVar - // this way all the additions to the list will be traversed first -// pRing->pRoot = pVar->pPrev; - // delete the node - pVar->pPrev->pNext = pVar->pNext; - pVar->pNext->pPrev = pVar->pPrev; - pVar->pPrev = NULL; - pVar->pNext = NULL; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |