Enabling variable elim in &bmcs -g.

4 files changed, 41 insertions, 7 deletions

diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index f4bc41b7..064c723e 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -40,7 +40,7 @@ extern "C" {
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-//#define USE_SIMP_SOLVER 1
+#define USE_SIMP_SOLVER 1
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -188,6 +188,17 @@ int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v )
     return ((Gluco::SimpSolver*)s)->isEliminated(v);
 }
 
+void bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze )
+{
+    ((Gluco::SimpSolver*)s)->setFrozen(v, freeze != 0);
+}
+
+int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s)
+{
+//    return 0; 
+    return ((Gluco::SimpSolver*)s)->eliminated_vars;
+}
+
 int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
 {
     return glucose_solver_read_cex_varvalue((Gluco::SimpSolver*)s, ivar);
@@ -407,13 +418,24 @@ void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars )
 int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim )
 {
     return 1; 
-//    return ((Gluco::Solver*)s)->eliminate(turn_off_elim != 0);
+//    return ((Gluco::SimpSolver*)s)->eliminate(turn_off_elim != 0);
 }
 
 int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v )
 {
     return 0; 
-//    return ((Gluco::Solver*)s)->isEliminated(v);
+//    return ((Gluco::SimpSolver*)s)->isEliminated(v);
+}
+
+void bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze )
+{
+//    ((Gluco::SimpSolver*)s)->setFrozen(v, freeze);
+}
+
+int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s)
+{
+    return 0;
+//    return ((Gluco::SimpSolver*)s)->eliminated_vars;
 }
 
 int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
@@ -618,7 +640,12 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
         printf("c |  Number of clauses:    %12d                                         |\n", S.nClauses());
     }
     
-    if ( pPars->pre ) S.eliminate(true);
+    if ( pPars->pre ) 
+    {
+        S.eliminate(true);
+        printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
 
     vec<Lit> dummy;
     lbool ret = S.solveLimited(dummy, 0);
@@ -773,7 +800,11 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
     }
 
     if (pPars->pre) 
+    {
         S.eliminate(true);
+        printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
     
     vec<Lit> dummy;
     lbool ret = S.solveLimited(dummy, 0);
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index c0078845..e36b7a24 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -75,6 +75,8 @@ extern int               bmcg_sat_solver_addvar( bmcg_sat_solver* s );
 extern void              bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars );
 extern int               bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim );
 extern int               bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v );
+extern void              bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze );
+extern int               bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s);
 extern int               bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int );
 extern void              bmcg_sat_solver_set_stop( bmcg_sat_solver* s, int * pstop );
 extern abctime           bmcg_sat_solver_set_runtime_limit( bmcg_sat_solver* s, abctime Limit );
diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp
index 43d98146..0c6639fb 100644
--- a/src/sat/glucose/SimpSolver.cpp
+++ b/src/sat/glucose/SimpSolver.cpp
@@ -54,6 +54,7 @@ SimpSolver::SimpSolver() :
   , merges             (0)
   , asymm_lits         (0)
   , eliminated_vars    (0)
+  , eliminated_clauses (0)
   , elimorder          (1)
   , use_simplification (true)
   , occurs             (ClauseDeleted(ca))
@@ -523,10 +524,12 @@ bool SimpSolver::eliminateVar(Var v)
         for (i = 0; i < neg.size(); i++)
             mkElimClause(elimclauses, v, ca[neg[i]]);
         mkElimClause(elimclauses, mkLit(v));
+        eliminated_clauses += neg.size();
     }else{
         for (i = 0; i < pos.size(); i++)
             mkElimClause(elimclauses, v, ca[pos[i]]);
         mkElimClause(elimclauses, ~mkLit(v));
+        eliminated_clauses += pos.size();
     }
 
 
@@ -690,9 +693,6 @@ bool SimpSolver::eliminate(bool turn_off_elim)
     if (verbosity >= 1 && elimclauses.size() > 0)
         printf("c |  Eliminated clauses:     %10.2f Mb                                                                |\n", 
                double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
-
-    printf( "c Simplication removed %d variables and %d clauses.  ", eliminated_vars, elimclauses.size() );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return ok;
 }
 
diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h
index 260ab5e3..520a5cc9 100644
--- a/src/sat/glucose/SimpSolver.h
+++ b/src/sat/glucose/SimpSolver.h
@@ -97,6 +97,7 @@ class SimpSolver : public Solver {
     int     merges;
     int     asymm_lits;
     int     eliminated_vars;
+    int     eliminated_clauses;
 
  protected: