From 7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 26 Sep 2007 08:01:00 -0700
Subject: Version abc70926

---
 src/sat/bsat/satSolver.c | 18 +++++++++++-------
 src/sat/bsat/satSolver.h |  2 ++
 src/sat/bsat/satUtil.c   | 12 +++++++-----
 3 files changed, 20 insertions(+), 12 deletions(-)

(limited to 'src/sat')

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 512c5751..439d9e76 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -90,9 +90,9 @@ static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[
 //=================================================================================================
 // Encode literals in clause pointers:
 
-static clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
-static bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);                              }
-static lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1);                        }
+static inline clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
+static inline bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);                              }
+static inline lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1);                        }
 
 //=================================================================================================
 // Simple helpers:
@@ -148,7 +148,7 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder
     }
 }
 
-static int  order_select(sat_solver* s, float random_var_freq) // selectvar
+static inline int  order_select(sat_solver* s, float random_var_freq) // selectvar
 {
     int*    heap;
     double* activity;
@@ -442,7 +442,7 @@ static inline void assume(sat_solver* s, lit l){
 }
 
 
-static inline void sat_solver_canceluntil(sat_solver* s, int level) {
+static void sat_solver_canceluntil(sat_solver* s, int level) {
     lit*     trail;   
     lbool*   values;  
     clause** reasons; 
@@ -723,13 +723,14 @@ clause* sat_solver_propagate(sat_solver* s)
         //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
         for (i = j = begin; i < end; ){
             if (clause_is_lit(*i)){
+//                s->stats.inspects2++;
                 *j++ = *i;
                 if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
                     confl = s->binary;
                     (clause_begin(confl))[1] = lit_neg(p);
                     (clause_begin(confl))[0] = clause_read_lit(*i++);
-
                     // Copy the remaining watches:
+//                    s->stats.inspects2 += end - i;
                     while (i < end)
                         *j++ = *i++;
                 }
@@ -770,6 +771,7 @@ clause* sat_solver_propagate(sat_solver* s)
                     if (!enqueue(s,lits[0], *i)){
                         confl = *i++;
                         // Copy the remaining watches:
+//                        s->stats.inspects2 += end - i;
                         while (i < end)
                             *j++ = *i++;
                     }
@@ -1154,6 +1156,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
     lit*    i;
 
     // set the external limits
+    s->nCalls++;
     s->nRestarts  = 0;
     s->nConfLimit = 0;
     s->nInsLimit  = 0;
@@ -1175,12 +1178,13 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
             assume(s, *i);
             if (sat_solver_propagate(s) == NULL)
                 break;
-            // falltrough
+            // fallthrough
         case -1: /* l_False */
             sat_solver_canceluntil(s, 0);
             return l_False;
         }
     }
+    s->nCalls2++;
 
     s->root_level = sat_solver_dlevel(s);
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index f5424c85..542b9895 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -172,6 +172,8 @@ struct sat_solver_t
     veci     act_vars;      // variables whose activity has changed
     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
  
     Sat_MmStep_t * pMem;
 
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 3001957f..62f3c208 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -146,11 +146,13 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
 ***********************************************************************/
 void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 {
-    printf( "starts        : %d\n", (int)p->stats.starts );
-    printf( "conflicts     : %d\n", (int)p->stats.conflicts );
-    printf( "decisions     : %d\n", (int)p->stats.decisions );
-    printf( "propagations  : %d\n", (int)p->stats.propagations );
-    printf( "inspects      : %d\n", (int)p->stats.inspects );
+//    printf( "calls         : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
+    printf( "starts        : %8d\n", (int)p->stats.starts );
+    printf( "conflicts     : %8d\n", (int)p->stats.conflicts );
+    printf( "decisions     : %8d\n", (int)p->stats.decisions );
+    printf( "propagations  : %8d\n", (int)p->stats.propagations );
+    printf( "inspects      : %8d\n", (int)p->stats.inspects );
+//    printf( "inspects2     : %8d\n", (int)p->stats.inspects2 );
 }
 
 /**Function*************************************************************
-- 
cgit v1.2.3