Restructing sat_solver_solve() method for pushing/popping assumptions.

3 files changed, 153 insertions, 151 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 6c987672..ba5834f9 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -513,7 +513,7 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
 }
 
 
-static inline int sat_solver_assume(sat_solver* s, lit l){
+static inline int sat_solver_decision(sat_solver* s, lit l){
     assert(s->qtail == s->qhead);
     assert(var_value(s, lit_var(l)) == varX);
 #ifdef VERBOSEDEBUG
@@ -1689,156 +1689,22 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
             }
 
             if ( var_polar(s, next) ) // positive polarity
-                sat_solver_assume(s,toLit(next));
+                sat_solver_decision(s,toLit(next));
             else
-                sat_solver_assume(s,lit_neg(toLit(next)));
+                sat_solver_decision(s,lit_neg(toLit(next)));
         }
     }
 
     return l_Undef; // cannot happen
 }
 
-int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+// internal call to the SAT solver
+int sat_solver_solve_internal(sat_solver* s)
 {
+    lbool status = l_Undef;
     int restart_iter = 0;
-    ABC_INT64_T  nof_conflicts;
-//    ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
-    lbool   status        = l_Undef;
-    lit*    i;
-
-    if ( s->fVerbose )
-        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
-
-    ////////////////////////////////////////////////
-    if ( s->fSolved )
-    {
-        if ( s->pStore )
-        {
-            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
-            assert( RetValue );
-            (void) RetValue;
-        }
-        return l_False;
-    }
-    ////////////////////////////////////////////////
     veci_resize(&s->unit_lits, 0);
-
-    // set the external limits
     s->nCalls++;
-    s->nRestarts  = 0;
-    s->nConfLimit = 0;
-    s->nInsLimit  = 0;
-    if ( nConfLimit )
-        s->nConfLimit = s->stats.conflicts + nConfLimit;
-    if ( nInsLimit )
-//        s->nInsLimit = s->stats.inspects + nInsLimit;
-        s->nInsLimit = s->stats.propagations + nInsLimit;
-    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
-        s->nConfLimit = nConfLimitGlobal;
-    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
-        s->nInsLimit = nInsLimitGlobal;
-
-#ifndef SAT_USE_ANALYZE_FINAL
-
-    //printf("solve: "); printlits(begin, end); printf("\n");
-    for (i = begin; i < end; i++){
-//        switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
-        switch (var_value(s, *i)) {
-        case var1: // l_True: 
-            break;
-        case varX: // l_Undef
-            sat_solver_assume(s, *i);
-            if (sat_solver_propagate(s) == 0)
-                break;
-            // fallthrough
-        case var0: // l_False 
-            sat_solver_canceluntil(s, 0);
-            return l_False;
-        }
-    }
-    s->root_level = sat_solver_dl(s);
-
-#endif
-
-/*
-    // Perform assumptions:
-    root_level = assumps.size();
-    for (int i = 0; i < assumps.size(); i++){
-        Lit p = assumps[i];
-        assert(var(p) < nVars());
-        if (!sat_solver_assume(p)){
-            GClause r = reason[var(p)];
-            if (r != GClause_NULL){
-                Clause* confl;
-                if (r.isLit()){
-                    confl = propagate_tmpbin;
-                    (*confl)[1] = ~p;
-                    (*confl)[0] = r.lit();
-                }else
-                    confl = r.clause();
-                analyzeFinal(confl, true);
-                conflict.push(~p);
-            }else
-                conflict.clear(),
-                conflict.push(~p);
-            cancelUntil(0);
-            return false; }
-        Clause* confl = propagate();
-        if (confl != NULL){
-            analyzeFinal(confl), assert(conflict.size() > 0);
-            cancelUntil(0);
-            return false; }
-    }
-    assert(root_level == decisionLevel());
-*/
-
-#ifdef SAT_USE_ANALYZE_FINAL
-    // Perform assumptions:
-    s->root_level = end - begin;
-    for ( i = begin; i < end; i++ )
-    {
-        lit p = *i;
-        assert(lit_var(p) < s->size);
-        veci_push(&s->trail_lim,s->qtail);
-        if (!sat_solver_enqueue(s,p,0))
-        {
-            int h = s->reasons[lit_var(p)];
-            if (h)
-            {
-                if (clause_is_lit(h))
-                {
-                    (clause_begin(s->binary))[1] = lit_neg(p);
-                    (clause_begin(s->binary))[0] = clause_read_lit(h);
-                    h = s->hBinary;
-                }
-                sat_solver_analyze_final(s, h, 1);
-                veci_push(&s->conf_final, lit_neg(p));
-            }
-            else
-            {
-                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);
-            }
-            sat_solver_canceluntil(s, 0);
-            return l_False; 
-        }
-        else
-        {
-            int fConfl = sat_solver_propagate(s);
-            if (fConfl){
-                sat_solver_analyze_final(s, fConfl, 0);
-                //assert(s->conf_final.size > 0);
-                sat_solver_canceluntil(s, 0);
-                return l_False; }
-        }
-    }
-    assert(s->root_level == sat_solver_dl(s));
-#endif
-
-    s->nCalls2++;
 
     if (s->verbosity >= 1){
         printf("==================================[MINISAT]===================================\n");
@@ -1848,6 +1714,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     }
 
     while (status == l_Undef){
+        ABC_INT64_T nof_conflicts;
         double Ratio = (s->stats.learnts == 0)? 0.0 :
             s->stats.learnts_literals / (double)s->stats.learnts;
         if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
@@ -1858,7 +1725,6 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
                 (double)s->stats.conflicts,
                 (double)s->stats.clauses, 
                 (double)s->stats.clauses_literals,
-//                (double)nof_learnts, 
                 (double)0, 
                 (double)s->stats.learnts, 
                 (double)s->stats.learnts_literals,
@@ -1868,7 +1734,6 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
         }
         nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
         status = sat_solver_search(s, nof_conflicts);
