Added new feature to bmc3.

4 files changed, 87 insertions, 35 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 4441b923..6b85a3df 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -58,18 +58,21 @@ struct Sec_MtrStatus_t_
 typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
 struct Saig_ParBmc_t_
 {
-    int         nStart;       // starting timeframe
-    int         nFramesMax;   // maximum number of timeframes 
-    int         nConfLimit;   // maximum number of conflicts at a node
-    int         nTimeOut;     // approximate timeout in seconds
-    int         nPisAbstract; // the number of PIs to abstract
-    int         fSolveAll;    // does not stop at the first SAT output
-    int         fDropSatOuts; // replace sat outputs by constant 0
-    int         nFfToAddMax;  // max number of flops to add during CBA
-    int         fVerbose;     // verbose 
-    int         iFrame;       // explored up to this frame
-    int         nFailOuts;    // the number of failed outputs
+    int         nStart;         // starting timeframe
+    int         nFramesMax;     // maximum number of timeframes 
+    int         nConfLimit;     // maximum number of conflicts at a node
+    int         nConfLimitJump; // maximum number of conflicts after jumping
+    int         nFramesJump;    // the number of tiemframes to jump
+    int         nTimeOut;       // approximate timeout in seconds
+    int         nPisAbstract;   // the number of PIs to abstract
+    int         fSolveAll;      // does not stop at the first SAT output
+    int         fDropSatOuts;   // replace sat outputs by constant 0
+    int         nFfToAddMax;    // max number of flops to add during CBA
+    int         fVerbose;       // verbose 
+    int         iFrame;         // explored up to this frame
+    int         nFailOuts;      // the number of failed outputs
 };
+
  
 typedef struct Saig_ParBbr_t_ Saig_ParBbr_t;
 struct Saig_ParBbr_t_
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index f5a6234e..7248ed1a 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1073,6 +1073,8 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
     p->nStart         =     0;    // maximum number of timeframes 
     p->nFramesMax     =  2000;    // maximum number of timeframes 
     p->nConfLimit     =  2000;    // maximum number of conflicts at a node
+    p->nConfLimitJump =     0;    // maximum number of conflicts after jumping
+    p->nFramesJump    =     0;    // the number of tiemframes to jump
     p->nTimeOut       =     0;    // approximate timeout in seconds
     p->nPisAbstract   =     0;    // the number of PIs to abstract
     p->fSolveAll      =     0;    // stops on the first SAT instance
@@ -1097,7 +1099,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
 {
     Gia_ManBmc_t * p;
     Aig_Obj_t * pObj;
-    int RetValue = -1, fFirst = 1;
+    int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
     int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) );
     int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock();
     if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 )
@@ -1133,7 +1135,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
             return 0;
         }
         // consider the next timeframe
-        if ( RetValue == -1 && pPars->nStart == 0 )
+        if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
             pPars->iFrame = f-1;
         // resize the array
         Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
@@ -1173,7 +1175,7 @@ clkOther += clock() - clk2;
                 return 1;
             }
         }
-        if ( pPars->nStart && f < pPars->nStart )
+        if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
             continue;
         // solve SAT
         clk = clock(); 
@@ -1211,6 +1213,7 @@ clkOther += clock() - clk2;
                 continue;
             }
             // solve this output
+            fUnfinished = 0;
             sat_solver_compress( p->pSat );
             status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( status == l_False )
@@ -1232,7 +1235,7 @@ clkOther += clock() - clk2;
 //ABC_PRT( "CNF generation runtime", clkOther );
                     if ( pPars->fVerbose )
                     {
-                        printf( "%3d : ", f );
+                        printf( "%3d %s : ", f, fUnfinished ? "-" : "+" );
                         printf( "Var =%8.0f. ", (double)p->nSatVars );
                         printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
                         printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
@@ -1261,6 +1264,19 @@ clkOther += clock() - clk2;
             else 
             {
                 assert( status == l_Undef );
+                if ( pPars->nTimeOut && ((float)pPars->nTimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+                {
+                    printf( "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
+                    Saig_Bmc3ManStop( p );
+                    return RetValue;
+                }
+                if ( pPars->nFramesJump )
+                {
+                    pPars->nConfLimit = pPars->nConfLimitJump;
+                    nJumpFrame = f + pPars->nFramesJump;
+                    fUnfinished = 1;
+                    break;
+                }
                 Saig_Bmc3ManStop( p );
                 return RetValue;
             }
@@ -1278,7 +1294,7 @@ clkOther += clock() - clk2;
                 fFirst = 0;
 //                printf( "Outputs of frames up to %d are trivially UNSAT.\n", f );
             }
-            printf( "%3d : ", f );
+            printf( "%3d %s : ", f, fUnfinished ? "-" : "+" );
             printf( "Var =%8.0f. ", (double)p->nSatVars );
             printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
             printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
@@ -1293,7 +1309,9 @@ clkOther += clock() - clk2;
         }
     }
     // consider the next timeframe
-    if ( RetValue == -1 && pPars->nStart == 0 )
+    if ( nJumpFrame && pPars->nStart == 0 )
+        pPars->iFrame = nJumpFrame - pPars->nFramesJump;
+    else if ( RetValue == -1 && pPars->nStart == 0 )
         pPars->iFrame = f;
 //ABC_PRT( "CNF generation runtime", clkOther );
     if ( pPars->fVerbose )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4cbecb4e..cbbebd1f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19017,7 +19017,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, "SFTCILsdrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILsdrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -19065,6 +19065,28 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nConfLimit < 0 ) 
                 goto usage;
             break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nConfLimitJump = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nConfLimitJump < 0 ) 
