From 719b06f91295cc0dd811241b7bc30707546241bd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 20 Jan 2012 17:55:34 -0800 Subject: Variable timeframe abstraction. --- src/sat/bsat/satProof.c | 29 +++++++++++++++++------------ src/sat/bsat/satSolver.h | 6 +++--- src/sat/bsat/satSolver2.c | 28 ++++++++++++++++------------ src/sat/bsat/satSolver2.h | 6 +++--- 4 files changed, 39 insertions(+), 30 deletions(-) (limited to 'src/sat/bsat') diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 27fd698c..79179952 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -443,12 +443,13 @@ 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->learnts, s->hLearntLast>>1)->Id]; - Vec_Rec_t * vResolves; Vec_Int_t * vUsed, * vTemp; satset * pSet, * pSet0, * pSet1; - int i, k, Handle, Counter = 0, clk = clock(); + int i, k, hRoot, Handle, Counter = 0, clk = clock(); + if ( s->hLearntLast < 0 ) + return; + hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; // collect visited clauses vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); Proof_CleanCollected( vProof, vUsed ); @@ -509,7 +510,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_ if ( pFanin && !pFanin->mark ) { pFanin->mark = 1; - Vec_IntPush( vCore, pNode->pEnts[i] >> 2 ); + Vec_IntPush( vCore, pNode->pEnts[k] >> 2 ); } } // clean core clauses and reexpress core in terms of clause IDs @@ -586,13 +587,14 @@ 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->learnts, s->hLearntLast>>1)->Id]; - Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; satset * pNode, * pFanin; Aig_Man_t * pAig; Aig_Obj_t * pObj; - int i, k, iVar, Lit, Entry; + int i, k, iVar, Lit, Entry, hRoot; + if ( s->hLearntLast < 0 ) + return NULL; + hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; Sat_ProofInterpolantCheckVars( s, vGlobVars ); @@ -683,16 +685,17 @@ word * Sat_ProofInterpolantTruth( 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->learnts, s->hLearntLast>>1)->Id]; - Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; satset * pNode, * pFanin; Tru_Man_t * pTru; int nVars = Vec_IntSize(vGlobVars); int nWords = (nVars < 6) ? 1 : (1 << (nVars-6)); word * pRes = ABC_ALLOC( word, nWords ); - int i, k, iVar, Lit, Entry; + int i, k, iVar, Lit, Entry, hRoot; assert( nVars > 0 && nVars <= 16 ); + if ( s->hLearntLast < 0 ) + return NULL; + hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; Sat_ProofInterpolantCheckVars( s, vGlobVars ); @@ -789,9 +792,11 @@ 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->learnts, s->hLearntLast>>1)->Id]; - Vec_Int_t * vCore, * vUsed; + int hRoot; + if ( s->hLearntLast < 0 ) + return NULL; + hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; // collect visited clauses vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); // collect core clauses diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 1437f5c1..0ca934ed 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -292,19 +292,19 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i assert( Cid ); return 4; } -static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int fCompl ) +static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int iVar2, int fCompl ) { lit Lits[2]; int Cid; assert( iVar >= 0 ); Lits[0] = toLitCond( iVar, fCompl ); - Lits[1] = toLitCond( iVar+1, 0 ); + Lits[1] = toLitCond( iVar2, 0 ); Cid = sat_solver_addclause( pSat, Lits, Lits + 2 ); assert( Cid ); Lits[0] = toLitCond( iVar, fCompl ); - Lits[1] = toLitCond( iVar+1, 1 ); + Lits[1] = toLitCond( iVar2, 1 ); Cid = sat_solver_addclause( pSat, Lits, Lits + 2 ); assert( Cid ); return 2; diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index f4625d51..f2215fea 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -150,7 +150,8 @@ static inline int clause_is_used(sat_solver2* s, cla h) { return (h & 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 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++; } +//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++; } +static inline void var_set_unit_clause(sat_solver2* s, int v, cla i){ assert(v >= 0 && v < s->size); s->units[v] = i; s->nUnits++; } // these two only work after creating a clause before the solver is called int clause_is_partA (sat_solver2* s, int h) { return clause_read(s, h)->partA; } @@ -1102,7 +1103,8 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts) if (solver2_dlevel(s) <= s->root_level){ #ifdef SAT_USE_ANALYZE_FINAL proof_id = solver2_analyze_final(s, confl, 0); - if ( proof_id > 0 ) + assert( proof_id > 0 ); +// if ( proof_id > 0 ) solver2_record(s,&s->conf_final, proof_id); #endif veci_delete(&learnt_clause); @@ -1307,11 +1309,11 @@ void sat_solver2_setnvars(sat_solver2* s,int n) void sat_solver2_delete(sat_solver2* s) { - veci * pCore; +// veci * pCore; // report statistics printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits ); - +/* pCore = Sat_ProofCore( s ); printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); veci_delete( pCore ); @@ -1319,7 +1321,7 @@ void sat_solver2_delete(sat_solver2* s) if ( s->fProofLogging ) Sat_ProofCheck( s ); - +*/ // delete vectors veci_delete(&s->order); veci_delete(&s->trail_lim); @@ -1392,7 +1394,7 @@ int sat_solver2_addclause__(sat_solver2* s, lit* begin, lit* end) // delete duplicates last = lit_Undef; for (i = j = begin; i < end; i++){ - //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)])); + //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -var_value(s, lit_var(*i)) : var_value(s, lit_var(*i)))); if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i)) return true; // tautology else if (*i != last && var_value(s, lit_var(*i)) == varX) @@ -1634,9 +1636,9 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim int restart_iter = 0; ABC_INT64_T nof_conflicts; ABC_INT64_T nof_learnts = sat_solver2_nclauses(s) / 3; - lbool status = l_Undef; -// lbool* values = s->assigns; - lit* i; + lbool status = l_Undef; + int proof_id; + lit * i; s->hLearntLast = -1; @@ -1659,7 +1661,6 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim //printf("solve: "); printlits(begin, end); printf("\n"); for (i = begin; i < end; i++){ -// switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){ switch (var_value(s, *i)) { case var1: // l_True: break; @@ -1723,17 +1724,19 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim if (r != NULL) { satset* confl = r; - solver2_analyze_final(s, confl, 1); + proof_id = solver2_analyze_final(s, confl, 1); veci_push(&s->conf_final, lit_neg(p)); } else { + proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions) veci_resize(&s->conf_final,0); veci_push(&s->conf_final, lit_neg(p)); // the two lines below are a bug fix by Siert Wieringa if (var_level(s, lit_var(p)) > 0) veci_push(&s->conf_final, p); } + solver2_record(s, &s->conf_final, proof_id); solver2_canceluntil(s, 0); return l_False; } @@ -1741,9 +1744,10 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim { satset* confl = solver2_propagate(s); if (confl != NULL){ - solver2_analyze_final(s, confl, 0); + proof_id = solver2_analyze_final(s, confl, 0); assert(s->conf_final.size > 0); solver2_canceluntil(s, 0); + solver2_record(s,&s->conf_final, proof_id); return l_False; } } diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 4b26f55f..baccf68d 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -355,20 +355,20 @@ static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, clause_set_partA( pSat, Cid, 1 ); return 4; } -static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int fCompl, int fMark ) +static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark ) { lit Lits[2]; int Cid; assert( iVar >= 0 ); Lits[0] = toLitCond( iVar, fCompl ); - Lits[1] = toLitCond( iVar+1, 0 ); + Lits[1] = toLitCond( iVar2, 0 ); Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); if ( fMark ) clause_set_partA( pSat, Cid, 1 ); Lits[0] = toLitCond( iVar, fCompl ); - Lits[1] = toLitCond( iVar+1, 1 ); + Lits[1] = toLitCond( iVar2, 1 ); Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 ); if ( fMark ) clause_set_partA( pSat, Cid, 1 ); -- cgit v1.2.3