-//        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
             break;
@@ -1880,7 +1745,134 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     if (s->verbosity >= 1)
         printf("==============================================================================\n");
 
+    sat_solver_canceluntil(s,s->root_level);
+    return status;
+}
+
+// pushing one assumption to the stack of assumptions
+int sat_solver_push(sat_solver* s, int p)
+{
+    assert(lit_var(p) < s->size);
+    veci_push(&s->trail_lim,s->qtail);
+    s->root_level++;
+    if (!sat_solver_enqueue(s,p,0))
+    {
+        int h = s->reasons[lit_var(p)];
+        if (h)
+        {
+            if (clause_is_lit(h))
+            {
+                (clause_begin(s->binary))[1] = lit_neg(p);
+                (clause_begin(s->binary))[0] = clause_read_lit(h);
+                h = s->hBinary;
+            }
+            sat_solver_analyze_final(s, h, 1);
+            veci_push(&s->conf_final, lit_neg(p));
+        }
+        else
+        {
+            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);
+        }
+        //sat_solver_canceluntil(s, 0);
+        return false; 
+    }
+    else
+    {
+        int fConfl = sat_solver_propagate(s);
+        if (fConfl){
+            sat_solver_analyze_final(s, fConfl, 0);
+            //assert(s->conf_final.size > 0);
+            //sat_solver_canceluntil(s, 0);
+            return false; }
+    }
+    return true;
+}
+
+// removing one assumption from the stack of assumptions
+void sat_solver_pop(sat_solver* s)
+{
+    assert( sat_solver_dl(s) > 0 );
+    sat_solver_canceluntil(s, --s->root_level);
+}
+
+void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+{
+    // set the external limits
+    s->nRestarts  = 0;
+    s->nConfLimit = 0;
+    s->nInsLimit  = 0;
+    if ( nConfLimit )
+        s->nConfLimit = s->stats.conflicts + nConfLimit;
+    if ( nInsLimit )
+//        s->nInsLimit = s->stats.inspects + nInsLimit;
+        s->nInsLimit = s->stats.propagations + nInsLimit;
+    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
+        s->nConfLimit = nConfLimitGlobal;
+    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
+        s->nInsLimit = nInsLimitGlobal;
+}
+
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
+{
+    lbool status;
+    lit * i;
+    ////////////////////////////////////////////////
+    if ( s->fSolved )
+    {
+        if ( s->pStore )
+        {
+            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
+            assert( RetValue );
+            (void) RetValue;
+        }
+        return l_False;
+    }
+    ////////////////////////////////////////////////
+
+    if ( s->fVerbose )
+        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
+
+    sat_solver_set_resource_limits( s, nConfLimit, nInsLimit, nConfLimitGlobal, nInsLimitGlobal );
+
+#ifdef SAT_USE_ANALYZE_FINAL
+    // Perform assumptions:
+    s->root_level = 0;
+    for ( i = begin; i < end; i++ )
+        if ( !sat_solver_push(s, *i) )
+        {
+            sat_solver_canceluntil(s,0);
+            s->root_level = 0;
+            return l_False;
+        }
+    assert(s->root_level == sat_solver_dl(s));
+#else
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+//        switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
+        switch (var_value(s, *i)) {
+        case var1: // l_True: 
+            break;
+        case varX: // l_Undef
+            sat_solver_decision(s, *i);
+            if (sat_solver_propagate(s) == 0)
+                break;
+            // fallthrough
+        case var0: // l_False 
+            sat_solver_canceluntil(s, 0);
+            return l_False;
+        }
+    }
+    s->root_level = sat_solver_dl(s);
+#endif
+
+    status = sat_solver_solve_internal(s);
+
     sat_solver_canceluntil(s,0);
