/**CFile**************************************************************** FileName [jfront.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [C-language MiniSat solver.] Synopsis [Implementation of J-frontier.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: jfront.c,v 1.4 2005/09/16 22:55:03 casem Exp $] ***********************************************************************/ #include #include #include "solver.h" #include "extra.h" #include "vec.h" /* At any time during the solving process, the J-frontier is the set of currently unassigned variables, each of which has at least one fanin/fanout variable that is currently assigned. In the context of a CNF-based solver, default decisions based on variable activity are modified to choose the most active variable among those currently on the J-frontier. */ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// // variable on the J-frontier typedef struct Asat_JVar_t_ Asat_JVar_t; struct Asat_JVar_t_ { unsigned int Num; // variable number unsigned int nRefs; // the number of adjacent assigned vars unsigned int Prev; // the previous variable unsigned int Next; // the next variable unsigned int nFans; // the number of fanins/fanouts unsigned int Fans[0]; // the fanin/fanout variables }; // the J-frontier as a ring of variables // (ring is used instead of list because it allows to control the insertion point) typedef struct Asat_JRing_t_ Asat_JRing_t; struct Asat_JRing_t_ { Asat_JVar_t * pRoot; // the pointer to the root int nItems; // the number of variables in the ring }; // the J-frontier manager struct Asat_JMan_t_ { solver * pSat; // the SAT solver Asat_JRing_t rVars; // the ring of variables Vec_Ptr_t * vVars; // the pointers to variables Extra_MmFlex_t * pMem; // the memory manager for variables }; // getting hold of the given variable static inline Asat_JVar_t * Asat_JManVar( Asat_JMan_t * p, int Num ) { return !Num? NULL : Vec_PtrEntry(p->vVars, Num); } static inline Asat_JVar_t * Asat_JVarPrev( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return Asat_JManVar(p, pVar->Prev); } static inline Asat_JVar_t * Asat_JVarNext( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return Asat_JManVar(p, pVar->Next); } //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 //- the array of arrays of variables adjacent to each other static inline int Asat_JVarIsInBoundary( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return pVar->Next > 0; } static inline int Asat_JVarIsAssigned( Asat_JMan_t * p, Asat_JVar_t * pVar ) { return p->pSat->assigns[pVar->Num] != l_Undef; } //static inline int Asat_JVarIsUsedInCone( Asat_JMan_t * p, int Var ) { return p->pSat->vVarsUsed->pArray[i]; } // manipulating the ring of variables static void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar ); static void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar ); // iterator through the entries in J-boundary #define Asat_JRingForEachEntry( p, pVar, pNext ) \ for ( pVar = p->rVars.pRoot, \ pNext = pVar? Asat_JVarNext(p, pVar) : NULL; \ pVar; \ pVar = (pNext != p->rVars.pRoot)? pNext : NULL, \ pNext = pVar? Asat_JVarNext(p, pVar) : NULL ) // iterator through the adjacent variables #define Asat_JVarForEachFanio( p, pVar, pFan, i ) \ for ( i = 0; (i < (int)pVar->nFans) && (((pFan) = Asat_JManVar(p, pVar->Fans[i])), 1); i++ ) extern void Asat_JManAssign( Asat_JMan_t * p, int Var ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Start the J-frontier.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Asat_JMan_t * Asat_JManStart( solver * pSat, void * pCircuit ) { Vec_Vec_t * vCircuit = pCircuit; Asat_JMan_t * p; Asat_JVar_t * pVar; Vec_Int_t * vConnect; int i, nBytes, Entry, k; // make sure the number of variables is less than sizeof(unsigned int) assert( Vec_VecSize(vCircuit) < (1 << 16) ); assert( Vec_VecSize(vCircuit) == pSat->size ); // allocate the manager p = ALLOC( Asat_JMan_t, 1 ); memset( p, 0, sizeof(Asat_JMan_t) ); p->pSat = pSat; p->pMem = Extra_MmFlexStart(); // fill in the variables p->vVars = Vec_PtrAlloc( Vec_VecSize(vCircuit) ); for ( i = 0; i < Vec_VecSize(vCircuit); i++ ) { vConnect = Vec_VecEntry( vCircuit, i ); nBytes = sizeof(Asat_JVar_t) + sizeof(int) * Vec_IntSize(vConnect); nBytes = sizeof(void *) * (nBytes / sizeof(void *) + ((nBytes % sizeof(void *)) != 0)); pVar = (Asat_JVar_t *)Extra_MmFlexEntryFetch( p->pMem, nBytes ); memset( pVar, 0, nBytes ); pVar->Num = i; // add fanins/fanouts pVar->nFans = Vec_IntSize( vConnect ); Vec_IntForEachEntry( vConnect, Entry, k ) pVar->Fans[k] = Entry; // add the variable Vec_PtrPush( p->vVars, pVar ); } // set the current assignments Vec_PtrForEachEntryStart( p->vVars, pVar, i, 1 ) { // if ( !Asat_JVarIsUsedInCone(p, pVar) ) // continue; // skip assigned vars, vars in the boundary, and vars not used in the cone if ( Asat_JVarIsAssigned(p, pVar) ) Asat_JManAssign( p, pVar->Num ); } pSat->pJMan = p; return p; } /**Function************************************************************* Synopsis [Stops the J-frontier.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Asat_JManStop( solver * pSat ) { Asat_JMan_t * p = pSat->pJMan; if ( p == NULL ) return; pSat->pJMan = NULL; Extra_MmFlexStop( p->pMem, 0 ); Vec_PtrFree( p->vVars ); free( p ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Asat_JManCheck( Asat_JMan_t * p ) { Asat_JVar_t * pVar, * pNext, * pFan; // Msat_IntVec_t * vRound; // int * pRound, nRound; // int * pVars, nVars, i, k; int i, k; int Counter = 0; // go through all the variables in the boundary Asat_JRingForEachEntry( p, pVar, pNext ) { assert( !Asat_JVarIsAssigned(p, pVar) ); // 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++ ) Asat_JVarForEachFanio( p, pVar, pFan, i ) { // if ( !Asat_JVarIsUsedInCone(p, pFan) ) // continue; if ( Asat_JVarIsAssigned(p, pFan) ) break; } // assert( i != pVar->nFans ); // if ( i == pVar->nFans ) // return 0; if ( i == (int)pVar->nFans ) 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++ ) Vec_PtrForEachEntry( p->vVars, pVar, i ) { // assert( Asat_JVarIsUsedInCone(p, pVar) ); // skip assigned vars, vars in the boundary, and vars not used in the cone if ( Asat_JVarIsAssigned(p, pVar) || Asat_JVarIsInBoundary(p, pVar) ) 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 ( i = 0; i < nRound; i++ ) Asat_JVarForEachFanio( p, pVar, pFan, k ) { // if ( !Asat_JVarIsUsedInCone(p, pFan) ) // continue; if ( Asat_JVarIsAssigned(p, pFan) ) break; } // assert( k == pVar->nFans ); // if ( k != pVar->nFans ) // return 0; } return 1; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Asat_JManAssign( Asat_JMan_t * p, int Var ) { // Msat_IntVec_t * vRound; Asat_JVar_t * pVar, * pFan; int i, clk = clock(); // make sure the variable is in the boundary assert( Var < Vec_PtrSize(p->vVars) ); // if it is not in the boundary (initial decision, random decision), do not remove pVar = Asat_JManVar( p, Var ); if ( Asat_JVarIsInBoundary( p, pVar ) ) Asat_JRingRemove( p, pVar ); // 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++ ) Asat_JVarForEachFanio( p, pVar, pFan, i ) { // if ( !Asat_JVarIsUsedInCone(p, pFan) ) // continue; pFan->nRefs++; if ( Asat_JVarIsAssigned(p, pFan) || Asat_JVarIsInBoundary(p, pFan) ) continue; Asat_JRingAddLast( p, pFan ); } //timeSelect += clock() - clk; // Asat_JManCheck( p ); p->pSat->timeUpdate += clock() - clk; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Asat_JManUnassign( Asat_JMan_t * p, int Var ) { // Msat_IntVec_t * vRound, * vRound2; Asat_JVar_t * pVar, * pFan; int i, clk = clock();//, k // make sure the variable is not in the boundary assert( Var < Vec_PtrSize(p->vVars) ); pVar = Asat_JManVar( p, Var ); assert( !Asat_JVarIsInBoundary( p, pVar ) ); // 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 ( Asat_JVarIsAssigned(p, vRound->pArray[i]) ) // break; // if ( i != vRound->nSize ) // Asat_JRingAddLast( &p->rVars, &p->pVars[Var] ); if ( pVar->nRefs != 0 ) Asat_JRingAddLast( p, pVar ); /* // unassigning a variable may lead to its adjacents dropping from the boundary for ( i = 0; i < vRound->nSize; i++ ) if ( Asat_JVarIsInBoundary(p, vRound->pArray[i]) ) { // the neighbor is in the J-boundary (and unassigned) assert( !Asat_JVarIsAssigned(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 ( Asat_JVarIsAssigned(p, vRound2->pArray[k]) ) break; if ( k == vRound2->nSize ) // there is no assigned vars, delete this one Asat_JRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] ); } */ Asat_JVarForEachFanio( p, pVar, pFan, i ) { // if ( !Asat_JVarIsUsedInCone(p, pFan) ) // continue; assert( pFan->nRefs > 0 ); pFan->nRefs--; if ( !Asat_JVarIsInBoundary(p, pFan) ) continue; // the neighbor is in the J-boundary (and unassigned) assert( !Asat_JVarIsAssigned(p, pFan) ); // if there is no assigned vars, delete this one if ( pFan->nRefs == 0 ) Asat_JRingRemove( p, pFan ); } //timeSelect += clock() - clk; // Asat_JManCheck( p ); p->pSat->timeUpdate += clock() - clk; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Asat_JManSelect( Asat_JMan_t * p ) { Asat_JVar_t * pVar, * pNext, * pVarBest; double * pdActs = p->pSat->activity; double dfActBest; int clk = clock(); pVarBest = NULL; dfActBest = -1.0; Asat_JRingForEachEntry( p, pVar, pNext ) { if ( dfActBest <= pdActs[pVar->Num] )//+ 0.00001 ) { dfActBest = pdActs[pVar->Num]; pVarBest = pVar; } } //timeSelect += clock() - clk; //timeAssign += clock() - clk; //if ( pVarBest && pVarBest->Num % 1000 == 0 ) //printf( "%d ", p->rVars.nItems ); // Asat_JManCheck( p ); p->pSat->timeSelect += clock() - clk; if ( pVarBest ) { // assert( Asat_JVarIsUsedInCone(p, pVarBest) ); return pVarBest->Num; } return var_Undef; } /**Function************************************************************* Synopsis [Adds node to the end of the ring.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Asat_JRingAddLast( Asat_JMan_t * p, Asat_JVar_t * pVar ) { Asat_JRing_t * pRing = &p->rVars; //printf( "adding %d\n", pVar->Num ); // check that the node is not in a ring assert( pVar->Prev == 0 ); assert( pVar->Next == 0 ); // if the ring is empty, make the node point to itself pRing->nItems++; if ( pRing->pRoot == NULL ) { pRing->pRoot = pVar; // pVar->pPrev = pVar; pVar->Prev = pVar->Num; // pVar->pNext = pVar; pVar->Next = pVar->Num; return; } // if the ring is not empty, add it as the last entry // pVar->pPrev = pRing->pRoot->pPrev; pVar->Prev = pRing->pRoot->Prev; // pVar->pNext = pRing->pRoot; pVar->Next = pRing->pRoot->Num; // pVar->pPrev->pNext = pVar; Asat_JVarPrev(p, pVar)->Next = pVar->Num; // pVar->pNext->pPrev = pVar; Asat_JVarNext(p, pVar)->Prev = pVar->Num; // move the root so that it points to the new entry // pRing->pRoot = pRing->pRoot->pPrev; pRing->pRoot = Asat_JVarPrev(p, pRing->pRoot); } /**Function************************************************************* Synopsis [Removes the node from the ring.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Asat_JRingRemove( Asat_JMan_t * p, Asat_JVar_t * pVar ) { Asat_JRing_t * pRing = &p->rVars; //printf( "removing %d\n", pVar->Num ); // check that the var is in a ring assert( pVar->Prev ); assert( pVar->Next ); pRing->nItems--; if ( pRing->nItems == 0 ) { assert( pRing->pRoot == pVar ); // pVar->pPrev = NULL; pVar->Prev = 0; // pVar->pNext = NULL; pVar->Next = 0; pRing->pRoot = NULL; return; } // move the root if needed if ( pRing->pRoot == pVar ) // pRing->pRoot = pVar->pNext; pRing->pRoot = Asat_JVarNext(p, pVar); // move the root to the next entry after pVar // this way all the additions to the list will be traversed first // pRing->pRoot = pVar->pNext; pRing->pRoot = Asat_JVarPrev(p, pVar); // delete the node // pVar->pPrev->pNext = pVar->pNext; Asat_JVarPrev(p, pVar)->Next = Asat_JVarNext(p, pVar)->Num; // pVar->pNext->pPrev = pVar->pPrev; Asat_JVarNext(p, pVar)->Prev = Asat_JVarPrev(p, pVar)->Num; // pVar->pPrev = NULL; pVar->Prev = 0; // pVar->pNext = NULL; pVar->Next = 0; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////