Trying to enable CNF simplification in &bmcs -g.

6 files changed, 74 insertions, 42 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6c5e762a..66c0ecca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40017,6 +40017,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fUseSynth     =    0;  // use synthesis
     pPars->fUseOldCnf    =    0;  // use old CNF construction
     pPars->fUseGlucose   =    0;  // use Glucose 3.0
+    pPars->fUseEliminate =    0;  // use variable elimination
     pPars->fVerbose      =    0;  // verbose
     pPars->fVeryVerbose  =    0;  // very verbose
     pPars->fNotVerbose   =    0;  // skip line-by-line print-out
@@ -40026,7 +40027,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncOnFrameDone = pAbc->pFuncOnFrameDone; // frame done callback
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCFATgevwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -40088,6 +40089,9 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'g':
             pPars->fUseGlucose ^= 1;
             break;
+        case 'e':
+            pPars->fUseEliminate ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -40116,7 +40120,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gvwh]\n" );
+    Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gevwh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking\n" );
     Abc_Print( -2, "\t-P num : the number of parallel solvers [default = %d]\n",              pPars->nProcs );
     Abc_Print( -2, "\t-C num : the SAT solver conflict limit [default = %d]\n",               pPars->nConfLimit );
@@ -40124,6 +40128,7 @@ usage:
     Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n",   pPars->nFramesAdd );
     Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n",              pPars->nTimeOut );
     Abc_Print( -2, "\t-g     : toggle using Glucose 3.0 [default = %s]\n",                    pPars->fUseGlucose?  "Glucose" : "Satoko" );
+    Abc_Print( -2, "\t-e     : toggle using variable eliminatation [default = %s]\n",         pPars->fUseEliminate?"yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",         pPars->fVerbose?     "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 2585c773..8e249339 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -95,6 +95,7 @@ struct Bmc_AndPar_t_
     int         fUseSynth;      // use synthesis
     int         fUseOldCnf;     // use old CNF construction
     int         fUseGlucose;    // use Glucose 3.0 as the default solver
+    int         fUseEliminate;  // use variable elimination
     int         fVerbose;       // verbose 
     int         fVeryVerbose;   // very verbose 
     int         fNotVerbose;    // skip line-by-line print-out 
diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c
index 27d6b8d3..3dadfb20 100644
--- a/src/sat/bmc/bmcBmcG.c
+++ b/src/sat/bmc/bmcBmcG.c
@@ -42,7 +42,6 @@ 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               nSatVarsOld;         // number of SAT variables used
     int               fStopNow;            // signal when it is time to stop
     abctime           timeUnf;             // runtime of unfolding
     abctime           timeCnf;             // runtime of CNF generation
@@ -90,7 +89,7 @@ Bmcg_Man_t * Bmcg_ManStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 //        p->pSats[i]->SolverType = i;
         bmcg_sat_solver_addvar( p->pSats[i] );
         bmcg_sat_solver_addclause( p->pSats[i], &Lit, 1 );  
-        bmcg_sat_solver_setstop( p->pSats[i], &p->fStopNow );
+        bmcg_sat_solver_set_stop( p->pSats[i], &p->fStopNow );
     }
     p->nSatVars = 1;
     return p;
@@ -166,7 +165,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 || Gia_ObjIsCi(pObj) )
+    if ( (iSatVar > 0 && !bmcg_sat_solver_var_is_elim(p->pSats[0], iSatVar)) || Gia_ObjIsCi(pObj) )
         iLitClean = Gia_ManAppendCi( p->pClean );
     else if ( Gia_ObjIsAnd(pObj) )
     {
@@ -319,11 +318,12 @@ 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;
-    for ( i = p->nSatVarsOld; i < p->nSatVars; i++ )
-        bmcg_sat_solver_addvar( pSat );
+    bmcg_sat_solver_set_nvars( pSat, p->nSatVars );
     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 );
 }
 int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 {
@@ -345,7 +345,6 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
         }
         nClauses += pCnf->nClauses;
         Bmcg_ManAddCnf( p, p->pSats[0], pCnf );