+    s->root_level = 0;
 
     ////////////////////////////////////////////////
     if ( status == l_False && s->pStore )
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index a0d9c478..401ac213 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -48,6 +48,10 @@ extern int         sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
 extern int         sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt);
 extern int         sat_solver_simplify(sat_solver* s);
 extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
+extern int         sat_solver_solve_internal(sat_solver* s);
+extern int         sat_solver_push(sat_solver* s, int p);
+extern void        sat_solver_pop(sat_solver* s);
+extern void        sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 extern void        sat_solver_restart( sat_solver* s );
 extern void        sat_solver_rollback( sat_solver* s );
 
@@ -223,12 +227,27 @@ static void sat_solver_compress(sat_solver* s)
         (void) RetValue;
     }
 }
+
 static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
 {
     int i;
     for ( i = 0; i < nVars; i++ )
         s->polarity[pVars[i]] = 0;
 }
+static void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
+{
+    int i;
+    for ( i = 0; i < s->size; i++ )
+        s->polarity[i] = 0;
+    for ( i = 0; i < nVars; i++ )
+        s->polarity[pVars[i]] = 1;
+}
+static void sat_solver_set_literal_polarity(sat_solver* s, int * pLits, int nLits )
+{
+    int i;
+    for ( i = 0; i < nLits; i++ )
+        s->polarity[Abc_Lit2Var(pLits[i])] = !Abc_LitIsCompl(pLits[i]);
+}
 
 static int sat_solver_final(sat_solver* s, int ** ppArray)
 {
@@ -279,14 +298,6 @@ static inline int sat_solver_count_usedvars(sat_solver* s)
         }
     return nVars;
 }
-static void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
-{
-    int i;
-    for ( i = 0; i < s->size; i++ )
-        s->polarity[i] = 0;
-    for ( i = 0; i < nVars; i++ )
-        s->polarity[pVars[i]] = 1;
-}
 
 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
 {
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index f1f03ce2..1d94d685 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -192,7 +192,6 @@ static inline double Sat_Wrd2Dbl( word w )  { return (double)(unsigned)(w&0x3FFF
 
 void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 {
-//    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
     printf( "starts        : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) );
     printf( "conflicts     : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) );
     printf( "decisions     : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) );