Version abc50915

3 files changed, 73 insertions, 70 deletions

diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index 98024a7f..d248b115 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -317,11 +317,11 @@ static void clause_remove(solver* s, clause* c)
     vec_remove(solver_read_wlist(s,neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
 
     if (clause_learnt(c)){
-        s->stats.learnts--;
-        s->stats.learnts_literals -= clause_size(c);
+        s->solver_stats.learnts--;
+        s->solver_stats.learnts_literals -= clause_size(c);
     }else{
-        s->stats.clauses--;
-        s->stats.clauses_literals -= clause_size(c);
+        s->solver_stats.clauses--;
+        s->solver_stats.clauses_literals -= clause_size(c);
     }
 
     free(c);
@@ -409,7 +409,7 @@ static inline bool enqueue(solver* s, lit l, clause* from)
         s->trail[s->qtail++] = l;
 
         order_assigned(s, v);
-        return true;
+        return 1;
     }
 }
 
@@ -465,8 +465,8 @@ static void solver_record(solver* s, vec* cls)
     if (c != 0) {
         vec_push(&s->learnts,(void*)c);
         act_clause_bump(s,c);
-        s->stats.learnts++;
-        s->stats.learnts_literals += vec_size(cls);
+        s->solver_stats.learnts++;
+        s->solver_stats.learnts_literals += vec_size(cls);
     }
 }
 
@@ -521,7 +521,7 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
                     for (j = top; j < vec_size(&s->tagged); j++)
                         tags[tagged[j]] = l_Undef;
                     vec_resize(&s->tagged,top);
-                    return false;
+                    return 0;
                 }
             }
         }else{
@@ -541,14 +541,14 @@ static bool solver_lit_removable(solver* s, lit l, int minl)
                         for (j = top; j < vec_size(&s->tagged); j++)
                             tags[tagged[j]] = l_Undef;
                         vec_resize(&s->tagged,top);
-                        return false;
+                        return 0;
                     }
                 }
             }
         }
     }
 
-    return true;
+    return 1;
 }
 
 static void solver_analyze(solver* s, clause* c, vec* learnt)
@@ -627,9 +627,9 @@ static void solver_analyze(solver* s, clause* c, vec* learnt)
     }
 
     // update size of learnt + statistics
-    s->stats.max_literals += vec_size(learnt);
+    s->solver_stats.max_literals += vec_size(learnt);
     vec_resize(learnt,j);
-    s->stats.tot_literals += j;
+    s->solver_stats.tot_literals += j;
 
     // clear tags
     tagged = (int*)vec_begin(&s->tagged);
@@ -684,7 +684,7 @@ clause* solver_propagate(solver* s)
         clause **end   = begin + vec_size(ws);
         clause **i, **j;
 
-        s->stats.propagations++;
+        s->solver_stats.propagations++;
         s->simpdb_props--;
 
         //printf("checking lit %d: "L_LIT"\n", vec_size(ws), L_lit(p));
@@ -746,7 +746,7 @@ clause* solver_propagate(solver* s)
             i++;
         }
 
-        s->stats.inspects += j - (clause**)vec_begin(ws);
+        s->solver_stats.inspects += j - (clause**)vec_begin(ws);
         vec_resize(ws,j - (clause**)vec_begin(ws));
     }
 
@@ -796,7 +796,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 
     assert(s->root_level == solver_dlevel(s));
 
-    s->stats.starts++;
+    s->solver_stats.starts++;
     s->var_decay = (float)(1 / var_decay   );
     s->cla_decay = (float)(1 / clause_decay);
     vec_resize(&s->model,0);
@@ -811,7 +811,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 #ifdef VERBOSEDEBUG
             printf(L_IND"**CONFLICT**\n", L_ind);
 #endif
-            s->stats.conflicts++; conflictC++;
+            s->solver_stats.conflicts++; conflictC++;
             if (solver_dlevel(s) == s->root_level){
                 vec_delete(&learnt_clause);
                 return l_False;
@@ -845,7 +845,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
                 solver_reducedb(s);
 
             // New variable decision:
-            s->stats.decisions++;
+            s->solver_stats.decisions++;
             next = order_select(s,(float)random_var_freq);
 
             if (next == var_Undef){
@@ -910,17 +910,17 @@ solver* solver_new(void)
     s->binary->size_learnt    = (2 << 1);
     s->verbosity              = 0;
 
-    s->stats.starts           = 0;
-    s->stats.decisions        = 0;
-    s->stats.propagations     = 0;
-    s->stats.inspects         = 0;
-    s->stats.conflicts        = 0;
-    s->stats.clauses          = 0;
-    s->stats.clauses_literals = 0;
-    s->stats.learnts          = 0;
-    s->stats.learnts_literals = 0;
-    s->stats.max_literals     = 0;
-    s->stats.tot_literals     = 0;
+    s->solver_stats.starts           = 0;
+    s->solver_stats.decisions        = 0;
+    s->solver_stats.propagations     = 0;
+    s->solver_stats.inspects         = 0;
+    s->solver_stats.conflicts        = 0;
+    s->solver_stats.clauses          = 0;
+    s->solver_stats.clauses_literals = 0;
+    s->solver_stats.learnts          = 0;
+    s->solver_stats.learnts_literals = 0;
+    s->solver_stats.max_literals     = 0;
+    s->solver_stats.tot_literals     = 0;
 
     return s;
 }
@@ -973,7 +973,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
     lbool* values;
     lit last;
 
-    if (begin == end) return false;
+    if (begin == end) return 0;
 
     //printlits(begin,end); printf("\n");
     // insertion sort
@@ -996,7 +996,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
         //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
         lbool sig = !lit_sign(*i); sig += sig - 1;
         if (*i == neg(last) || sig == values[lit_var(*i)])
-            return true;   // tautology
+            return 1;   // tautology
         else if (*i != last && values[lit_var(*i)] == l_Undef)
             last = *j++ = *i;
     }
