Integrating Glucose into bmc3 -g.

8 files changed, 87 insertions, 11 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 994f81f8..bb321175 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1943,6 +1943,10 @@ SOURCE=.\src\sat\bmc\bmcBmcAnd.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcBmcG.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcBmci.c
 # End Source File
 # Begin Source File
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2b5df5cd..6c5e762a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -24739,7 +24739,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Saig_ParBmcSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursvzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -24911,6 +24911,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fUseSatoko ^= 1;
             break;
+        case 'g':
+            pPars->fUseGlucose ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -24977,7 +24980,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdursvzh]\n" );
+    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdursgvzh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking with dynamic unrolling\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n",      pPars->nFramesMax );
@@ -24999,6 +25002,7 @@ usage:
     Abc_Print( -2, "\t-u     : toggle performing structural OR-decomposition [default = %s]\n",   fOrDecomp? "yes": "not" );
     Abc_Print( -2, "\t-r     : toggle disabling periodic restarts [default = %s]\n",              pPars->fNoRestarts? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle using Satoko instead of build-in MiniSAT [default = %s]\n", pPars->fUseSatoko? "yes": "no" );
+    Abc_Print( -2, "\t-g     : toggle using Glucose instead of build-in MiniSAT [default = %s]\n",pPars->fUseGlucose? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n",                           pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n",  pPars->fNotVerbose? "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 06c503ac..2585c773 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -62,6 +62,7 @@ struct Saig_ParBmc_t_
     int         fSkipRand;      // skip random decisions
     int         fNoRestarts;    // disables periodic restarts
     int         fUseSatoko;     // enables using Satoko
+    int         fUseGlucose;    // enables using Glucose 3.0
     int         nLearnedStart;  // starting learned clause limit
     int         nLearnedDelta;  // delta of learned clause limit
     int         nLearnedPerce;  // ratio of learned clause limit
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index f990a982..dd4bf490 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -22,6 +22,7 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
 #include "sat/satoko/satoko.h"
+#include "sat/glucose/AbcGlucose.h"
 #include "misc/vec/vecHsh.h"
 #include "misc/vec/vecWec.h"
 #include "bmc.h"
@@ -62,6 +63,7 @@ struct Gia_ManBmc_t_
     // SAT solver
     sat_solver *      pSat;        // SAT solver
     satoko_t *        pSat2;       // SAT solver
+    bmcg_sat_solver * pSat3;       // SAT solver
     int               nSatVars;    // SAT variables
     int               nObjNums;    // SAT objects
     int               nWordNum;    // unsigned words for ternary simulation
@@ -716,7 +718,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko )
+Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose )
 {
     Gia_ManBmc_t * p;
     Aig_Obj_t * pObj;
@@ -754,6 +756,13 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLi
         satoko_configure(p->pSat2, &opts);
         satoko_setnvars(p->pSat2, 1000);
     }
+    else if ( fUseGlucose )
+    {
+        //opts.conf_limit = nConfLimit;
+        p->pSat3 = bmcg_sat_solver_start();  
+        for ( i = 0; i < 1000; i++ )
+            bmcg_sat_solver_addvar( p->pSat3 );
+    }
     else
     {
         p->pSat  = sat_solver_new();
@@ -797,9 +806,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
             p->pSat ? p->pSat->nLearntDelta     : 0, 
             p->pSat ? p->pSat->nLearntRatio     : 0, 
             p->pSat ? p->pSat->nDBreduces       : 0, 
-            p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2), 
+            p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), 
             nUsedVars, 
-            100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2)) );
+            100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) );
         Abc_Print( 1, "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  UniProps = %d.\n", 
             p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
     }
@@ -820,6 +829,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
     Vec_PtrFreeFree( p->vTerInfo );
     if ( p->pSat )  sat_solver_delete( p->pSat );
     if ( p->pSat2 ) satoko_destroy( p->pSat2 );
+    if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 );
     ABC_FREE( p->pTime4Outs );
     Vec_IntFree( p->vData );
     Hsh_IntManStop( p->vHash );
@@ -1014,6 +1024,11 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
                 if ( !satoko_add_clause( p->pSat2, ClaLits, nClaLits ) )
                     assert( 0 );
             }
+            else if ( p->pSat3 )
+            {
+                if ( !bmcg_sat_solver_addclause( p->pSat3, ClaLits, nClaLits ) )
+                    assert( 0 );
+            }
             else
             {
                 if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
@@ -1267,6 +1282,11 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
     // extend the SAT solver
     if ( p->pSat2 )
         satoko_setnvars( p->pSat2, p->nSatVars );
+    else if ( p->pSat3 )
+    {
+        for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ )
+            bmcg_sat_solver_addvar( p->pSat3 );
+    }
     else
         sat_solver_setnvars( p->pSat, p->nSatVars );
     return Lit;
@@ -1384,6 +1404,11 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
                 if ( iLit != ~0 && satoko_read_cex_varvalue(p->pSat2, lit_var(iLit)) )
                     Abc_InfoSetBit( pCex->pData, iBit + k );
             }
+            else if ( p->pSat3 )
+            {
+                if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) )
+                    Abc_InfoSetBit( pCex->pData, iBit + k );
+            }
             else
             {
                 if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
@@ -1413,6 +1438,11 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit )
         return l_True;
     if ( p->pSat2 )
         return satoko_solve_assumptions_limit( p->pSat2, &Lit, 1, p->pPars->nConfLimit );
