Adding an option to bmc3 to use Satoko intead of the default SAT solver.

5 files changed, 130 insertions, 49 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a841b5f9..6ef02a06 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -24728,7 +24728,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, "SFTHGCDJIPQRLWaxdurvzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursvzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -24897,6 +24897,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             pPars->fNoRestarts ^= 1;
             break;
+        case 's':
+            pPars->fUseSatoko ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -24963,7 +24966,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdurvzh]\n" );
+    Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdursvzh]\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 );
@@ -24984,6 +24987,7 @@ usage:
     Abc_Print( -2, "\t-d     : toggle dropping (replacing by 0) SAT outputs [default = %s]\n",    pPars->fDropSatOuts? "yes": "no" );
     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-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 0eac7fb0..bdb89684 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -61,6 +61,7 @@ struct Saig_ParBmc_t_
     int         nFfToAddMax;    // max number of flops to add during CBA
     int         fSkipRand;      // skip random decisions
     int         fNoRestarts;    // disables periodic restarts
+    int         fUseSatoko;     // enables using Satoko
     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 a1011ae1..36c60b36 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -21,6 +21,8 @@
 #include "proof/fra/fra.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
+#include "sat/satoko/satoko.h"
+#include "sat/satoko/solver.h"
 #include "misc/vec/vecHsh.h"
 #include "misc/vec/vecWec.h"
 #include "bmc.h"
@@ -60,6 +62,7 @@ struct Gia_ManBmc_t_
     int               nLitUseless; // useless literals
     // SAT solver
     sat_solver *      pSat;        // SAT solver
+    satoko_t *        pSat2;       // SAT solver
     int               nSatVars;    // SAT variables
     int               nObjNums;    // SAT objects
     int               nWordNum;    // unsigned words for ternary simulation
@@ -714,7 +717,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 )
+Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko )
 {
     Gia_ManBmc_t * p;
     Aig_Obj_t * pObj;
@@ -743,8 +746,21 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne )
     p->vVisited = Vec_WecAlloc( 100 );
     // create solver
     p->nSatVars = 1;
-    p->pSat     = sat_solver_new();
-    sat_solver_setnvars( p->pSat, 1000 );
+    if ( fUseSatoko )
+    {
+        satoko_opts_t opts;
+        satoko_default_opts(&opts);
+        opts.conf_limit = nConfLimit;
+        p->pSat2 = satoko_create();  
+        satoko_configure(p->pSat2, &opts);
+        for ( i = 0; i < 1000; i++ )
+            satoko_add_variable( p->pSat2, 0 );
+    }
+    else
+    {
+        p->pSat  = sat_solver_new();
+        sat_solver_setnvars( p->pSat, 1000 );
+    }
     Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
     // terminary simulation 
     p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
@@ -777,10 +793,15 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
 {
     if ( p->pPars->fVerbose )
     {
-        int nUsedVars = sat_solver_count_usedvars(p->pSat);
+        int nUsedVars = p->pSat ? sat_solver_count_usedvars(p->pSat) : 0;
         Abc_Print( 1, "LStart(P) = %d  LDelta(Q) = %d  LRatio(R) = %d  ReduceDB = %d  Vars = %d  Used = %d (%.2f %%)\n", 
-            p->pSat->nLearntStart, p->pSat->nLearntDelta, p->pSat->nLearntRatio, 
-            p->pSat->nDBreduces, p->pSat->size, nUsedVars, 100.0*nUsedVars/p->pSat->size );
+            p->pSat ? p->pSat->nLearntStart     : 0, 
+            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) : solver_varnum(p->pSat2), 
+            nUsedVars, 
+            100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : solver_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 );
     }
@@ -799,7 +820,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
     Vec_IntFree( p->vId2Num );
     Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
     Vec_PtrFreeFree( p->vTerInfo );
-    sat_solver_delete( p->pSat );
+    if ( p->pSat )  sat_solver_delete( p->pSat );
+    if ( p->pSat2 ) satoko_destroy( p->pSat2 );
     ABC_FREE( p->pTime4Outs );
     Vec_IntFree( p->vData );
     Hsh_IntManStop( p->vHash );
@@ -989,8 +1011,16 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
                 }
                 CutLit = CutLit / 3;
             }
-            if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
-                assert( 0 );
+            if ( p->pSat2 )
+            {
+                if ( !satoko_add_clause( p->pSat2, ClaLits, nClaLits ) )
+                    assert( 0 );
+            }
+            else
+            {
+                if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
+                    assert( 0 );
+            }
         }
     }
 }