-        p->nSatVarsOld = p->nSatVars;
         Cnf_DataFree( pCnf );
         assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) );
         for ( k = 0; k < pPars->nFramesAdd; k++ )
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index 141ecbde..caacac10 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -54,19 +54,19 @@ extern "C" {
   SeeAlso     []
 
 ***********************************************************************/
-Gluco::Solver * glucose_solver_start()
+Gluco::SimpSolver * glucose_solver_start()
 {
-    Solver * S = new Solver;
+    SimpSolver * S = new SimpSolver;
     S->setIncrementalMode();
     return S;
 }
 
-void glucose_solver_stop(Gluco::Solver* S)
+void glucose_solver_stop(Gluco::SimpSolver* S)
 {
     delete S;
 }
 
-int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits)
+int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits)
 {
     vec<Lit> lits;
     for ( int i = 0; i < nlits; i++,plits++)
@@ -81,14 +81,14 @@ int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits)
     return S->addClause(lits); // returns 0 if the problem is UNSAT
 }
 
-void glucose_solver_setcallback(Gluco::Solver* S, void * pman, int(*pfunc)(void*, int, int*))
+void glucose_solver_setcallback(Gluco::SimpSolver* S, void * pman, int(*pfunc)(void*, int, int*))
 {
     S->pCnfMan = pman;
     S->pCnfFunc = pfunc;
     S->nCallConfl = 1000;
 }
 
-int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits)
+int glucose_solver_solve(Gluco::SimpSolver* S, int * plits, int nlits)
 {
     vec<Lit> lits;
     for (int i=0;i<nlits;i++,plits++)
@@ -97,22 +97,22 @@ int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits)
         p.x = *plits;
         lits.push(p);
     }
-    Gluco::lbool res = S->solveLimited(lits);
+    Gluco::lbool res = S->solveLimited(lits, 0);
     return (res == l_True ? 1 : res == l_False ? -1 : 0);
 }
 
-int glucose_solver_addvar(Gluco::Solver* S)
+int glucose_solver_addvar(Gluco::SimpSolver* S)
 {
     S->newVar();
     return S->nVars() - 1;
 }
 
-int glucose_solver_read_cex_varvalue(Gluco::Solver* S, int ivar)
+int glucose_solver_read_cex_varvalue(Gluco::SimpSolver* S, int ivar)
 {
     return S->model[ivar] == l_True;
 }
 
-void glucose_solver_setstop(Gluco::Solver* S, int * pstop)
+void glucose_solver_setstop(Gluco::SimpSolver* S, int * pstop)
 {
     S->pstop = pstop;
 }
@@ -155,69 +155,92 @@ bmcg_sat_solver * bmcg_sat_solver_start()
 }
 void bmcg_sat_solver_stop(bmcg_sat_solver* s)
 {
-    glucose_solver_stop((Gluco::Solver*)s);
+    glucose_solver_stop((Gluco::SimpSolver*)s);
 }
 
 int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits)
 {
-    return glucose_solver_addclause((Gluco::Solver*)s,plits,nlits);
+    return glucose_solver_addclause((Gluco::SimpSolver*)s,plits,nlits);
 }
 
 void bmcg_sat_solver_setcallback(bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*))
 {
-    glucose_solver_setcallback((Gluco::Solver*)s,pman,pfunc);
+    glucose_solver_setcallback((Gluco::SimpSolver*)s,pman,pfunc);
 }
 
 int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits)
 {
-    return glucose_solver_solve((Gluco::Solver*)s,plits,nlits);
+    return glucose_solver_solve((Gluco::SimpSolver*)s,plits,nlits);
+}
+
+int bmcg_sat_solver_final(bmcg_sat_solver* s, int ** ppArray)
+{
+    *ppArray = (int *)(Lit *)((Gluco::SimpSolver*)s)->conflict;
+    return ((Gluco::SimpSolver*)s)->conflict.size();
 }
 
 int bmcg_sat_solver_addvar(bmcg_sat_solver* s)
 {
-    return glucose_solver_addvar((Gluco::Solver*)s);
+    return glucose_solver_addvar((Gluco::SimpSolver*)s);
+}
+
+void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars )
+{
+    int i;
+    for ( i = bmcg_sat_solver_varnum(s); i < nvars; i++ )
+        bmcg_sat_solver_addvar(s);
+}
+
+int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim )
+{
+    return ((Gluco::SimpSolver*)s)->eliminate(turn_off_elim != 0);
+}
+
+int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v )
+{
+    return ((Gluco::SimpSolver*)s)->isEliminated(v);
 }
 
 int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
 {
-    return glucose_solver_read_cex_varvalue((Gluco::Solver*)s, ivar);
+    return glucose_solver_read_cex_varvalue((Gluco::SimpSolver*)s, ivar);
 }
 
