Improvements to the interpolation command 'int'; change of default switch -t.

4 files changed, 104 insertions, 40 deletions

diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index c0df48fb..646c83e1 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -50,7 +50,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
     p->nSecLimit    = 0;     // time limit in seconds
     p->nFramesK     = 1;     // the number of timeframes to use in induction
     p->fRewrite     = 0;     // use additional rewriting to simplify timeframes
-    p->fTransLoop   = 1;     // add transition into the init state under new PI var
+    p->fTransLoop   = 0;     // add transition into the init state under new PI var
     p->fUsePudlak   = 0;     // use Pudluk interpolation procedure
     p->fUseOther    = 0;     // use other undisclosed option
     p->fUseMiniSat  = 0;     // use MiniSat-1.14p instead of internal proof engine
@@ -78,6 +78,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
 {
     extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
     Inter_Man_t * p;
+    Inter_Check_t * pCheck = NULL;
     Aig_Man_t * pAigTemp;
     int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
     // sanity checks
@@ -116,12 +117,14 @@ p->timeCnf += clock() - clk;
             Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
             p->pCnfAig->nVars, p->pCnfAig->nClauses );
     }
-
+ 
     // derive interpolant
     *piFrame = -1;
     p->nFrames = 1;
     for ( s = 0; ; s++ )
     {
+        Cnf_Dat_t * pCnfInter2;
+
 clk2 = clock();
         // initial state
         if ( pPars->fUseBackward )
@@ -157,6 +160,23 @@ p->timeCnf += clock() - clk;
                 s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
             ABC_PRT( "Time", clock() - clk2 );
         }
+
+
+        //////////////////////////////////////////
+        // start containment checking
+        if ( !(pPars->fTransLoop || pPars->fUseBackward) )
+        {
+            pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK );
+            // try new containment check for the initial state
+clk = clock();
+            pCnfInter2 = Cnf_Derive( p->pInter, 1 );  
+p->timeCnf += clock() - clk;    
+            RetValue = Inter_CheckPerform( pCheck, pCnfInter2 );
+//            assert( RetValue == 0 );
+            Cnf_DataFree( pCnfInter2 );
+        }
+        //////////////////////////////////////////
+
         // iterate the interpolation procedure
         for ( i = 0; ; i++ )
         {
@@ -166,6 +186,7 @@ p->timeCnf += clock() - clk;
                     printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
                 p->timeTotal = clock() - clkTotal;
                 Inter_ManStop( p );
+                Inter_CheckStop( pCheck );
                 return -1;
             }
 
@@ -199,6 +220,7 @@ p->timeCnf += clock() - clk;
                     *piFrame = p->nFrames;
                     pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
                     Inter_ManStop( p );
+                    Inter_CheckStop( pCheck );
                     return 0;
                 }
                 // likely spurious counter-example
@@ -213,6 +235,7 @@ p->timeCnf += clock() - clk;
                 assert( p->nConfCur >= p->nConfLimit );
                 p->timeTotal = clock() - clkTotal;
                 Inter_ManStop( p );
+                Inter_CheckStop( pCheck );
                 return -1;
             }
             assert( RetValue == 1 ); // found new interpolant
@@ -234,6 +257,7 @@ p->timeRwr += clock() - clk;
                     printf( "The problem is trivially true for all states.\n" );
                 p->timeTotal = clock() - clkTotal;
                 Inter_ManStop( p );
+                Inter_CheckStop( pCheck );
                 return 1;
             }
 
@@ -242,7 +266,18 @@ clk = clock();
             if ( pPars->fCheckKstep ) // k-step unique-state induction
             {
                 if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
-                    Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
+                {
+                    if ( pPars->fTransLoop || pPars->fUseBackward )
+                        Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
+                    else
+                    {   // new containment check
+clk2 = clock();
+                        pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );  
+p->timeCnf += clock() - clk2;
+                        Status = Inter_CheckPerform( pCheck, pCnfInter2 );
+                        Cnf_DataFree( pCnfInter2 );
+                    }
+                }
                 else
                     Status = 0;
             }
