diff options
Diffstat (limited to 'src/sat/asat')
| -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 |
5 files changed, 589 insertions, 7 deletions
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 |