SAT solver with dynamic CNF loading.

5 files changed, 135 insertions, 4 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index edf4af1b..76c604bb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -391,6 +391,7 @@ static int Abc_CommandAbc9Cycle              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Cone               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9PoPart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -942,6 +943,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&cone",         Abc_CommandAbc9Cone,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&popart",       Abc_CommandAbc9PoPart,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -31547,6 +31549,90 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_LadPar_t * pPars );
+    int c;
+    Bmc_LadPar_t Pars, * pPars = &Pars;
+    memset( pPars, 0, sizeof(Bmc_LadPar_t) );
+    pPars->nStart        =    0;  // starting timeframe
+    pPars->nFramesMax    =    0;  // maximum number of timeframes 
+    pPars->nConfLimit    =    0;  // maximum number of conflicts at a node
+    pPars->fLoadCnf      =    0;  // dynamic CNF loading
+    pPars->fVerbose      =    0;  // verbose 
+    pPars->fNotVerbose   =    0;  // skip line-by-line print-out 
+    pPars->iFrame        =    0;  // explored up to this frame
+    pPars->nFailOuts     =    0;  // the number of failed outputs
+    pPars->nDropOuts     =    0;  // the number of dropped outputs
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nStart < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesMax < 0 )
+                goto usage;
+            break;
+        case 'c':
+            pPars->fLoadCnf ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Rpm(): There is no AIG.\n" );
+        return 0;
+    }
+    Bmc_PerformBmc( pAbc->pGia, pPars );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &bmc [-SF num] [-cvh]\n" );
+    Abc_Print( -2, "\t         performs bounded model checking\n" );
+    Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n",              pPars->nStart );
+    Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n",    pPars->nFramesMax );
+    Abc_Print( -2, "\t-c     : toggle dynamic CNF loading [default = %s]\n",          pPars->fLoadCnf? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     return -1;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 6e1fd62a..f1407936 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -68,6 +68,20 @@ struct Saig_ParBmc_t_
     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
 };
 
+ 
+typedef struct Bmc_LadPar_t_ Bmc_LadPar_t;
+struct Bmc_LadPar_t_
+{
+    int         nStart;         // starting timeframe
+    int         nFramesMax;     // maximum number of timeframes 
+    int         nConfLimit;     // maximum number of conflicts at a node
+    int         fLoadCnf;       // dynamic CNF loading
+    int         fVerbose;       // verbose 
+    int         fNotVerbose;    // skip line-by-line print-out 
+    int         iFrame;         // explored up to this frame
+    int         nFailOuts;      // the number of failed outputs
+    int         nDropOuts;      // the number of dropped outputs
+};
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 1ac04203..cde439b4 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -6,4 +6,5 @@ SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcCexMin1.c \
     src/sat/bmc/bmcCexMin2.c \
     src/sat/bmc/bmcCexTools.c \
+    src/sat/bmc/bmcLoad.c \
     src/sat/bmc/bmcUnroll.c
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 56bd128c..022a3221 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -399,7 +399,7 @@ static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
 
 /* pre: size > 1 && no variable occurs twice
  */