@@ -260,6 +295,7 @@ p->timeEqu += clock() - clk;
                     printf( "Proved containment of interpolants.\n" );
                 p->timeTotal = clock() - clkTotal;
                 Inter_ManStop( p );
+                Inter_CheckStop( pCheck );
                 return 1;
             }
             if ( pPars->nSecLimit && ((float)pPars->nSecLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
@@ -267,6 +303,7 @@ p->timeEqu += clock() - clk;
                 printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
                 p->timeTotal = clock() - clkTotal;
                 Inter_ManStop( p );
+                Inter_CheckStop( pCheck );
                 return -1;
             }
             // save interpolant and convert it into CNF
@@ -277,14 +314,22 @@ p->timeEqu += clock() - clk;
             }
             else
             {
-                p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
-                Aig_ManStop( pAigTemp );
-                Aig_ManStop( p->pInterNew );
-                // compress the interpolant
+                if ( pPars->fUseBackward )
+                {
+                    p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
+                    Aig_ManStop( pAigTemp );
+                    Aig_ManStop( p->pInterNew );
+                    // compress the interpolant
 clk = clock();
-                p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
-                Aig_ManStop( pAigTemp );
+                    p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
+                    Aig_ManStop( pAigTemp );
 p->timeRwr += clock() - clk;
+                }
+                else // forward with the new containment checking (using only the frontier)
+                {
+                    Aig_ManStop( p->pInter );
+                    p->pInter = p->pInterNew; 
+                }
             }
             p->pInterNew = NULL;
             Cnf_DataFree( p->pCnfInter );
@@ -292,6 +337,9 @@ clk = clock();
             p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
 p->timeCnf += clock() - clk;
         }
+
+        // start containment checking
+        Inter_CheckStop( pCheck );
     }
     assert( 0 );
     return RetValue;
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index 72079a49..d5e8ed00 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -79,6 +79,9 @@ struct Inter_Man_t_
     int              timeTotal;
 };
 
+// containment checking manager
+typedef struct Inter_Check_t_ Inter_Check_t;
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -87,38 +90,43 @@ struct Inter_Man_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== intContain.c ==========================================================*/
-extern int           Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
-extern int           Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
-extern int           Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
+/*=== intCheck.c ============================================================*/
+extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
+extern void            Inter_CheckStop( Inter_Check_t * p );
+extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf );
+
+/*=== intContain.c ============================================================*/
+extern int             Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
+extern int             Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
+extern int             Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
 
-/*=== intCtrex.c ==========================================================*/
-extern void *        Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
+/*=== intCtrex.c ============================================================*/
+extern void *          Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
 
-/*=== intDup.c ==========================================================*/
-extern Aig_Man_t *   Inter_ManStartInitState( int nRegs );
-extern Aig_Man_t *   Inter_ManStartDuplicated( Aig_Man_t * p );
-extern Aig_Man_t *   Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo );
+/*=== intDup.c ============================================================*/
+extern Aig_Man_t *     Inter_ManStartInitState( int nRegs );
+extern Aig_Man_t *     Inter_ManStartDuplicated( Aig_Man_t * p );
+extern Aig_Man_t *     Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo );
 
-/*=== intFrames.c ==========================================================*/
-extern Aig_Man_t *   Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts );
+/*=== intFrames.c ============================================================*/
+extern Aig_Man_t *     Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts );
 
-/*=== intMan.c ==========================================================*/
-extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars );
-extern void          Inter_ManClean( Inter_Man_t * p );
-extern void          Inter_ManStop( Inter_Man_t * p );
+/*=== intMan.c ============================================================*/
+extern Inter_Man_t *   Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars );
+extern void            Inter_ManClean( Inter_Man_t * p );
+extern void            Inter_ManStop( Inter_Man_t * p );
 
