diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-04-07 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-04-07 08:01:00 -0700 |
commit | 3f4fc5e4507f7fb9df431fc116529b4c209ab97c (patch) | |
tree | d468f472a10aa98499f98c639447b7838e495476 /src/sat | |
parent | 8e5398c501a873dffcb562a11bc19e630872c931 (diff) | |
download | abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.tar.gz abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.tar.bz2 abc-3f4fc5e4507f7fb9df431fc116529b4c209ab97c.zip |
Version abc60407
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/aig/rwrTruth.c | 2 | ||||
-rw-r--r-- | src/sat/asat/added.c | 27 | ||||
-rw-r--r-- | src/sat/asat/jfront.c | 514 | ||||
-rw-r--r-- | src/sat/asat/module.make | 1 | ||||
-rw-r--r-- | src/sat/asat/solver.c | 40 | ||||
-rw-r--r-- | src/sat/asat/solver.h | 14 | ||||
-rw-r--r-- | src/sat/csat/csat_apis.c | 23 | ||||
-rw-r--r-- | src/sat/fraig/fraig.h | 27 | ||||
-rw-r--r-- | src/sat/fraig/fraigApi.c | 2 | ||||
-rw-r--r-- | src/sat/fraig/fraigInt.h | 6 | ||||
-rw-r--r-- | src/sat/fraig/fraigMan.c | 40 | ||||
-rw-r--r-- | src/sat/fraig/fraigNode.c | 1 | ||||
-rw-r--r-- | src/sat/fraig/fraigPrime.c | 6 | ||||
-rw-r--r-- | src/sat/fraig/fraigSat.c | 50 | ||||
-rw-r--r-- | src/sat/msat/msatOrderJ.c | 44 |
15 files changed, 759 insertions, 38 deletions
diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c index 63a437ce..92a39f0a 100644 --- a/src/sat/aig/rwrTruth.c +++ b/src/sat/aig/rwrTruth.c @@ -95,7 +95,7 @@ static inline int Aig_WordCountOnes( unsigned val ) val = (val & 0x33333333) + ((val>>2) & 0x33333333); val = (val & 0x0F0F0F0F) + ((val>>4) & 0x0F0F0F0F); val = (val & 0x00FF00FF) + ((val>>8) & 0x00FF00FF); - return (val & 0x0000FFFF) + (val>>8); + return (val & 0x0000FFFF) + (val>>16); } /**Function************************************************************* diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index 497087fb..e1b1bb2a 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -41,6 +41,7 @@ static inline int lit_sign(lit l) { return (l & 1); } static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); +extern void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -77,6 +78,7 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin return; } fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); +// Io_WriteCnfOutputPiMapping( pFile, incrementVars ); fprintf( pFile, "p cnf %d %d\n", p->size, nClauses ); // write the original clauses @@ -161,6 +163,31 @@ int * solver_get_model( solver * p, int * pVars, int nVars ) return pModel; } +/**Function************************************************************* + + Synopsis [Writes the given clause in a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_SatPrintStats( FILE * pFile, solver * p ) +{ + printf( "Start = %4d. Conf = %6d. Dec = %6d. Prop = %7d. Insp = %8d.\n", + (int)p->solver_stats.starts, + (int)p->solver_stats.conflicts, + (int)p->solver_stats.decisions, + (int)p->solver_stats.propagations, + (int)p->solver_stats.inspects ); + printf( "Total runtime = %7.2f sec. Var select = %7.2f sec. Var update = %7.2f sec.\n", + (float)(p->timeTotal)/(float)(CLOCKS_PER_SEC), + (float)(p->timeSelect)/(float)(CLOCKS_PER_SEC), + (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// 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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/asat/module.make b/src/sat/asat/module.make index d5cf69bf..26489191 100644 --- a/src/sat/asat/module.make +++ b/src/sat/asat/module.make @@ -1,3 +1,4 @@ SRC += src/sat/asat/added.c \ src/sat/asat/asatmem.c \ + src/sat/asat/jfront.c \ src/sat/asat/solver.c diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index 1130d437..6d76d890 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -121,6 +121,7 @@ static inline void vec_remove(vec* v, void* e) static inline void order_update(solver* s, int v) // updateorder { +// int clk = clock(); int* orderpos = s->orderpos; double* activity = s->activity; int* heap = (int*)vec_begin(&s->order); @@ -138,6 +139,7 @@ static inline void order_update(solver* s, int v) // updateorder } heap[i] = x; orderpos[x] = i; +// s->timeUpdate += clock() - clk; } static inline void order_assigned(solver* s, int v) @@ -146,16 +148,19 @@ static inline void order_assigned(solver* s, int v) static inline void order_unassigned(solver* s, int v) // undoorder { +// int clk = clock(); int* orderpos = s->orderpos; if (orderpos[v] == -1){ orderpos[v] = vec_size(&s->order); vec_push(&s->order,(void*)v); order_update(s,v); } +// s->timeUpdate += clock() - clk; } static int order_select(solver* s, float random_var_freq) // selectvar { +// int clk = clock(); int* heap; double* activity; int* orderpos; @@ -215,9 +220,15 @@ static int order_select(solver* s, float random_var_freq) // selectvar return next; } +// s->timeSelect += clock() - clk; return var_Undef; } +// J-frontier +extern void Asat_JManAssign( Asat_JMan_t * p, int Var ); +extern void Asat_JManUnassign( Asat_JMan_t * p, int Var ); +extern int Asat_JManSelect( Asat_JMan_t * p ); + //================================================================================================= // Activity functions: @@ -236,7 +247,7 @@ static inline void act_var_bump(solver* s, int v) { //printf("bump %d %f\n", v-1, activity[v]); - if (s->orderpos[v] != -1) + if ( s->pJMan == NULL && s->orderpos[v] != -1 ) order_update(s,v); } @@ -422,7 +433,10 @@ static inline bool enqueue(solver* s, lit l, clause* from) reasons[v] = from; s->trail[s->qtail++] = l; - order_assigned(s, v); + if ( s->pJMan ) + Asat_JManAssign( s->pJMan, v ); + else + order_assigned(s, v); return 1; } } @@ -460,8 +474,12 @@ static inline void solver_canceluntil(solver* s, int level) { reasons[x] = (clause*)0; } - for (c = s->qhead-1; c >= bound; c--) - order_unassigned(s,lit_var(trail[c])); + if ( s->pJMan ) + for (c = s->qtail-1; c >= bound; c--) + Asat_JManUnassign( s->pJMan, lit_var(trail[c]) ); + else + for (c = s->qhead-1; c >= bound; c--) + order_unassigned( s, lit_var(trail[c]) ); s->qhead = s->qtail = bound; vec_resize(&s->trail_lim,level); @@ -803,7 +821,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) int* levels = s->levels; double var_decay = 0.95; double clause_decay = 0.999; - double random_var_freq = 0.02; + double random_var_freq = 0.0;//0.02; int conflictC = 0; vec learnt_clause; @@ -872,7 +890,10 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) // New variable decision: s->solver_stats.decisions++; - next = order_select(s,(float)random_var_freq); + if ( s->pJMan ) + next = Asat_JManSelect( s->pJMan ); + else + next = order_select(s,(float)random_var_freq); if (next == var_Undef){ // Model found: @@ -953,7 +974,10 @@ solver* solver_new(void) #else s->pMem = Asat_MmStepStart( 10 ); #endif - + s->pJMan = NULL; + s->timeTotal = clock(); + s->timeSelect = 0; + s->timeUpdate = 0; return s; } @@ -998,6 +1022,7 @@ void solver_delete(solver* s) free(s->tags ); } + if ( s->pJMan ) Asat_JManStop( s ); free(s); } @@ -1155,6 +1180,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit printf("==============================================================================\n"); solver_canceluntil(s,0); + s->timeTotal = clock() - s->timeTotal; return status; } diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 62815656..3684d259 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -64,6 +64,8 @@ static inline lit toLitCond (int v, int c) { return v + v + (int)(c != 0); } //================================================================================================= // Public interface: +typedef struct Asat_JMan_t_ Asat_JMan_t; + struct solver_t; typedef struct solver_t solver; @@ -82,6 +84,12 @@ extern int solver_nclauses(solver* s); extern void Asat_SolverWriteDimacs( solver * pSat, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars); +extern void Asat_SatPrintStats( FILE * pFile, solver * p ); + +// J-frontier support +extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit ); +extern void Asat_JManStop( solver * pSat ); + struct stats_t { @@ -143,7 +151,13 @@ struct solver_t // the memory manager Asat_MmStep_t * pMem; + // J-frontier + Asat_JMan_t * pJMan; + stats solver_stats; + int timeTotal; + int timeSelect; + int timeUpdate; }; #ifdef __cplusplus diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 2129bfb0..9184cab9 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -17,6 +17,7 @@ ***********************************************************************/ #include "abc.h" +#include "fraig.h" #include "csat_apis.h" //////////////////////////////////////////////////////////////////////// @@ -105,6 +106,8 @@ ABC_Manager ABC_InitManager() ***********************************************************************/ void ABC_ReleaseManager( ABC_Manager mng ) { + CSAT_Target_ResultT * p_res = ABC_Get_Target_Result( mng,0 ); + ABC_TargetResFree(p_res); if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name ); if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); if ( mng->pMmNames ) Extra_MmFlexStop( mng->pMmNames, 0 ); @@ -536,6 +539,7 @@ void ABC_AnalyzeTargets( ABC_Manager mng ) ***********************************************************************/ enum CSAT_StatusT ABC_Solve( ABC_Manager mng ) { + Prove_Params_t Params, * pParams = &Params; int RetValue, i; // check if the target network is available @@ -544,9 +548,16 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng ) // try to prove the miter using a number of techniques if ( mng->mode ) - RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0 ); + RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0, 0 ); else - RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 ); + { + // set default parameters for CEC + Prove_ParamsSetDefault( pParams ); + // set infinite resource limit for the final mitering + pParams->nMiteringLimitLast = ABC_INFINITY; + // call the checker + RetValue = Abc_NtkMiterProve( &mng->pTarget, pParams ); + } // analyze the result mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); @@ -658,6 +669,14 @@ void ABC_TargetResFree( CSAT_Target_ResultT * p ) { if ( p == NULL ) return; + if( p->names ) + { + int i = 0; + for ( i = 0; i < p->no_sig; i++ ) + { + FREE(p->names[i]); + } + } FREE( p->names ); FREE( p->values ); free( p ); diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 4e2a295e..d6215465 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -41,6 +41,7 @@ typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t; typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t; typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t; typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t; +typedef struct Prove_ParamsStruct_t_ Prove_Params_t; struct Fraig_ParamsStruct_t_ { @@ -61,6 +62,31 @@ struct Fraig_ParamsStruct_t_ int fInternal; // is set to 1 for internal fraig calls }; +struct Prove_ParamsStruct_t_ +{ + // general parameters + int fUseFraiging; // enables fraiging + int fUseRewriting; // enables rewriting + int fUseBdds; // enables BDD construction when other methods fail + int fVerbose; // prints verbose stats + // iterations + int nItersMax; // the number of iterations + // mitering + int nMiteringLimitStart; // starting mitering limit + float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration + // rewriting + int nRewritingLimitStart; // the number of rewriting iterations + float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration + // fraiging + int nFraigingLimitStart; // starting backtrack(conflict) limit + float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration + // last-gasp BDD construction + int nBddSizeLimit; // the number of BDD nodes when construction is aborted + int fBddReorder; // enables dynamic BDD variable reordering + // last-gasp mitering + int nMiteringLimitLast; // final mitering limit +}; + //////////////////////////////////////////////////////////////////////// /// GLOBAL VARIABLES /// //////////////////////////////////////////////////////////////////////// @@ -155,6 +181,7 @@ extern Fraig_Node_t * Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode, extern void Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew ); /*=== fraigMan.c =============================================================*/ +extern void Prove_ParamsSetDefault( Prove_Params_t * pParams ); extern void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ); extern void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams ); extern Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ); diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c index 3b8da17f..b4bdbcab 100644 --- a/src/sat/fraig/fraigApi.c +++ b/src/sat/fraig/fraigApi.c @@ -65,7 +65,7 @@ int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) { // returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns) int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; } // returns the number of times FRAIG package timed out -int Fraig_ManReadSatFails( Fraig_Man_t * p ) { return p->nSatFails; } +int Fraig_ManReadSatFails( Fraig_Man_t * p ) { return p->nSatFailsReal; } /**Function************************************************************* diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 890af13c..8e016331 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -189,7 +189,8 @@ struct Fraig_ManStruct_t_ int nSatCalls; // the number of times equivalence checking was called int nSatProof; // the number of times a proof was found int nSatCounter; // the number of times a counter example was found - int nSatFails; // the number of times the SAT solver failed to complete + int nSatFails; // the number of times the SAT solver failed to complete due to resource limit or prediction + int nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit int nSatCallsImp; // the number of times equivalence checking was called int nSatProofImp; // the number of times a proof was found @@ -243,8 +244,9 @@ struct Fraig_NodeStruct_t_ unsigned fMark3 : 1; // the mark used for traversals unsigned fFeedUse : 1; // the presence of the variable in the feedback unsigned fFeedVal : 1; // the value of the variable in the feedback + unsigned fFailTfo : 1; // the node is in the TFO of the failed SAT run unsigned nFanouts : 2; // the indicator of fanouts (none, one, or many) - unsigned nOnes : 21; // the number of 1's in the random sim info + unsigned nOnes : 20; // the number of 1's in the random sim info // the children of the node Fraig_Node_t * p1; // the first child diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index ff6faa33..3268ac3a 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -40,6 +40,42 @@ int timeAssign; SeeAlso [] ***********************************************************************/ +void Prove_ParamsSetDefault( Prove_Params_t * pParams ) +{ + // general parameters + pParams->fUseFraiging = 1; // enables fraiging + pParams->fUseRewriting = 1; // enables rewriting + pParams->fUseBdds = 1; // enables BDD construction when other methods fail + pParams->fVerbose = 0; // prints verbose stats + // iterations + pParams->nItersMax = 6; // the number of iterations + // mitering + pParams->nMiteringLimitStart = 1000; // starting mitering limit + pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration + // rewriting + pParams->nRewritingLimitStart = 3; // the number of rewriting iterations + pParams->nRewritingLimitMulti = 1.0; // multiplicative coefficient to increase the limit in each iteration + // fraiging + pParams->nFraigingLimitStart = 2; // starting backtrack(conflict) limit + pParams->nFraigingLimitMulti = 8.0; // multiplicative coefficient to increase the limit in each iteration + // last-gasp BDD construction + pParams->nBddSizeLimit = 1000000; // the number of BDD nodes when construction is aborted + pParams->fBddReorder = 1; // enables dynamic BDD variable reordering + // last-gasp mitering + pParams->nMiteringLimitLast = 1000000; // final mitering limit +} + +/**Function************************************************************* + + Synopsis [Sets the default parameters of the package.] + + Description [This set of parameters is tuned for equivalence checking.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) { memset( pParams, 0, sizeof(Fraig_Params_t) ); @@ -271,8 +307,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p ) (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20); printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory ); - printf( "Proof = %d. Counter-example = %d. Fail = %d. Zero = %d.\n", - p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatZeros ); + printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", + p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros ); printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses ); if ( p->pSat ) Msat_SolverPrintStats( p->pSat ); diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c index 84509e9e..6e3d3c7d 100644 --- a/src/sat/fraig/fraigNode.c +++ b/src/sat/fraig/fraigNode.c @@ -176,6 +176,7 @@ Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_ // compute the level of this node pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level); pNode->fInv = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2); + pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo; // derive the simulation info clk = clock(); diff --git a/src/sat/fraig/fraigPrime.c b/src/sat/fraig/fraigPrime.c index 9745b7e6..127ad478 100644 --- a/src/sat/fraig/fraigPrime.c +++ b/src/sat/fraig/fraigPrime.c @@ -22,7 +22,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -// The 1,000 smallest prime numbers used to compute the hash value +// The 1,024 smallest prime numbers used to compute the hash value // http://www.math.utah.edu/~alfeld/math/primelist.html int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, @@ -93,7 +93,9 @@ int s_FraigPrimes[FRAIG_MAX_PRIMES] = { 2, 3, 5, 7523, 7529, 7537, 7541, 7547, 7549, 7559, 7561, 7573, 7577, 7583, 7589, 7591, 7603, 7607, 7621, 7639, 7643, 7649, 7669, 7673, 7681, 7687, 7691, 7699, 7703, 7717, 7723, 7727, 7741, 7753, 7757, 7759, 7789, 7793, 7817, 7823, 7829, 7841, 7853, 7867, 7873, -7877, 7879, 7883, 7901, 7907, 7919 }; +7877, 7879, 7883, 7901, 7907, 7919, 7927, 7933, 7937, 7949, 7951, 7963, 7993, 8009, +8011, 8017, 8039, 8053, 8059, 8069, 8081, 8087, 8089, 8093, 8101, 8111, 8117, 8123, +8147, 8161 }; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index d4358772..aa28a4f2 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -17,6 +17,7 @@ ***********************************************************************/ #include "fraigInt.h" +#include "math.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -304,6 +305,20 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * assert( !Fraig_IsComplement(pOld) ); assert( pNew != pOld ); + // if at least one of the nodes is a failed node, perform adjustments: + // if the backtrack limit is small, simply skip this node + // if the backtrack limit is > 10, take the quare root of the limit + if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) ) + { + p->nSatFails++; +// return 0; +// if ( nBTLimit > 10 ) +// nBTLimit /= 10; + if ( nBTLimit <= 10 ) + return 0; + nBTLimit = (int)sqrt(nBTLimit); + } + p->nSatCalls++; // make sure the solver is allocated and has enough variables @@ -394,13 +409,27 @@ PRT( "time", clock() - clk ); // record the counter example Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "s(%d)", pNew->Level ); p->nSatCounter++; return 0; } else // if ( RetValue1 == MSAT_UNKNOWN ) { p->time3 += clock() - clk; - p->nSatFails++; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "T(%d)", pNew->Level ); + + // mark the node as the failed node + if ( pOld != p->pConst1 ) + pOld->fFailTfo = 1; + pNew->fFailTfo = 1; +// p->nSatFails++; + p->nSatFailsReal++; return 0; } @@ -454,17 +483,34 @@ PRT( "time", clock() - clk ); // record the counter example Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew ); p->nSatCounter++; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "s(%d)", pNew->Level ); return 0; } else // if ( RetValue1 == MSAT_UNKNOWN ) { p->time3 += clock() - clk; - p->nSatFails++; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "T(%d)", pNew->Level ); + + // mark the node as the failed node + pOld->fFailTfo = 1; + pNew->fFailTfo = 1; +// p->nSatFails++; + p->nSatFailsReal++; return 0; } // return SAT proof p->nSatProof++; + +// if ( pOld->fFailTfo || pNew->fFailTfo ) +// printf( "*" ); +// printf( "u(%d)", pNew->Level ); return 1; } diff --git a/src/sat/msat/msatOrderJ.c b/src/sat/msat/msatOrderJ.c index 5cba1165..4db7ff7b 100644 --- a/src/sat/msat/msatOrderJ.c +++ b/src/sat/msat/msatOrderJ.c @@ -38,7 +38,7 @@ struct Msat_OrderVar_t_ { Msat_OrderVar_t * pNext; Msat_OrderVar_t * pPrev; - int Num; + int Num; }; // the ring of variables data structure (J-boundary) @@ -170,7 +170,8 @@ int Msat_OrderCheck( Msat_Order_t * p ) Msat_OrderVar_t * pVar, * pNext; Msat_IntVec_t * vRound; int * pRound, nRound; - int * pVars, nVars, i; + int * pVars, nVars, i, k; + int Counter = 0; // go through all the variables in the boundary Msat_OrderRingForEachEntry( p->rVars.pRoot, pVar, pNext ) @@ -188,10 +189,14 @@ int Msat_OrderCheck( Msat_Order_t * p ) if ( Msat_OrderVarIsAssigned(p, pRound[i]) ) break; } - assert( i != nRound ); - if ( i != nRound ) - return 0; +// 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, @@ -209,16 +214,16 @@ int Msat_OrderCheck( Msat_Order_t * p ) 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++ ) + for ( k = 0; k < nRound; k++ ) { - if ( !Msat_OrderVarIsUsedInCone(p, pRound[i]) ) + if ( !Msat_OrderVarIsUsedInCone(p, pRound[k]) ) continue; - if ( Msat_OrderVarIsAssigned(p, pRound[i]) ) + if ( Msat_OrderVarIsAssigned(p, pRound[k]) ) break; } - assert( i == nRound ); - if ( i == nRound ) - return 0; +// assert( k == nRound ); +// if ( k != nRound ) +// return 0; } return 1; } @@ -256,7 +261,7 @@ int Msat_OrderVarSelect( Msat_Order_t * p ) Msat_OrderVar_t * pVar, * pNext, * pVarBest; double * pdActs = p->pSat->pdActivity; double dfActBest; - int clk = clock(); +// int clk = clock(); pVarBest = NULL; dfActBest = -1.0; @@ -268,12 +273,13 @@ int Msat_OrderVarSelect( Msat_Order_t * p ) pVarBest = pVar; } } -timeSelect += clock() - clk; -timeAssign += clock() - clk; +//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) ); @@ -296,7 +302,7 @@ timeAssign += clock() - clk; void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ) { Msat_IntVec_t * vRound; - int i, clk = clock(); + int i;//, clk = clock(); // make sure the variable is in the boundary assert( Var < p->nVarsAlloc ); @@ -316,7 +322,7 @@ void Msat_OrderVarAssigned( Msat_Order_t * p, int Var ) continue; Msat_OrderRingAddLast( &p->rVars, &p->pVars[vRound->pArray[i]] ); } -timeSelect += clock() - clk; +//timeSelect += clock() - clk; // Msat_OrderCheck( p ); } @@ -334,7 +340,7 @@ timeSelect += clock() - clk; void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) { Msat_IntVec_t * vRound, * vRound2; - int i, k, clk = clock(); + int i, k;//, clk = clock(); // make sure the variable is not in the boundary assert( Var < p->nVarsAlloc ); @@ -363,7 +369,7 @@ void Msat_OrderVarUnassigned( Msat_Order_t * p, int Var ) if ( k == vRound2->nSize ) // there is no assigned vars, delete this one Msat_OrderRingRemove( &p->rVars, &p->pVars[vRound->pArray[i]] ); } -timeSelect += clock() - clk; +//timeSelect += clock() - clk; // Msat_OrderCheck( p ); } @@ -450,7 +456,7 @@ void Msat_OrderRingRemove( Msat_OrderRing_t * pRing, Msat_OrderVar_t * 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->pNext; +// pRing->pRoot = pVar->pPrev; // delete the node pVar->pPrev->pNext = pVar->pNext; pVar->pNext->pPrev = pVar->pPrev; |