Variable timeframe abstraction.

4 files changed, 39 insertions, 30 deletions

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 );