-/*=== intM114.c ==========================================================*/
-extern int           Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
+/*=== intM114.c ============================================================*/
+extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
 
-/*=== intM114p.c ==========================================================*/
+/*=== intM114p.c ============================================================*/
 #ifdef ABC_USE_LIBRARIES
-extern int           Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther );
+extern int             Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther );
 #endif
 
-/*=== intUtil.c ==========================================================*/
-extern int           Inter_ManCheckInitialState( Aig_Man_t * p );
-extern int           Inter_ManCheckAllStates( Aig_Man_t * p );
+/*=== intUtil.c ============================================================*/
+extern int             Inter_ManCheckInitialState( Aig_Man_t * p );
+extern int             Inter_ManCheckAllStates( Aig_Man_t * p );
 
 
 
diff --git a/src/aig/int/module.make b/src/aig/int/module.make
index cf0f827f..8e0e4319 100644
--- a/src/aig/int/module.make
+++ b/src/aig/int/module.make
@@ -1,4 +1,5 @@
-SRC +=    src/aig/int/intContain.c \
+SRC +=    src/aig/int/intCheck.c \
+    src/aig/int/intContain.c \
     src/aig/int/intCore.c \
     src/aig/int/intCtrex.c \
     src/aig/int/intDup.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c9860528..733e2722 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8427,6 +8427,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern void Bbl_ManTest( Abc_Ntk_t * pNtk );
     extern void Bbl_ManSimpleDemo();
     extern Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose );
+    extern void Abc_NktMffcTest( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
 
@@ -8489,13 +8490,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
+/*
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
         Abc_Print( -1, "Only works for sequential networks.\n" );
         return 1;
     }
-
-    Abc_NtkDarTest( pNtk, nLevels );
+*/
+//    if ( fBmc )
+//        Abc_NtkBddDec( pNtk, 1 );
+//    else
+//        Abc_NktMffcTest( pNtk );
+//    Abc_NtkDarTest( pNtk, nLevels );
 
 //    Abc_NtkTestEsop( pNtk );
 //    Abc_NtkTestSop( pNtk );
@@ -18603,7 +18609,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Inter_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CFTNLrtpomcgbkdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLrtpomcgbkdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18640,7 +18646,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nSecLimit < 0 ) 
                 goto usage;
             break;
-        case 'N':
+        case 'K':
             if ( globalUtilOptind >= argc )
             {
                 Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
@@ -18760,12 +18766,13 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: int [-CFTN num] [-L file] [-rtpomcgbkdvh]\n" );
+    Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbkdvh]\n" );
     Abc_Print( -2, "\t         uses interpolation to prove the property\n" );
     Abc_Print( -2, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-F num : the limit on number of frames to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-T num : the limit on runtime per output in seconds [default = %d]\n", pPars->nSecLimit );
-    Abc_Print( -2, "\t-N num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK );
+    Abc_Print( -2, "\t-K num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK );
+    Abc_Print( -2, "\t         (K = 1 works in all cases; K > 1 works without -t and -b)\n" );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
     Abc_Print( -2, "\t-r     : toggle rewriting of the unrolled timeframes [default = %s]\n", pPars->fRewrite? "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle adding transition into the initial state [default = %s]\n", pPars->fTransLoop? "yes": "no" );
@@ -18774,7 +18781,7 @@ usage:
     Abc_Print( -2, "\t-m     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", pPars->fUseMiniSat? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" );
     Abc_Print( -2, "\t-g     : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" );
-    Abc_Print( -2, "\t-b     : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle using backward interpolation (works with -t) [default = %s]\n", pPars->fUseBackward? "yes": "no" );
     Abc_Print( -2, "\t-k     : toggle solving each output separately [default = %s]\n", pPars->fUseSeparate? "yes": "no" );
     Abc_Print( -2, "\t-d     : drops (replaces by 0) sat outputs (with -k is used) [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );