diff options
Diffstat (limited to 'src/sat/asat/jfront.c')
| -rw-r--r-- | src/sat/asat/jfront.c | 514 |
1 files changed, 0 insertions, 514 deletions
diff --git a/src/sat/asat/jfront.c b/src/sat/asat/jfront.c deleted file mode 100644 index efbe7883..00000000 --- a/src/sat/asat/jfront.c +++ /dev/null @@ -1,514 +0,0 @@ -/**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 <stdio.h> -#include <assert.h> -#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 ); - 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 /// -//////////////////////////////////////////////////////////////////////// - - |