New BMC engine.

src/aig/gia/giaJf.c

@@ -1453,6 +1453,8 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
     {
         vLits = Vec_IntAlloc( 1000 );
         vClas = Vec_IntAlloc( 1000 );
+        Vec_IntPush( vClas, Vec_IntSize(vLits) );
+        Vec_IntPush( vLits, 1 );
     }
     // create new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
@@ -1538,8 +1540,6 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
     // derive CNF
     if ( p->pPars->fGenCnf )
     {
-        Vec_IntPush( vClas, Vec_IntSize(vLits) );
-        Vec_IntPush( vLits, 1 );
         pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas );
     }
     Vec_IntFreeP( &vLits );

src/base/abci/abc.c

@@ -32454,6 +32454,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFramesMax    =    0;  // maximum number of timeframes 
     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->fLoadCnf      =    0;  // dynamic CNF loading
     pPars->fDumpFrames   =    0;  // dump unrolled timeframes
     pPars->fUseSynth     =    0;  // use synthesis
@@ -32465,7 +32466,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, "SFAdscvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFATdscvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32502,6 +32503,17 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nFramesAdd < 0 )
                 goto usage;
             break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTimeOut < 0 )
+                goto usage;
+            break;
         case 'd':
             pPars->fDumpFrames ^= 1;
             break;
@@ -32534,11 +32546,12 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &bmc [-SFA num] [-dscvwh]\n" );
+    Abc_Print( -2, "usage: &bmc [-SFAT 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-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

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

src/sat/bmc/bmcBmcAnd.c

@@ -868,14 +868,14 @@ 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;
     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) )
     {
@@ -960,6 +960,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2;
     abctime clk = Abc_Clock();
     p = Bmc_MnaAlloc();
+    sat_solver_set_runtime_limit( p->pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
     p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
     nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
     if ( pPars->fVerbose )