Recording and reusing learned util clauses in bmc3.

5 files changed, 78 insertions, 16 deletions

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 6527dd3f..fc6a5ef3 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -48,7 +48,7 @@ struct Ga2_Man_t_
     Vec_Int_t *    pvLeaves;        // leaves for each object
     Vec_Int_t *    pvCnfs0;          // positive CNF 
     Vec_Int_t *    pvCnfs1;          // negative CNF
-    Vec_Int_t *    pvMaps;           // mapping into SAT vars for each frame  
+    Vec_Int_t *    pvMaps;           // mapping into SAT vars for each frame  (these should be organized by frame, not by object!)
     // temporaries
     Vec_Int_t *    vCnf;
     Vec_Int_t *    vLits;
diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c
index 38e51f11..4532a90b 100644
--- a/src/aig/gia/giaAbsRef.c
+++ b/src/aig/gia/giaAbsRef.c
@@ -327,7 +327,7 @@ int Rnm_ManSensitize( Rnm_Man_t * p )
 void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect )
 {
     Rnm_Obj_t * pRnm0, * pRnm1, * pRnm = Rnm_ManObj( p, pObj, f );
-    Gia_Obj_t * pFanout;
+    Gia_Obj_t * pFanout = NULL;
     int i, k;//, Id = Gia_ObjId(p->pGia, pObj);
     assert( pRnm->fVisit == 0 );
     pRnm->fVisit = 1;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index fde874df..2fbe88de 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -50,6 +50,7 @@ struct Gia_ManBmc_t_
     int               nHashOver;
     int               nBufNum;     // the number of simple nodes
     int               nDupNum;     // the number of simple nodes
+    int               nUniProps; // propagating learned clause values
     // SAT solver
     sat_solver *      pSat;        // SAT solver
     int               nSatVars;    // SAT variables
@@ -718,8 +719,8 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
 void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
 {
     if ( p->pPars->fVerbose )
-    printf( "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  Hash overs = %d.\n", 
-        p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver );
+    printf( "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  Hash overs = %d.  UniProps = %d.\n", 
+        p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps );
 //    Aig_ManCleanMarkA( p->pAig );
     if ( p->vCexes )
     {
@@ -1126,7 +1127,36 @@ int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
     unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
     int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
     if ( Value != SAIG_TER_NON )
+    {
+/*
+        // check the value of this literal in the SAT solver
+        if ( Value == SAIG_TER_UND && Saig_ManBmcMapping(p, pObj) )
+        {
+            int Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
+            if ( Lit >= 0  )
+            {
+                assert( Lit >= 2 );
+                if ( p->pSat->assigns[Abc_Lit2Var(Lit)] < 2 )
+                {
+                    p->nUniProps++;
+                    if ( Abc_LitIsCompl(Lit) ^ (p->pSat->assigns[Abc_Lit2Var(Lit)] == 0) )
+                        Value = SAIG_TER_ONE;
+                    else
+                        Value = SAIG_TER_ZER;
+
+//                    Value = SAIG_TER_UND;  // disable!
+
+                    // use the new value
+                    Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
+                    // transfer to the unrolling
+                    if ( Value != SAIG_TER_UND )
+                        Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
+                }
+            }
+        }
+*/
         return Value;
+    }
     if ( Aig_ObjIsCo(pObj) )
     {
         Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
@@ -1251,7 +1281,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     unsigned * pInfo;
     int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
-    int i, f, Lit, status;
+    int i, f, k, Lit, status;
     clock_t clk, clk2, clkOther = 0, clkTotal = clock();
     clock_t nTimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     p = Saig_Bmc3ManStart( pAig );
@@ -1350,23 +1380,35 @@ clkOther += clock() - clk2;
                 RetValue = 0;
                 continue;
             }
-            // solve this output
+            // solve th is output
             fUnfinished = 0;
             sat_solver_compress( p->pSat );
             status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( status == l_False )
-            {/*
-                Lit = lit_neg( Lit );
-                status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-                assert( status );
-                sat_solver_compress( p->pSat );
-              */
+            {
+                if ( 1 )
+                {
+                    // 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 );
+                }
             }
             else if ( status == l_True )
             {
                 Aig_Obj_t * pObjPi;
                 Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
-                int j, k, iBit = Saig_ManRegNum(pAig);
+                int j, iBit = Saig_ManRegNum(pAig);
                 for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) )
                     Saig_ManForEachPi( p->pAig, pObjPi, k )
                     {
@@ -1383,7 +1425,8 @@ clkOther += clock() - clk2;
                         printf( "Var =%8.0f. ",  (double)p->nSatVars );
                         printf( "Cla =%9.0f. ",  (double)p->pSat->stats.clauses );
                         printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
-                        printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
+//                        printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
+                        printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
 //                        ABC_PRT( "Time", clock() - clk );
                         printf( "%4.0f MB",      4.25*(f+1)*p->nObjNums /(1<<20) );
                         printf( "%4.0f MB",      1.0*sat_solver_memory(p->pSat)/(1<<20) );
@@ -1446,7 +1489,8 @@ clkOther += clock() - clk2;
             printf( "Var =%8.0f. ", (double)p->nSatVars );
             printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
             printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
-            printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
+//            printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
+            printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
 //            ABC_PRT( "Time", clock() - clk );
 //            printf( "%4.0f MB",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
             printf( "%4.0f MB",     4.0*(f+1)*p->nObjNums /(1<<20) );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 5472e25d..b2014404 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -505,6 +505,7 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     if (sat_solver_dl(s) <= level)
         return;
 
+    assert( veci_size(&s->trail_lim) > 0 );
     bound   = (veci_begin(&s->trail_lim))[level];
     lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
 
@@ -536,6 +537,8 @@ static void sat_solver_record(sat_solver* s, veci* cls)
     int     h     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
     sat_solver_enqueue(s,*begin,h);
     assert(veci_size(cls) > 0);
+    if ( h == 0 )
+        veci_push( &s->unit_lits, *begin );
 
     ///////////////////////////////////
     // add clause to internal storage
@@ -554,6 +557,16 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 */
 }
 
+int sat_solver_count_assigned(sat_solver* s)
+{
+    // count top-level assignments
+    int i, Count = 0;
+    assert(sat_solver_dl(s) == 0);
+    for ( i = 0; i < s->size; i++ )
+        if (var_value(s, i) != varX)
+            Count++;
+    return Count;
+}
 
 static double sat_solver_progress(sat_solver* s)
 {
@@ -931,6 +944,7 @@ sat_solver* sat_solver_new(void)
     veci_new(&s->stack);
 //    veci_new(&s->model);
     veci_new(&s->act_vars);
+    veci_new(&s->unit_lits);
     veci_new(&s->temp_clause);
     veci_new(&s->conf_final);
 
@@ -1052,6 +1066,7 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->stack);
 //    veci_delete(&s->model);
     veci_delete(&s->act_vars);
+    veci_delete(&s->unit_lits);
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
 
@@ -1157,6 +1172,7 @@ double sat_solver_memory( sat_solver* s )
 //    Mem += s->learned.cap * sizeof(int);
     Mem += s->stack.cap * sizeof(int);
     Mem += s->act_vars.cap * sizeof(int);
+    Mem += s->unit_lits.cap * sizeof(int);
     Mem += s->act_clas.cap * sizeof(int);
     Mem += s->temp_clause.cap * sizeof(int);
     Mem += s->conf_final.cap * sizeof(int);
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index eace9eea..24350b36 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -53,6 +53,7 @@ extern int         sat_solver_nvars(sat_solver* s);
 extern int         sat_solver_nclauses(sat_solver* s);
 extern int         sat_solver_nconflicts(sat_solver* s);
 extern double      sat_solver_memory(sat_solver* s);
+extern int         sat_solver_count_assigned(sat_solver* s);
 
 extern void        sat_solver_setnvars(sat_solver* s,int n);
 extern int         sat_solver_get_var_value(sat_solver* s, int v);
@@ -155,7 +156,8 @@ struct sat_solver_t
     double*     factors;       // the activity factors
     int         nRestarts;     // the number of local restarts
     int         nCalls;        // the number of local restarts
-    int         nCalls2;        // the number of local restarts
+    int         nCalls2;       // the number of local restarts
+    veci        unit_lits;     // variables whose activity has changed
 
     int         fSkipSimplify; // set to one to skip simplification of the clause database
     int         fNotUseRandom; // do not allow random decisions with a fixed probability