Integrating new CNF generation into &bmc.

src/base/abci/abc.c

@@ -37132,10 +37132,11 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFramesAdd    =   50;  // the number of additional frames
     pPars->nConfLimit    =    0;  // maximum number of conflicts at a node
     pPars->nTimeOut      =    0;  // timeout in seconds
+    pPars->nLutSize      =    6;  // max LUT size for CNF computation
     pPars->fLoadCnf      =    0;  // dynamic CNF loading
     pPars->fDumpFrames   =    0;  // dump unrolled timeframes
     pPars->fUseSynth     =    0;  // use synthesis
-    pPars->fUseOldCnf    =    1;  // use old CNF construction
+    pPars->fUseOldCnf    =    0;  // use old CNF construction
     pPars->fVerbose      =    0;  // verbose 
     pPars->fVeryVerbose  =    0;  // very verbose 
     pPars->fNotVerbose   =    0;  // skip line-by-line print-out 
@@ -37143,7 +37144,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFailOuts     =    0;  // the number of failed outputs
     pPars->nDropOuts     =    0;  // the number of dropped outputs
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFATdscvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFATKdscvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -37191,6 +37192,17 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOut < 0 )
                 goto usage;
             break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLutSize < 0 )
+                goto usage;
+            break;
         case 'd':
             pPars->fDumpFrames ^= 1;
             break;
@@ -37217,23 +37229,19 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Bmc(): There is no AIG.\n" );
         return 0;
     }
-    if ( !pPars->fUseOldCnf && !Sdm_ManCanRead() )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Bmc(): Cannot input precomputed DSD information.\n" );
-        return 0;
-    }
     pAbc->Status  = Gia_ManBmcPerform( pAbc->pGia, pPars );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmc [-SFAT num] [-dscvwh]\n" );
+    Abc_Print( -2, "usage: &bmc [-SFATK num] [-dscvwh]\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-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-K num : the maximum cut size for CNF computation [default = %d]\n",    pPars->nLutSize );
     Abc_Print( -2, "\t-d     : toggle dumping unfolded timeframes [default = %s]\n",          pPars->fDumpFrames?  "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle synthesizing unrolled timeframes [default = %s]\n",     pPars->fUseSynth?    "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle using old CNF computation [default = %s]\n",            pPars->fUseOldCnf?   "yes": "no" );

src/sat/bmc/bmc.h

@@ -83,6 +83,7 @@ struct Bmc_AndPar_t_
     int         nFramesAdd;     // the number of additional frames
     int         nConfLimit;     // maximum number of conflicts at a node
     int         nTimeOut;       // timeout in seconds
+    int         nLutSize;       // LUT size for cut computation
     int         fLoadCnf;       // dynamic CNF loading
     int         fDumpFrames;    // dump unrolled timeframes
     int         fUseSynth;      // use synthesis

src/sat/bmc/bmcBmcAnd.c

@@ -868,14 +868,15 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
 void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
 {
     int iObj = Gia_ObjId( p->pFrames, pObj );
+    if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
+        return;
+    Vec_IntWriteEntry(p->vId2Var, iObj, 1);
     if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 )
     {
         Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
         Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
         return;
     }
-    if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
-        return;
     Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++);
     if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) )
     {
@@ -891,7 +892,7 @@ void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
         iCla  = p->pCnf->pObj2Clause[iObj];
         for ( i = 0; i < nClas; i++ )
         {
-            int nLits, pLits[8];
+            int nLits, pLits[10];
             int * pClauseThis = p->pCnf->pClauses[iCla+i];
             int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
             for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
@@ -901,7 +902,7 @@ void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
                 assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
                 pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
             }
-            assert( nLits < 8 );
+            assert( nLits <= 9 );
             if ( !sat_solver_addclause( p->pSat, pLits, pLits + nLits ) )
                 break;
         }
@@ -983,10 +984,10 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
         p->pCnf = Cnf_DeriveGia( p->pFrames );
     else
     {
-        p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 );  Gia_ManStop( pTemp );
-        p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
-//        extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-//        p->pCnf = Mf_ManGenerateCnf( p->pFrames, 6, 1, 0, 0 );
+//        p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 );  Gia_ManStop( pTemp );
+//        p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
+        extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+        p->pCnf = Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, pPars->fVerbose );
     }
     Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
     // create clauses for constant node