+                goto usage;
+            break;
+        case 'J':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesJump = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesJump < 0 ) 
+                goto usage;
+            break;
         case 'I':
             if ( globalUtilOptind >= argc )
             {
@@ -19144,12 +19166,14 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bmc3 [-SFTCI num] [-L file] [-sdvh]\n" );
+    Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-sdvh]\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 [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->nTimeOut );
-    Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-C num : max conflicts at an output [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-D num : max conflicts after jumping (0 = infinity) [default = %d]\n", pPars->nConfLimitJump );
+    Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump );
     Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
     Abc_Print( -2, "\t-s     : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
diff --git a/src/map/if/ifDec10f.c b/src/map/if/ifDec10f.c
index 9f30cf96..9e2126e8 100644
--- a/src/map/if/ifDec10f.c
+++ b/src/map/if/ifDec10f.c
@@ -27,6 +27,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define CLU_MAX 16
+
 // the bit count for the first 256 integer numbers
 static int BitCount8[256] = {
     0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
@@ -55,18 +57,7 @@ static word Truth6[6] = {
     0xFFFF0000FFFF0000,
     0xFFFFFFFF00000000
 };
-static word Truth10[10][16] = {
-    0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA,
-    0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC,
-    0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0,
-    0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,0xFF00FF00FF00FF00,
-    0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,0xFFFF0000FFFF0000,
-    0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,0xFFFFFFFF00000000,
-    0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,
-    0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0x0000000000000000,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF,0xFFFFFFFFFFFFFFFF
-};
+static word TruthAll[CLU_MAX][1 << (CLU_MAX-6)];
 
 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
 extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
@@ -76,10 +67,26 @@ extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
 //  moving up means moving from LSB -> MSB
 //  groups list vars indices from MSB to LSB
 
+//  group representation
+//  nVars | nCofs | v5 | v4 | v3 | v2 | v1 | v0 
+//  if nCofs > 2, v0 is the shared variable
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+void If_CluInitTruthTables()
+{
+    int i, k;
+    assert( CLU_MAX <= 16 );
+    for ( i = 0; i < 6; i++ )
+        for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
+            TruthAll[i][k] = Truth6[i];
+    for ( i = 6; i < CLU_MAX; i++ )
+        for ( k = 0; k < (1 << (CLU_MAX-6)); k++ )
+            TruthAll[i][k] = ((k >> i) & 1) ? ~0 : 0;
+}
+
 // variable permutation for large functions
 static inline int If_CluWordNum( int nVars )
 {
@@ -131,7 +138,7 @@ static inline void If_CluSwapAdjacent( word * pOut, word * pIn, int iVar, int nV
 // moves one var (v) to the given position (p)
 void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
 {
-    word pG[16], * pIn = pF, * pOut = pG, * pTemp;
+    word pG[32], * pIn = pF, * pOut = pG, * pTemp;
     int iPlace0, iPlace1, Count = 0;
     assert( v >= 0 && v < nVars );
     assert( Var2Pla[v] >= p );
@@ -156,7 +163,7 @@ void If_CluMoveVarOneUp( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int
 // moves one var (v) to the given position (p)
 void If_CluMoveVarOneDown( word * pF, int * Var2Pla, int * Pla2Var, int nVars, int v, int p )
 {
-    word pG[16], * pIn = pF, * pOut = pG, * pTemp;
+    word pG[32], * pIn = pF, * pOut = pG, * pTemp;
     int iPlace0, iPlace1, Count = 0;
     assert( v >= 0 && v < nVars );
     assert( Var2Pla[v] <= p );
@@ -194,7 +201,7 @@ int If_CluCountCofs( word * pF, int * V2P, int * P2V, int nVars, int nBSsize )
     word iCofs[16], iCof;
     int i, c, nMints = (1 << nBSsize), nCofs = 1;
     assert( nBSsize >= 3 && nBSsize <= 5 );
-    assert( nVars - nBSsize >= 0 && nVars - nBSsize <= 6 );
+    assert( nVars - nBSsize > 0 && nVars - nBSsize <= 6 );
     if ( nVars - nBSsize == 6 )
         Mask = ~0;
     iCofs[0] = pF[0] & Mask;