diff options
| -rw-r--r-- | src/sat/bsat/satProof.c | 24 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 262 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 13 |
3 files changed, 218 insertions, 81 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index d51df229..337fe3ca 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -215,7 +215,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed ) SeeAlso [] ***********************************************************************/ -void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) +void Proof_CollectUsed_iter( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) { satset * pNext; int i, hNode; @@ -223,7 +223,7 @@ void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, V return; // start with node pNode->Id = 1; - Vec_IntPush( vStack, Proof_NodeHandle(p, pNode) << 1 ); + Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNode) << 1 ); // perform DFS search while ( Vec_IntSize(vStack) ) { @@ -236,12 +236,12 @@ void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, V // extracted first time Vec_IntPush( vStack, hNode ^ 1 ); // add second time // add its anticedents ; - pNode = Proof_NodeRead( p, hNode >> 1 ); - Proof_NodeForeachFanin( p, pNode, pNext, i ) + pNode = Proof_NodeRead( vProof, hNode >> 1 ); + Proof_NodeForeachFanin( vProof, pNode, pNext, i ) if ( pNext && !pNext->Id ) { pNext->Id = 1; - Vec_IntPush( vStack, Proof_NodeHandle(p, pNext) << 1 ); // add first time + Vec_IntPush( vStack, Proof_NodeHandle(vProof, pNext) << 1 ); // add first time } } } @@ -314,17 +314,17 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int h SeeAlso [] ***********************************************************************/ -void Proof_CollectUsed_rec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed ) +void Proof_CollectUsed_rec( Vec_Int_t * vProof, satset * pNode, Vec_Int_t * vUsed ) { satset * pNext; int i; if ( pNode->Id ) return; pNode->Id = 1; - Proof_NodeForeachFanin( p, pNode, pNext, i ) + Proof_NodeForeachFanin( vProof, pNode, pNext, i ) if ( pNext && !pNext->Id ) - Proof_CollectUsed_rec( p, pNext, vUsed ); - Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) ); + Proof_CollectUsed_rec( vProof, pNext, vUsed ); + Vec_IntPush( vUsed, Proof_NodeHandle(vProof, pNode) ); } /**Function************************************************************* @@ -637,7 +637,7 @@ void Sat_ProofCheck( sat_solver2 * s ) { Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; - int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id]; + int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; Rec_Int_t * vResolves; Vec_Int_t * vUsed, * vTemp; @@ -731,7 +731,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; - int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id]; + int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; satset * pNode, * pFanin; @@ -822,7 +822,7 @@ void * Sat_ProofCore( sat_solver2 * s ) { Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; - int hRoot = veci_begin(&s->claProofs)[satset_read(&s->clauses, s->hLearntLast)->Id]; + int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; Vec_Int_t * vCore, * vUsed; // collect visited clauses diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index bf616a10..2807e4c0 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -141,17 +141,20 @@ static inline void solver2_clear_marks(sat_solver2* s) { //================================================================================================= // Clause datatype + minor functions: -static inline satset* clause_read (sat_solver2* s, cla h) { return satset_read( &s->clauses, h ); } -static inline cla clause_handle (sat_solver2* s, satset* c) { return satset_handle( &s->clauses, c ); } -static inline int clause_check (sat_solver2* s, satset* c) { return satset_check( &s->clauses, c ); } -static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (clause_handle(s,c)<<2) | 1; } +static inline satset* clause_read (sat_solver2* s, cla h) { return (h & 1) ? satset_read(&s->learnts, h>>1) : satset_read(&s->clauses, h>>1); } +static inline cla clause_handle (sat_solver2* s, satset* c) { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1; } +static inline int clause_check (sat_solver2* s, satset* c) { return c->learnt ? satset_check(&s->learnts, c) : satset_check(&s->clauses, c); } +static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | 1; } +static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot; } + + //static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; } //static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } //static inline satset* var_unit_clause(sat_solver2* s, int v) { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL; } //static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(i && !s->reasons[v]); s->reasons[v] = (i << 1) | 1; } -static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; } -static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; } +static inline int var_reason (sat_solver2* s, int v) { return s->reasons[v]; } +static inline int lit_reason (sat_solver2* s, int l) { return s->reasons[lit_var(l)]; } static inline satset* var_unit_clause(sat_solver2* s, int v) { return clause_read(s, s->units[v]); } static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size && !s->units[v]); s->units[v] = i; s->nUnits++; } @@ -161,7 +164,7 @@ void clause_set_partA(sat_solver2* s, int h, int partA) { clause_read(s int clause_id(sat_solver2* s, int h) { return clause_read(s, h)->Id; } #define sat_solver_foreach_clause( s, c, h ) satset_foreach_entry( &s->clauses, c, h, 1 ) -#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->clauses, c, h, s->hLearntFirst ) +#define sat_solver_foreach_learnt( s, c, h ) satset_foreach_entry( &s->learnts, c, h, 1 ) //================================================================================================= // Simple helpers: @@ -377,26 +380,27 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i assert(nLits < 1 || lit_var(begin[0]) < s->size); assert(nLits < 2 || lit_var(begin[1]) < s->size); // add memory if needed - if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap ) - { - int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20); - s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc ); -// memset( veci_begin(&s->clauses) + s->clauses.cap, 0, sizeof(int) * (nMemAlloc - s->clauses.cap) ); -// printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); - s->clauses.cap = nMemAlloc; - if ( veci_size(&s->clauses) == 0 ) - veci_push( &s->clauses, -1 ); - } - // create clause - c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); - ((int*)c)[0] = 0; - c->learnt = learnt; - c->nEnts = nLits; - for (i = 0; i < nLits; i++) - c->pEnts[i] = begin[i]; + // assign clause ID if ( learnt ) { + if ( veci_size(&s->learnts) + satset_size(nLits) > s->learnts.cap ) + { + int nMemAlloc = s->learnts.cap ? 2 * s->learnts.cap : (1 << 20); + s->learnts.ptr = ABC_REALLOC( int, veci_begin(&s->learnts), nMemAlloc ); + // printf( "Reallocing from %d to %d...\n", s->learnts.cap, nMemAlloc ); + s->learnts.cap = nMemAlloc; + if ( veci_size(&s->learnts) == 0 ) + veci_push( &s->learnts, -1 ); + } + // create clause + c = (satset*)(veci_begin(&s->learnts) + veci_size(&s->learnts)); + ((int*)c)[0] = 0; + c->learnt = learnt; + c->nEnts = nLits; + for (i = 0; i < nLits; i++) + c->pEnts[i] = begin[i]; + // count the clause s->stats.learnts++; s->stats.learnts_literals += nLits; c->Id = s->stats.learnts; @@ -406,28 +410,44 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i veci_push(&s->claProofs, proof_id); if ( nLits > 2 ) act_clause_bump( s,c ); - + // extend storage + Cid = (veci_size(&s->learnts) << 1) | 1; + s->learnts.size += satset_size(nLits); + assert( veci_size(&s->learnts) <= s->learnts.cap ); + assert(((ABC_PTRUINT_T)c & 3) == 0); // printf( "Clause for proof %d: ", proof_id ); // satset_print( c ); } else { + if ( veci_size(&s->clauses) + satset_size(nLits) > s->clauses.cap ) + { + int nMemAlloc = s->clauses.cap ? 2 * s->clauses.cap : (1 << 20); + s->clauses.ptr = ABC_REALLOC( int, veci_begin(&s->clauses), nMemAlloc ); + // printf( "Reallocing from %d to %d...\n", s->clauses.cap, nMemAlloc ); + s->clauses.cap = nMemAlloc; + if ( veci_size(&s->clauses) == 0 ) + veci_push( &s->clauses, -1 ); + } + // create clause + c = (satset*)(veci_begin(&s->clauses) + veci_size(&s->clauses)); + ((int*)c)[0] = 0; + c->learnt = learnt; + c->nEnts = nLits; + for (i = 0; i < nLits; i++) + c->pEnts[i] = begin[i]; + // count the clause s->stats.clauses++; s->stats.clauses_literals += nLits; c->Id = s->stats.clauses; + // extend storage + Cid = (veci_size(&s->clauses) << 1); + s->clauses.size += satset_size(nLits); + assert( veci_size(&s->clauses) <= s->clauses.cap ); + assert(((ABC_PTRUINT_T)c & 3) == 0); + // remember the last one + s->hLearntLast = Cid; } - - // extend storage - Cid = veci_size(&s->clauses); - s->clauses.size += satset_size(nLits); - assert( veci_size(&s->clauses) <= s->clauses.cap ); - assert(((ABC_PTRUINT_T)c & 3) == 0); - - // remember the last one and first learnt - s->hLearntLast = Cid; - if ( learnt && s->hLearntFirst == -1 ) - s->hLearntFirst = Cid; - // watch the clause if ( nLits > 1 ){ veci_push(solver2_wlist(s,lit_neg(begin[0])),Cid); @@ -439,7 +459,7 @@ static int clause_create_new(sat_solver2* s, lit* begin, lit* end, int learnt, i //================================================================================================= // Minor (solver) functions: -static inline int solver2_enqueue(sat_solver2* s, lit l, int from) +static inline int solver2_enqueue(sat_solver2* s, lit l, cla from) { int v = lit_var(l); #ifdef VERBOSEDEBUG @@ -507,7 +527,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id) { lit* begin = veci_begin(cls); lit* end = begin + veci_size(cls); - int Cid = clause_create_new(s,begin,end,1, proof_id); + cla Cid = clause_create_new(s,begin,end,1, proof_id); assert(veci_size(cls) > 0); if ( veci_size(cls) == 1 ) { @@ -1195,38 +1215,50 @@ sat_solver2* sat_solver2_new(void) veci_new(&s->min_lit_order); veci_new(&s->min_step_order); veci_new(&s->learnt_live); - veci_new(&s->proofs); veci_push(&s->proofs, -1); - veci_new(&s->claActs); veci_push(&s->claActs, -1); - veci_new(&s->claProofs); veci_push(&s->claProofs, -1); + veci_new(&s->claActs); veci_push(&s->claActs, -1); + veci_new(&s->claProofs); veci_push(&s->claProofs, -1); - // initialize other - s->hLearntFirst = -1; // the first learnt clause - s->hLearntLast = -1; // the last learnt clause #ifdef USE_FLOAT_ACTIVITY2 - s->var_inc = 1; - s->cla_inc = 1; - s->var_decay = (float)(1 / 0.95 ); - s->cla_decay = (float)(1 / 0.999 ); -// s->cla_decay = 1; -// s->var_decay = 1; + s->var_inc = 1; + s->cla_inc = 1; + s->var_decay = (float)(1 / 0.95 ); + s->cla_decay = (float)(1 / 0.999 ); +// s->cla_decay = 1; +// s->var_decay = 1; #else - s->var_inc = (1 << 5); - s->cla_inc = (1 << 11); + s->var_inc = (1 << 5); + s->cla_inc = (1 << 11); #endif - s->random_seed = 91648253; + s->random_seed = 91648253; #ifdef SAT_USE_PROOF_LOGGING - s->fProofLogging = 1; + s->fProofLogging = 1; #else - s->fProofLogging = 0; + s->fProofLogging = 0; #endif - // prealloc some arrays + // prealloc clause + assert( !s->clauses.ptr ); + s->clauses.cap = (1 << 20); + s->clauses.ptr = ABC_ALLOC( int, s->clauses.cap ); + veci_push(&s->clauses, -1); + // prealloc learnt + assert( !s->learnts.ptr ); + s->learnts.cap = (1 << 20); + s->learnts.ptr = ABC_ALLOC( int, s->learnts.cap ); + veci_push(&s->learnts, -1); + // prealloc proofs if ( s->fProofLogging ) { + assert( !s->proofs.ptr ); s->proofs.cap = (1 << 20); - s->proofs.ptr = ABC_REALLOC( int, s->proofs.ptr, s->proofs.cap ); + s->proofs.ptr = ABC_ALLOC( int, s->proofs.cap ); + veci_push(&s->proofs, -1); } + // initialize clause pointers + s->hClausePivot = 1; + s->hLearntPivot = 1; + s->hLearntLast = -1; // the last learnt clause return s; } @@ -1254,8 +1286,12 @@ void sat_solver2_setnvars(sat_solver2* s,int n) } for (var = s->size; var < n; var++){ - veci_new(&s->wlists[2*var]); - veci_new(&s->wlists[2*var+1]); + assert(!s->wlists[2*var].size); + assert(!s->wlists[2*var+1].size); + if ( s->wlists[2*var].ptr == NULL ) + veci_new(&s->wlists[2*var]); + if ( s->wlists[2*var+1].ptr == NULL ) + veci_new(&s->wlists[2*var+1]); *((int*)s->vi + var) = 0; s->vi[var].val = varX; s->orderpos[var] = veci_size(&s->order); s->reasons [var] = 0; @@ -1304,6 +1340,7 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->claActs); veci_delete(&s->claProofs); veci_delete(&s->clauses); + veci_delete(&s->learnts); // delete arrays if (s->vi != 0){ @@ -1460,15 +1497,17 @@ void solver2_reducedb(sat_solver2* s) veci_size(&s->learnt_live), s->stats.learnts, 100.0 * veci_size(&s->learnt_live) / s->stats.learnts ); // remap clause proofs and clauses - hHandle = s->hLearntFirst; - pArray = veci_begin(&s->claProofs); + hHandle = 1; + pArray = s->fProofLogging ? veci_begin(&s->claProofs) : NULL; pArray2 = veci_begin(&s->claActs); - satset_foreach_entry_vec( &s->learnt_live, &s->clauses, c, i ) + satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) { + if ( pArray ) pArray[i+1] = pArray[c->Id]; pArray2[i+1] = pArray2[c->Id]; c->Id = hHandle; hHandle += satset_size(c->nEnts); } + if ( s->fProofLogging ) veci_resize(&s->claProofs,veci_size(&s->learnt_live)+1); veci_resize(&s->claActs,veci_size(&s->learnt_live)+1); @@ -1477,33 +1516,120 @@ void solver2_reducedb(sat_solver2* s) { pArray = veci_begin(&s->wlists[i]); for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) - if ( pArray[k] < s->hLearntFirst ) + if ( pArray[k] & 1 ) pArray[j++] = pArray[k]; else if ( !(c = clause_read(s, pArray[k]))->mark ) pArray[j++] = c->Id; veci_resize(&s->wlists[i],j); } // compact units + if ( s->fProofLogging ) for ( i = 0; i < s->size; i++ ) - if ( s->units[i] >= s->hLearntFirst ) + if ( s->units[i] && (s->units[i] & 1) ) s->units[i] = clause_read(s, s->units[i])->Id; // compact clauses - satset_foreach_entry_vec( &s->learnt_live, &s->clauses, c, i ) + satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) { hTemp = c->Id; c->Id = i + 1; - memmove( veci_begin(&s->clauses) + hTemp, c, sizeof(int)*satset_size(c->nEnts) ); + memmove( veci_begin(&s->learnts) + hTemp, c, sizeof(int)*satset_size(c->nEnts) ); } assert( hHandle == hTemp + satset_size(c->nEnts) ); - veci_resize(&s->clauses,hHandle); + veci_resize(&s->learnts,hHandle); s->stats.learnts = veci_size(&s->learnt_live); // compact proof (compacts 'proofs' and update 'claProofs') + if ( s->fProofLogging ) Sat_ProofReduce( s ); TimeTotal += clock() - clk; Abc_PrintTime( 1, "Time", TimeTotal ); } +// reverses to the previously bookmarked point +void sat_solver2_rollback( sat_solver2* s ) +{ + int i, k, j; + assert( s->hClausePivot >= 1 && s->hClausePivot <= veci_size(&s->clauses) ); + assert( s->hLearntPivot >= 1 && s->hLearntPivot <= veci_size(&s->clauses) ); + assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); + veci_resize(&s->order, 0); + if ( s->hClausePivot > 1 || s->hLearntPivot > 1 ) + { + // update order + for ( i = 0; i < s->iVarPivot; i++ ) + { + if ( var_value(s, i) != varX ) + continue; + s->orderpos[i] = veci_size(&s->order); + veci_push(&s->order,i); + order_update(s, i); + } + // compact watches + for ( i = 0; i < s->size*2; i++ ) + { + cla* pArray = veci_begin(&s->wlists[i]); + for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) + if ( clause_is_used(s, pArray[k]) ) + pArray[j++] = pArray[k]; + veci_resize(&s->wlists[i],j); + } + // compact units + if ( s->fProofLogging ) + for ( i = 0; i < s->size; i++ ) + if ( s->units[i] && !clause_is_used(s, s->units[i]) ) + s->units[i] = 0; + } + // reset + if ( s->hLearntPivot < veci_size(&s->learnts) ) + { + satset* first = satset_read(&s->learnts, s->hLearntPivot); + veci_resize(&s->claActs, first->Id); + if ( s->fProofLogging ) { + veci_resize(&s->claProofs, first->Id); + Sat_ProofReduce( s ); + } + } + veci_resize(&s->clauses, s->hClausePivot); + veci_resize(&s->learnts, s->hLearntPivot); + for ( i = s->iVarPivot; i < s->size*2; i++ ) + s->wlists[i].size = 0; + s->size = s->iVarPivot; + // initialize other vars + if ( s->size == 0 ) + { + // s->size = 0; + // s->cap = 0; + s->qhead = 0; + s->qtail = 0; +#ifdef USE_FLOAT_ACTIVITY + s->var_inc = 1; + s->cla_inc = 1; + s->var_decay = (float)(1 / 0.95 ); + s->cla_decay = (float)(1 / 0.999 ); +#else + s->var_inc = (1 << 5); + s->cla_inc = (1 << 11); +#endif + s->root_level = 0; + s->simpdb_assigns = 0; + s->simpdb_props = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; + } +} + int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) { int restart_iter = 0; diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 8738abdf..063b6376 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -46,6 +46,7 @@ extern void sat_solver2_delete(sat_solver2* s); extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end); extern int sat_solver2_simplify(sat_solver2* s); extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); +extern void sat_solver2_rollback(sat_solver2* s); extern void sat_solver2_setnvars(sat_solver2* s,int n); @@ -112,9 +113,12 @@ struct sat_solver2_t // clauses veci clauses; // clause memory + veci learnts; // learnt memory veci* wlists; // watcher lists (for each literal) - int hLearntFirst; // the first learnt clause + int hClausePivot; // the pivot among problem clause + int hLearntPivot; // the pivot among learned clause int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) + int iVarPivot; // the pivot among the variables veci claActs; // clause activities veci claProofs; // clause proofs @@ -245,6 +249,13 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) return fNotUseRandomOld; } +static inline int sat_solver2_bookmark(sat_solver2* s) +{ + s->hLearntPivot = veci_size(&s->learnts); + s->hClausePivot = veci_size(&s->clauses); + s->iVarPivot = s->size; +} + ABC_NAMESPACE_HEADER_END #endif |