SAT variable profiling.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index acaceef9..e5ea1ba5 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -121,6 +121,8 @@ struct sat_solver_t
     unsigned*   activity;      // A heuristic measurement of the activity of a variable.
     unsigned*   activity2;     // backup variable activity
 #endif
+    char *      pFreqs;        // how many times this variable was assigned a value
+    int         nVarUsed;
 
 //    varinfo *   vi;            // variable information
     int*        levels;        //
@@ -248,6 +250,18 @@ static inline void sat_solver_bookmark(sat_solver* s)
     }
 }
 
+static inline int sat_solver_count_usedvars(sat_solver* s)
+{
+    int i, nVars = 0;
+    for ( i = 0; i < s->size; i++ )
+        if ( s->pFreqs[i] )
+        {
+            s->pFreqs[i] = 0;
+            nVars++;
+        }
+    return nVars;
+}
+
 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
 {
     lit Lits[1];