@@ -1004,7 +1004,7 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
     //printf("final: "); printlits(begin,j); printf("\n");
 
     if (j == begin)          // empty clause
-        return false;
+        return 0;
     else if (j - begin == 1) // unit clause
         return enqueue(s,*begin,(clause*)0);
 
@@ -1012,10 +1012,10 @@ bool solver_addclause(solver* s, lit* begin, lit* end)
     vec_push(&s->clauses,clause_new(s,begin,j,0));
 
 
-    s->stats.clauses++;
-    s->stats.clauses_literals += j - begin;
+    s->solver_stats.clauses++;
+    s->solver_stats.clauses_literals += j - begin;
 
-    return true;
+    return 1;
 }
 
 
@@ -1027,10 +1027,10 @@ bool   solver_simplify(solver* s)
     assert(solver_dlevel(s) == 0);
 
     if (solver_propagate(s) != 0)
-        return false;
+        return 0;
 
     if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
-        return true;
+        return 1;
 
     reasons = s->reasons;
     for (type = 0; type < 2; type++){
@@ -1050,13 +1050,13 @@ bool   solver_simplify(solver* s)
 
     s->simpdb_assigns = s->qhead;
     // (shouldn't depend on 'stats' really, but it will do for now)
-    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+    s->simpdb_props   = (int)(s->solver_stats.clauses_literals + s->solver_stats.learnts_literals);
 
-    return true;
+    return 1;
 }
 
 
-int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
+bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
 {
     double  nof_conflicts = 100;
     double  nof_learnts   = solver_nclauses(s) / 3;
@@ -1068,7 +1068,7 @@ int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
     for (i = begin; i < end; i++)
         if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){
             solver_canceluntil(s,0);
-            return false; }
+            return l_False; }
 
     s->root_level = solver_dlevel(s);
 
@@ -1080,17 +1080,17 @@ int   solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
     }
 
     while (status == l_Undef){
-        double Ratio = (s->stats.learnts == 0)? 0.0 :
-            s->stats.learnts_literals / (double)s->stats.learnts;
+        double Ratio = (s->solver_stats.learnts == 0)? 0.0 :
+            s->solver_stats.learnts_literals / (double)s->solver_stats.learnts;
 
         if (s->verbosity >= 1){
             printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
-                (double)s->stats.conflicts,
-                (double)s->stats.clauses, 
-                (double)s->stats.clauses_literals,
+                (double)s->solver_stats.conflicts,
+                (double)s->solver_stats.clauses, 
+                (double)s->solver_stats.clauses_literals,
                 (double)nof_learnts, 
-                (double)s->stats.learnts, 
-                (double)s->stats.learnts_literals,
+                (double)s->solver_stats.learnts, 
+                (double)s->solver_stats.learnts_literals,
                 Ratio,
                 s->progress_estimate*100);
             fflush(stdout);
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 8e981198..9f80bc7e 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -36,16 +36,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define bool int
 #endif
 
-static const bool  true      = 1;
-static const bool  false     = 0;
-
 typedef int                lit;
 typedef char               lbool;
 
 #ifdef _WIN32
-typedef signed __int64  sint64;   // compatible with MS VS 6.0
+typedef signed __int64     sint64;   // compatible with MS VS 6.0
 #else
-typedef long long       sint64;
+typedef long long          sint64;
 #endif
 
 static const int   var_Undef = -1;
@@ -132,7 +129,7 @@ struct solver_t
     double   progress_estimate;
     int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
 
-    stats    stats;
+    stats    solver_stats;
 };
 
 #endif
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index fcb1018f..d54a3119 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -123,26 +123,32 @@ void Fraig_ManProveMiter( Fraig_Man_t * p )
 int Fraig_ManCheckMiter( Fraig_Man_t * p )
 {
     Fraig_Node_t * pNode;
+    int i;
     FREE( p->pModel );
-    // get the output node (it can be complemented!)
-    pNode = p->vOutputs->pArray[0];
-    // if the miter is constant 0, the problem is UNSAT
-    if ( pNode == Fraig_Not(p->pConst1) )
-        return 1;
-    // consider the special case when the miter is constant 1
-    if ( pNode == p->pConst1 )
+    for ( i = 0; i < p->vOutputs->nSize; i++ )
     {
-        // in this case, any counter example will do to distinquish it from constant 0
-        // here we pick the counter example composed of all zeros
-        p->pModel = Fraig_ManAllocCounterExample( p );
-        return 0;
+        // get the output node (it can be complemented!)
+        pNode = p->vOutputs->pArray[i];
+        // if the miter is constant 0, the problem is UNSAT
+        if ( pNode == Fraig_Not(p->pConst1) )
+            continue;
+        // consider the special case when the miter is constant 1
+        if ( pNode == p->pConst1 )
+        {
+            // in this case, any counter example will do to distinquish it from constant 0
+            // here we pick the counter example composed of all zeros
+            p->pModel = Fraig_ManAllocCounterExample( p );
+            return 0;
+        }
+        // save the counter example
+        p->pModel = Fraig_ManSaveCounterExample( p, pNode );
+        // if the model is not found, return undecided
+        if ( p->pModel == NULL )
+            return -1;
+        else
+            return 0;
     }
-    // save the counter example
-    p->pModel = Fraig_ManSaveCounterExample( p, pNode );
-    // if the model is not found, return undecided
-    if ( p->pModel == NULL )
-        return -1;
-    return 0;
+    return 1;
 }