@@ -1237,8 +1267,16 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
             Saig_ManBmcCreateCnf_rec( p, pTemp, iFrame-f );
     Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
     // extend the SAT solver
-    if ( p->nSatVars > sat_solver_nvars(p->pSat) )
-        sat_solver_setnvars( p->pSat, p->nSatVars );
+    if ( p->pSat2 )
+    {
+        for ( i = solver_varnum(p->pSat2); i < p->nSatVars; i++ )
+            satoko_add_variable( p->pSat2, 0 );
+    }
+    else
+    {
+        if ( p->nSatVars > sat_solver_nvars(p->pSat) )
+            sat_solver_setnvars( p->pSat, p->nSatVars );
+    }
     return Lit;
 }
 
@@ -1349,8 +1387,16 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
         Saig_ManForEachPi( p->pAig, pObjPi, k )
         {
             int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
-            if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
-                Abc_InfoSetBit( pCex->pData, iBit + k );
+            if ( p->pSat2 )
+            {
+                if ( iLit != ~0 && var_polarity(p->pSat2, lit_var(iLit)) == LIT_TRUE )
+                    Abc_InfoSetBit( pCex->pData, iBit + k );
+            }
+            else
+            {
+                if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
+                    Abc_InfoSetBit( pCex->pData, iBit + k );
+            }
         }
     return pCex;
 }
@@ -1373,7 +1419,20 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit )
         return l_False;
     if ( Lit == 1 )
         return l_True;
