Recording and reusing learned util clauses in bmc2.

5 files changed, 22 insertions, 3 deletions

diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c
index 4532a90b..e982ced3 100644
--- a/src/aig/gia/giaAbsRef.c
+++ b/src/aig/gia/giaAbsRef.c
@@ -207,7 +207,7 @@ void Rnm_ManCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs, int
 }
 void Rnm_ManCollect( Rnm_Man_t * p )
 {
-    Gia_Obj_t * pObj;
+    Gia_Obj_t * pObj = NULL;
     int i;
     // mark const/PIs/PPIs
     Gia_ManIncrementTravId( p->pGia );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index c212fe64..01e2b1bd 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1461,6 +1461,8 @@ unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj )
         pTruth = Gla_ObjTruthElem( p, Gia_ObjCioId(pRoot) );
     else if ( Gia_ObjIsAnd(pRoot) )
         pTruth = Gla_ObjTruthNode( p, pRoot );
+    else
+        pTruth = NULL;
     return (unsigned *)Gla_ObjTruthDup( p, Gla_ObjTruthFree2(p), pTruth, Gia_ObjIsCo(pObj) && Gia_ObjFaninC0(pObj) );
 }
 
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 7533c952..94c8d2c0 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -671,7 +671,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
 int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
 {
     Aig_Obj_t * pObj;
-    int i, VarNum, Lit, RetValue;
+    int i, k, VarNum, Lit, status, RetValue;
     assert( Vec_PtrSize(p->vTargets) > 0 );
     if ( p->pSat->qtail != p->pSat->qhead )
     {
@@ -688,7 +688,23 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
         Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
         RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( RetValue == l_False ) // unsat
+        {
+            // add final unit clause
+            Lit = lit_neg( Lit );
+            status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+            assert( status );
+            // add learned units
+            for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
+            {
+                Lit = veci_begin(&p->pSat->unit_lits)[k];
+                status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+                assert( status );
+            }
+            veci_resize(&p->pSat->unit_lits, 0);
+            // propagate units
+            sat_solver_compress( p->pSat );
             continue;
+        }
         if ( RetValue == l_Undef ) // undecided
             return l_Undef;
         // generate counter-example
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index c490b14a..729d0c04 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -2402,7 +2402,7 @@ void Extra_NpnTest()
     clock_t clk = clock();
     word * pFuncs;
     int * pComp, * pPerm;
-    int i, k, nUnique = 0;
+    int i;//, k, nUnique = 0;
 /*
     // read functions
     pFuncs = Extra_NpnRead( "C:\\_projects\\abc\\_TEST\\allan\\lib6var5M.txt", nFuncs );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index b2014404..fa17f41c 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1526,6 +1526,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
         return l_False;
     }
     ////////////////////////////////////////////////
+    veci_resize(&s->unit_lits, 0);
 
     // set the external limits
     s->nCalls++;