-static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
+int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
 {
     int fUseBinaryClauses = 1;
     int size;
@@ -478,6 +478,25 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
     if (var_value(s, v) != varX)
         return var_value(s, v) == lit_sign(l);
     else{
+        if ( s->pCnfFunc )
+        {
+            if ( lit_sign(l) )
+            {
+                if ( (s->loads[v] & 1) == 0 )
+                {
+                    s->loads[v] ^= 1;
+                    s->pCnfFunc( s->pCnfMan, l );
+                }
+            }
+            else
+            {
+                if ( (s->loads[v] & 2) == 0 )
+                {
+                    s->loads[v] ^= 2;
+                    s->pCnfFunc( s->pCnfMan, l );
+                }
+            }
+        }
         // New fact -- store it.
 #ifdef VERBOSEDEBUG
         printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
@@ -561,7 +580,7 @@ static void sat_solver_record(sat_solver* s, veci* cls)
 {
     lit*    begin = veci_begin(cls);
     lit*    end   = begin + veci_size(cls);
-    int     h     = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
+    int     h     = (veci_size(cls) > 1) ? sat_solver_clause_new(s,begin,end,1) : 0;
     sat_solver_enqueue(s,*begin,h);
     assert(veci_size(cls) > 0);
     if ( h == 0 )
@@ -1026,6 +1045,8 @@ void sat_solver_setnvars(sat_solver* s,int n)
     if (s->cap < n){
         int old_cap = s->cap;
         while (s->cap < n) s->cap = s->cap*2+1;
+        if ( s->cap < 50000 )
+            s->cap = 50000;
 
         s->wlists    = ABC_REALLOC(veci,   s->wlists,   s->cap*2);
 //        s->vi        = ABC_REALLOC(varinfo,s->vi,       s->cap);
@@ -1033,6 +1054,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->assigns   = ABC_REALLOC(char,   s->assigns,  s->cap);
         s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
         s->tags      = ABC_REALLOC(char,   s->tags,     s->cap);
+        s->loads     = ABC_REALLOC(char,   s->loads,    s->cap);
 #ifdef USE_FLOAT_ACTIVITY
         s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
 #else
@@ -1070,6 +1092,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->assigns [var] = varX;
         s->polarity[var] = 0;
         s->tags    [var] = 0;
+        s->loads   [var] = 0;
         s->orderpos[var] = veci_size(&s->order);
         s->reasons [var] = 0;
         s->model   [var] = 0; 
@@ -1113,6 +1136,7 @@ void sat_solver_delete(sat_solver* s)
         ABC_FREE(s->assigns  );
         ABC_FREE(s->polarity );
         ABC_FREE(s->tags     );
+        ABC_FREE(s->loads    );
         ABC_FREE(s->activity );
         ABC_FREE(s->activity2);
         ABC_FREE(s->pFreqs   );
@@ -1188,6 +1212,7 @@ double sat_solver_memory( sat_solver* s )
     Mem += s->cap * sizeof(char);     // ABC_FREE(s->assigns  );
     Mem += s->cap * sizeof(char);     // ABC_FREE(s->polarity );
     Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     );
+    Mem += s->cap * sizeof(char);     // ABC_FREE(s->loads    );
 #ifdef USE_FLOAT_ACTIVITY
     Mem += s->cap * sizeof(double);   // ABC_FREE(s->activity );
 #else
@@ -1484,11 +1509,10 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
         return sat_solver_enqueue(s,*begin,0);
 
     // create new clause
-    clause_create_new(s,begin,j,0);
+    sat_solver_clause_new(s,begin,j,0);
     return true;
 }
 
-
 double luby(double y, int x)
 {
     int size, seq;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 50a4727c..81202179 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -45,6 +45,7 @@ extern sat_solver* sat_solver_new(void);
 extern void        sat_solver_delete(sat_solver* s);
 
 extern int         sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern int         sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt);
 extern int         sat_solver_simplify(sat_solver* s);
 extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 extern void        sat_solver_restart( sat_solver* s );
@@ -129,6 +130,7 @@ struct sat_solver_t
     char*       assigns;       // Current values of variables.
     char*       polarity;      //
     char*       tags;          //
+    char*       loads;         //
 
     int*        orderpos;      // Index in variable order.
     int*        reasons;       //
@@ -183,6 +185,10 @@ struct sat_solver_t
     int         nRoots;
 
     veci        temp_clause;    // temporary storage for a CNF clause
+
+    // CNF loading
+    void *      pCnfMan;           // external CNF manager
+    int(*pCnfFunc)(void * p, int); // external callback
 };
 
 static inline clause * clause_read( sat_solver * s, cla h )