-void bmcg_sat_solver_setstop(bmcg_sat_solver* s, int * pstop)
+void bmcg_sat_solver_set_stop(bmcg_sat_solver* s, int * pstop)
 {
-    glucose_solver_setstop((Gluco::Solver*)s, pstop);
+    glucose_solver_setstop((Gluco::SimpSolver*)s, pstop);
 }
 
 abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit)
 {
-    abctime nRuntimeLimit = ((Gluco::Solver*)s)->nRuntimeLimit;
-    ((Gluco::Solver*)s)->nRuntimeLimit = Limit;
+    abctime nRuntimeLimit = ((Gluco::SimpSolver*)s)->nRuntimeLimit;
+    ((Gluco::SimpSolver*)s)->nRuntimeLimit = Limit;
     return nRuntimeLimit;
 }
 
 void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit)
 {
     if ( Limit > 0 ) 
-        ((Gluco::Solver*)s)->setConfBudget( (int64_t)Limit );
+        ((Gluco::SimpSolver*)s)->setConfBudget( (int64_t)Limit );
     else 
-        ((Gluco::Solver*)s)->budgetOff();
+        ((Gluco::SimpSolver*)s)->budgetOff();
 }
 
 int bmcg_sat_solver_varnum(bmcg_sat_solver* s)
 {
-    return ((Gluco::Solver*)s)->nVars();
+    return ((Gluco::SimpSolver*)s)->nVars();
 }
 int bmcg_sat_solver_clausenum(bmcg_sat_solver* s)
 {
-    return ((Gluco::Solver*)s)->nClauses();
+    return ((Gluco::SimpSolver*)s)->nClauses();
 }
 int bmcg_sat_solver_learntnum(bmcg_sat_solver* s)
 {
-    return ((Gluco::Solver*)s)->nLearnts();
+    return ((Gluco::SimpSolver*)s)->nLearnts();
 }
 int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s)
 {
-    return ((Gluco::Solver*)s)->conflicts;
+    return ((Gluco::SimpSolver*)s)->conflicts;
 }
 
 /**Function*************************************************************
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index 4e3f13a5..c0078845 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -70,15 +70,19 @@ extern void              bmcg_sat_solver_stop( bmcg_sat_solver* s );
 extern int               bmcg_sat_solver_addclause( bmcg_sat_solver* s, int * plits, int nlits );
 extern void              bmcg_sat_solver_setcallback( bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*) );
 extern int               bmcg_sat_solver_solve( bmcg_sat_solver* s, int * plits, int nlits );
+extern int               bmcg_sat_solver_final( bmcg_sat_solver* s, int ** ppArray );
 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 int               bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int );
-extern void              bmcg_sat_solver_setstop( bmcg_sat_solver* s, int * );
-extern abctime           bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit);
-extern void              bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit);
-extern int               bmcg_sat_solver_varnum(bmcg_sat_solver* s);
-extern int               bmcg_sat_solver_clausenum(bmcg_sat_solver* s);
-extern int               bmcg_sat_solver_learntnum(bmcg_sat_solver* s);
-extern int               bmcg_sat_solver_conflictnum(bmcg_sat_solver* s);
+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 );
+extern void              bmcg_sat_solver_set_conflict_budget( bmcg_sat_solver* s, int Limit );
+extern int               bmcg_sat_solver_varnum( bmcg_sat_solver* s );
+extern int               bmcg_sat_solver_clausenum( bmcg_sat_solver* s );
+extern int               bmcg_sat_solver_learntnum( bmcg_sat_solver* s );
+extern int               bmcg_sat_solver_conflictnum( bmcg_sat_solver* s );
 
 extern void              Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars );
 extern int               Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars );
diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h
index 3f02f13e..0f619b19 100644
--- a/src/sat/glucose/SimpSolver.h
+++ b/src/sat/glucose/SimpSolver.h
@@ -167,7 +167,7 @@ class SimpSolver : public Solver {
 // Implementation of inline methods:
 
 
-inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v] != 0; }
+inline bool SimpSolver::isEliminated (Var v) const { return eliminated.size() ? eliminated[v] != 0 : 0; }
 inline void SimpSolver::updateElimHeap(Var v) {
     assert(use_simplification);
     // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)