Enabling variable elim in &bmcs -g.

5 files changed, 77 insertions, 14 deletions

diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c
index 8fef2ef6..af141d30 100644
--- a/src/sat/bmc/bmcBmcG.c
+++ b/src/sat/bmc/bmcBmcG.c
@@ -42,9 +42,12 @@ struct Bmcg_Man_t_
     Vec_Int_t         vCiMap;              // maps CIs of pFrames into CIs/frames of GIA
     bmcg_sat_solver * pSats[PAR_THR_MAX];  // concurrent SAT solvers
     int               nSatVars;            // number of SAT variables used
+    int               nOldFrPis;           // number of primary inputs
+    int               nOldFrPos;           // number of primary output
     int               fStopNow;            // signal when it is time to stop
     abctime           timeUnf;             // runtime of unfolding
     abctime           timeCnf;             // runtime of CNF generation
+    abctime           timeSmp;             // runtime of CNF simplification
     abctime           timeSat;             // runtime of the solvers
     abctime           timeOth;             // other runtime
 };
@@ -165,7 +168,7 @@ int Bmcg_ManCollect_rec( Bmcg_Man_t * p, int iObj )
         return iLitClean;
     pObj = Gia_ManObj( p->pFrames, iObj );
     iSatVar = Vec_IntEntry( &p->vFr2Sat, iObj );
-    if ( (iSatVar > 0 && !bmcg_sat_solver_var_is_elim(p->pSats[0], iSatVar)) || Gia_ObjIsCi(pObj) )
+    if ( iSatVar > 0 || Gia_ObjIsCi(pObj) )
         iLitClean = Gia_ManAppendCi( p->pClean );
     else if ( Gia_ObjIsAnd(pObj) )
     {
@@ -277,7 +280,7 @@ void Bmcg_ManPrintFrame( Bmcg_Man_t * p, int f, int nClauses, int Solver, abctim
     Abc_Print( 1, "%4d %s : ", f,   fUnfinished ? "-" : "+" );
 //    Abc_Print( 1, "Var =%8.0f.  ",  (double)p->nSatVars ); 
 //    Abc_Print( 1, "Cla =%9.0f.  ",  (double)nClauses );  
-    Abc_Print( 1, "Var =%8.0f.  ",  (double)bmcg_sat_solver_varnum(p->pSats[0]) ); 
+    Abc_Print( 1, "Var =%8.0f.  ",  (double)(bmcg_sat_solver_varnum(p->pSats[0])-bmcg_sat_solver_elim_varnum(p->pSats[0])) ); 
     Abc_Print( 1, "Cla =%9.0f.  ",  (double)bmcg_sat_solver_clausenum(p->pSats[0]) );  
     Abc_Print( 1, "Learn =%9.0f.  ",(double)bmcg_sat_solver_learntnum(p->pSats[0]) );  
     Abc_Print( 1, "Conf =%9.0f.  ", (double)bmcg_sat_solver_conflictnum(p->pSats[0]) );  
@@ -290,11 +293,12 @@ void Bmcg_ManPrintFrame( Bmcg_Man_t * p, int f, int nClauses, int Solver, abctim
 }
 void Bmcg_ManPrintTime( Bmcg_Man_t * p )
 {
-    abctime clkTotal = p->timeUnf + p->timeCnf + p->timeSat + p->timeOth;
+    abctime clkTotal = p->timeUnf + p->timeCnf + p->timeSmp + p->timeSat + p->timeOth;
     if ( !p->pPars->fVerbose )
         return;
     ABC_PRTP( "Unfolding     ", p->timeUnf,  clkTotal );
     ABC_PRTP( "CNF generation", p->timeCnf,  clkTotal );
+    ABC_PRTP( "CNF simplify  ", p->timeSmp,  clkTotal );
     ABC_PRTP( "SAT solving   ", p->timeSat,  clkTotal );
     ABC_PRTP( "Other         ", p->timeOth,  clkTotal );
     ABC_PRTP( "TOTAL         ", clkTotal  ,  clkTotal );
@@ -317,13 +321,38 @@ Abc_Cex_t * Bmcg_ManGenerateCex( Bmcg_Man_t * p, int i, int f, int s )
 }
 void Bmcg_ManAddCnf( Bmcg_Man_t * p, bmcg_sat_solver * pSat, Cnf_Dat_t * pCnf )
 {
-    int i;
+    int i, iSatVar;
+    abctime clk = Abc_Clock();
     bmcg_sat_solver_set_nvars( pSat, p->nSatVars );
+    if ( p->pPars->fUseEliminate )
+    {
+        for ( i = p->nOldFrPis; i < Gia_ManPiNum(p->pFrames); i++ )
+        {
+            Gia_Obj_t * pObj = Gia_ManPi( p->pFrames, i );
+            int iSatVar = Vec_IntEntry( &p->vFr2Sat, Gia_ObjId(p->pFrames, pObj) );
+            if ( iSatVar > 0 )
+                bmcg_sat_solver_var_set_frozen( pSat, iSatVar, 1 );
+        }
+        for ( i = p->nOldFrPos; i < Gia_ManPoNum(p->pFrames); i++ )
+        {
+            Gia_Obj_t * pObj = Gia_ManPo( p->pFrames, i );
+            int iSatVar = Vec_IntEntry( &p->vFr2Sat, Gia_ObjId(p->pFrames, pObj) );
+            if ( iSatVar > 0 )
+                bmcg_sat_solver_var_set_frozen( pSat, iSatVar, 1 );
+        }
+        p->nOldFrPis = Gia_ManPiNum(p->pFrames);
+        p->nOldFrPos = Gia_ManPoNum(p->pFrames);
+    }
     for ( i = 0; i < pCnf->nClauses; i++ )
         if ( !bmcg_sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
             assert( 0 );
-    if ( p->pPars->fUseEliminate )
-        bmcg_sat_solver_eliminate( pSat, 0 );
+    if ( !p->pPars->fUseEliminate )
+        return;
+    bmcg_sat_solver_eliminate( pSat, 0 );
+    Vec_IntForEachEntry( &p->vFr2Sat, iSatVar, i )
+        if ( iSatVar > 0 && bmcg_sat_solver_var_is_elim(pSat, iSatVar) )
+            Vec_IntWriteEntry( &p->vFr2Sat, i, -1 );
+    p->timeSmp += Abc_Clock() - clk;
 }
 int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
@@ -391,7 +420,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
         if ( k < pPars->nFramesAdd )
             break;
     }
-    p->timeOth = Abc_Clock() - clkStart - p->timeUnf - p->timeCnf - p->timeSat;
+    p->timeOth = Abc_Clock() - clkStart - p->timeUnf - p->timeCnf - p->timeSmp - p->timeSat;
     if ( RetValue == -1 && !pPars->fNotVerbose )
         printf( "No output failed in %d frames.  ", f + (k < pPars->nFramesAdd ? k+1 : 0) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
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: