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