+    else if ( p->pSat3 )
+    {
+        bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit );
+        return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 );
+    }
     else
         return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 }
@@ -1450,7 +1480,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
     nTimeToStop   = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
     // create BMC manager
-    p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko );
+    p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose );
     p->pPars = pPars;
     if ( p->pSat )
     {
@@ -1462,6 +1492,11 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
         p->pSat->RunId        = p->pPars->RunId;
         p->pSat->pFuncStop    = p->pPars->pFuncStop;
     }
+    else if ( p->pSat3 )
+    {
+//        satoko_set_runid(p->pSat3, p->pPars->RunId);
+//        satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop);
+    }
     else
     {
         satoko_set_runid(p->pSat2, p->pPars->RunId);
@@ -1483,6 +1518,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     {
         if ( p->pSat2 )
             satoko_set_runtime_limit( p->pSat2, nTimeToStop );
+        else if ( p->pSat3 )
+            bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
         else
             sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     }
@@ -1614,6 +1651,8 @@ clkOther += Abc_Clock() - clk2;
                 clkOne = Abc_Clock();
                 if ( p->pSat2 )
                     satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
+                else if ( p->pSat3 )
+                    bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() );
                 else
                     sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
             }
@@ -1641,6 +1680,8 @@ nTimeUnsat += clkSatRun;
                     Lit = lit_neg( Lit );
                     if ( p->pSat2 )
                         status = satoko_add_clause( p->pSat2, &Lit, 1 );
+                    else if ( p->pSat3 )
+                        status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 );
                     else
                         status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                     assert( status );
@@ -1672,8 +1713,8 @@ nTimeSat += clkSatRun;
                     {
                         Abc_Print( 1, "%4d %s : ", f,  fUnfinished ? "-" : "+" );
                         Abc_Print( 1, "Var =%8.0f. ",  (double)p->nSatVars );
-                        Abc_Print( 1, "Cla =%9.0f. ",  (double)(p->pSat ? p->pSat->stats.clauses   : satoko_clausenum(p->pSat2)) );
-                        Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
+                        Abc_Print( 1, "Cla =%9.0f. ",  (double)(p->pSat ? p->pSat->stats.clauses   : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3)   : satoko_clausenum(p->pSat2)) );
+                        Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
 //                        Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
                         Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
 //                        ABC_PRT( "Time", Abc_Clock() - clk );
@@ -1721,6 +1762,8 @@ nTimeSat += clkSatRun;
                 {
                     if ( p->pSat2 )
                         satoko_set_runtime_limit( p->pSat2, nTimeToStop );
+                    else if ( p->pSat3 )
+                        bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
                     else
                         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
                 }
@@ -1740,6 +1783,11 @@ nTimeSat += clkSatRun;
                         if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
                             continue;
                     }
+                    else if ( p->pSat3 )
+                    {
+                        if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
+                            continue;
+                    }
                     else
                     {
                         if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
@@ -1780,7 +1828,7 @@ nTimeUndec += clkSatRun;
         }
         if ( pPars->fVerbose ) 
         {
-            if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > 1 )
+            if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
             {
                 fFirst = 0;
 //                Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
@@ -1788,8 +1836,8 @@ nTimeUndec += clkSatRun;
             Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
             Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
 //            Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
-            Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses   : satoko_clausenum(p->pSat2)) );
-            Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
+            Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses   : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3)   : satoko_clausenum(p->pSat2))   );
+            Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
 //            Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
             Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
             if ( pPars->fSolveAll )
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index 8825b763..141ecbde 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -188,6 +188,21 @@ void bmcg_sat_solver_setstop(bmcg_sat_solver* s, int * pstop)
     glucose_solver_setstop((Gluco::Solver*)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;
+    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 );
+    else 
+        ((Gluco::Solver*)s)->budgetOff();
+}
+
 int bmcg_sat_solver_varnum(bmcg_sat_solver* s)
 {
     return ((Gluco::Solver*)s)->nVars();
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index 92a6594e..4e3f13a5 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -73,6 +73,8 @@ extern int               bmcg_sat_solver_solve( bmcg_sat_solver* s, int * plits,
 extern int               bmcg_sat_solver_addvar( bmcg_sat_solver* s );
 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);
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index caf33875..a66c323c 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -1250,6 +1250,7 @@ printf("c ==================================[ Search Statistics (every %6d confl
     while (status == l_Undef){
       status = search(0); // the parameter is useless in glucose, kept to allow modifications
         if (!withinBudget() || terminate_search_early || (pstop && *pstop)) break;
+        if (nRuntimeLimit && Abc_Clock() > nRuntimeLimit)                   break;
         curr_restarts++;
     }
 
diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h
index df110f67..dfc8f954 100644
--- a/src/sat/glucose/Solver.h
+++ b/src/sat/glucose/Solver.h
@@ -59,6 +59,7 @@ public:
     int nCallConfl;                      // callback will be called every this number of conflicts
     bool terminate_search_early;         // used to stop the solver early if it as instructed by an external caller
     int * pstop;                         // another callback
+    uint64_t nRuntimeLimit;              // runtime limit
 
     // Problem specification:
     //