-    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 );
+    if ( p->pSat2 )
+    {
+        int status;
+        satoko_assump_push( p->pSat2, Lit );
+        status = satoko_solve( p->pSat2 );
+        satoko_assump_pop( p->pSat2 );
+        if ( status == SATOKO_UNSAT )
+            return l_False;
+        if ( status == SATOKO_SAT )
+            return l_True;
+        return l_Undef;
+    }
+    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 );
 }
 
 /**Function*************************************************************
@@ -1409,15 +1468,18 @@ 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 );
+    p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko );
     p->pPars = pPars;
-    p->pSat->nLearntStart = p->pPars->nLearnedStart;
-    p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
-    p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
-    p->pSat->nLearntMax   = p->pSat->nLearntStart;
-    p->pSat->fNoRestarts  = p->pPars->fNoRestarts;
-    p->pSat->RunId        = p->pPars->RunId;
-    p->pSat->pFuncStop    = p->pPars->pFuncStop;
+    if ( p->pSat )
+    {
+        p->pSat->nLearntStart = p->pPars->nLearnedStart;
+        p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
+        p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
+        p->pSat->nLearntMax   = p->pSat->nLearntStart;
+        p->pSat->fNoRestarts  = p->pPars->fNoRestarts;
+        p->pSat->RunId        = p->pPars->RunId;
+        p->pSat->pFuncStop    = p->pPars->pFuncStop;
+    }
     if ( pPars->fSolveAll && p->vCexes == NULL )
         p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
     if ( pPars->fVerbose )
@@ -1430,7 +1492,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     } 
     pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
     // set runtime limit
-    if ( nTimeToStop )
+    if ( nTimeToStop && p->pSat )
         sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
     // perform frames
     Aig_ManRandom( 1 );
@@ -1553,7 +1615,7 @@ clk2 = Abc_Clock();
 clkOther += Abc_Clock() - clk2;
             // solve this output
             fUnfinished = 0;
-            sat_solver_compress( p->pSat );
+            if ( p->pSat ) sat_solver_compress( p->pSat );
             if ( p->pTime4Outs )
             {
                 assert( p->pTime4Outs[i] > 0 );
@@ -1582,18 +1644,24 @@ nTimeUnsat += clkSatRun;
                 {
                     // add final unit clause
                     Lit = lit_neg( Lit );
-                    status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+                    if ( p->pSat2 )
+                        status = satoko_add_clause( p->pSat2, &Lit, 1 );
+                    else
+                        status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
                     assert( status );
                     // add learned units
-                    for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
+                    if ( p->pSat )
                     {
-                        Lit = veci_begin(&p->pSat->unit_lits)[k];
-                        status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-                        assert( status );
+                        for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
+                        {
+                            Lit = veci_begin(&p->pSat->unit_lits)[k];
+                            status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+                            assert( status );
+                        }
+                        veci_resize(&p->pSat->unit_lits, 0);
+                        // propagate units
+                        sat_solver_compress( p->pSat );
                     }
-                    veci_resize(&p->pSat->unit_lits, 0);
-                    // propagate units
-                    sat_solver_compress( p->pSat );
                 }
                 if ( p->pPars->fUseBridge )
                     Gia_ManReportProgress( stdout, i, f );
@@ -1609,13 +1677,13 @@ 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->stats.clauses );
-                        Abc_Print( 1, "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
+                        Abc_Print( 1, "Cla =%9.0f. ",  (double)(p->pSat ? p->pSat->stats.clauses   : vec_uint_size(p->pSat2->originals)) );
+                        Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : satoko_stats(p->pSat2).n_conflicts) );
 //                        Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
-                        Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
+                        Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
 //                        ABC_PRT( "Time", Abc_Clock() - clk );
                         Abc_Print( 1, "%4.0f MB",      4.25*(f+1)*p->nObjNums /(1<<20) );
-                        Abc_Print( 1, "%4.0f MB",      1.0*sat_solver_memory(p->pSat)/(1<<20) );
+                        Abc_Print( 1, "%4.0f MB",      1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
                         Abc_Print( 1, "%9.2f sec  ",   (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
 //                        Abc_Print( 1, "\n" );
 //                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
@@ -1654,7 +1722,7 @@ nTimeSat += clkSatRun;
                 // reset the timeout
                 pPars->timeLastSolved = Abc_Clock();
                 nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
-                if ( nTimeToStop )
+                if ( nTimeToStop && p->pSat )
                     sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
 
                 // check if other outputs failed under the same counter-example
@@ -1667,8 +1735,16 @@ nTimeSat += clkSatRun;
                         continue;
                     // check if this output is solved
                     Lit = Saig_ManBmcCreateCnf( p, pObj, f );
-                    if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
-                        continue;
+                    if ( p->pSat2 )
+                    {
+                        if ( (var_polarity(p->pSat2, lit_var(Lit)) == LIT_TRUE) == Abc_LitIsCompl(Lit) )
+                            continue;
+                    }
+                    else
+                    {
+                        if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
+                            continue;
+                    }
                     // write entry
                     pPars->nFailOuts++;
                     if ( !pPars->fNotVerbose )
@@ -1704,7 +1780,7 @@ nTimeUndec += clkSatRun;
         }
         if ( pPars->fVerbose ) 
         {
-            if ( fFirst == 1 && f > 0 && p->pSat->stats.conflicts > 1 )
+            if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : 0) > 1 )
             {
                 fFirst = 0;
 //                Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
@@ -1712,10 +1788,10 @@ 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->stats.clauses );
-            Abc_Print( 1, "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
+            Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses   : vec_uint_size(p->pSat2->originals)) );
+            Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : satoko_stats(p->pSat2).n_conflicts) );
 //            Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
-            Abc_Print( 1, "Uni =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
+            Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
             if ( pPars->fSolveAll )
                 Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
             if ( pPars->nTimeOutOne )
@@ -1723,9 +1799,9 @@ nTimeUndec += clkSatRun;
 //            ABC_PRT( "Time", Abc_Clock() - clk );
 //            Abc_Print( 1, "%4.0f MB",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
             Abc_Print( 1, "%4.0f MB",     4.0*(f+1)*p->nObjNums /(1<<20) );
-            Abc_Print( 1, "%4.0f MB",     1.0*sat_solver_memory(p->pSat)/(1<<20) );
+            Abc_Print( 1, "%4.0f MB",     1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
 //            Abc_Print( 1, " %6d %6d ",   p->nLitUsed, p->nLitUseless );
-            Abc_Print( 1, "%9.2f sec ",  1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
+            Abc_Print( 1, "%9.2f sec ",   1.0*(Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
 //            Abc_Print( 1, "\n" );
 //            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
 //            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index 3a6afa20..d2ed3b75 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -146,7 +146,7 @@ static inline void     clause_set_id( clause * c, int id )          { c->lits[c-
 static inline int      clause_size( clause * c )                    { return c->size;                              }
 static inline lit *    clause_begin( clause * c )                   { return c->lits;                              }
 static inline lit *    clause_end( clause * c )                     { return c->lits + c->size;                    }
-static inline void     clause_print( clause * c )               
+static inline void     clause_print_( clause * c )               
 { 
     int i;
     printf( "{ " );
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 7a4470f1..0d17766c 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1783,7 +1783,7 @@ void sat_solver2_verify( sat_solver2* s )
         if ( k == (int)c->size )
         {
             Abc_Print(1, "Clause %d is not satisfied.   ", c->Id );
-            clause_print( c );
+            clause_print_( c );
             sat_solver2_find_clause( s, clause_handle(&s->clauses, c), 1 );
             Counter++;
         }