Enabling two-timeframe property check in the interpolation procedure.

src/base/abci/abc.c

@@ -21054,7 +21054,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, "CFTKLrtpomcgbkdfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLrtpomcgbqkdfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -21135,6 +21135,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             pPars->fUseBackward ^= 1;
             break;
+        case 'q':
+            pPars->fUseTwoFrames ^= 1;
+            break;
         case 'k':
             pPars->fUseSeparate ^= 1;
             break;
@@ -21226,7 +21229,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbkdfvh]\n" );
+    Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbqkdfvh]\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 );
@@ -21242,6 +21245,7 @@ usage:
     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 (works with -t) [default = %s]\n", pPars->fUseBackward? "yes": "no" );
+    Abc_Print( -2, "\t-q     : toggle using property in two last timeframes [default = %s]\n", pPars->fUseTwoFrames? "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-f     : toggle dumping inductive invariant into a file [default = %s]\n", pPars->fDropInvar? "yes": "no" );

src/proof/int/int.h

@@ -61,6 +61,7 @@ struct Inter_ManParams_t_
     int  fUseBias;      // bias decisions to global variables
     int  fUseBackward;  // perform backward interpolation
     int  fUseSeparate;  // solve each output separately
+    int  fUseTwoFrames; // create the OR of two last timeframes
     int  fDropSatOuts;  // replace by 1 the solved outputs
     int  fDropInvar;    // dump inductive invariant into file
     int  fVerbose;      // print verbose statistics

src/proof/int/intCore.c

@@ -46,22 +46,23 @@ ABC_NAMESPACE_IMPL_START
 void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
 { 
     memset( p, 0, sizeof(Inter_ManParams_t) );
-    p->nBTLimit     = 0;     // limit on the number of conflicts
-    p->nFramesMax   = 0;     // the max number timeframes to unroll
-    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   = 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
-    p->fCheckKstep  = 1;     // check using K-step induction
-    p->fUseBias     = 0;     // bias decisions to global variables
-    p->fUseBackward = 0;     // perform backward interpolation
-    p->fUseSeparate = 0;     // solve each output separately
-    p->fDropSatOuts = 0;     // replace by 1 the solved outputs
-    p->fVerbose     = 0;     // print verbose statistics
-    p->iFrameMax    =-1;
+    p->nBTLimit      = 0;     // limit on the number of conflicts
+    p->nFramesMax    = 0;     // the max number timeframes to unroll
+    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    = 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
+    p->fCheckKstep   = 1;     // check using K-step induction
+    p->fUseBias      = 0;     // bias decisions to global variables
+    p->fUseBackward  = 0;     // perform backward interpolation
+    p->fUseSeparate  = 0;     // solve each output separately
+    p->fUseTwoFrames = 0;     // create OR of two last timeframes
+    p->fDropSatOuts  = 0;     // replace by 1 the solved outputs
+    p->fVerbose      = 0;     // print verbose statistics
+    p->iFrameMax     =-1;
 }
 
 /**Function*************************************************************
@@ -146,7 +147,7 @@ clk = clock();
         p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
 p->timeCnf += clock() - clk;    
         // timeframes
-        p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward );
+        p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward, pPars->fUseTwoFrames );
 clk = clock();
         if ( pPars->fRewrite )
         {

src/proof/int/intFrames.c

@@ -44,10 +44,11 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts )
+Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts, int fUseTwoFrames )
 {
     Aig_Man_t * pFrames;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    Aig_Obj_t * pLastPo = NULL;
     int i, f;
     assert( Saig_ManRegNum(pAig) > 0 );
     assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
@@ -83,6 +84,9 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
         }
         if ( f == nFrames - 1 )
             break;
+        // remember the last PO
+        pObj = Aig_ManCo( pAig, 0 );
+        pLastPo = Aig_ObjChild0Copy(pObj);
         // save register inputs
         Saig_ManForEachLi( pAig, pObj, i )
             pObj->pData = Aig_ObjChild0Copy(pObj);
@@ -100,7 +104,12 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     else
     {
         pObj = Aig_ManCo( pAig, 0 );
-        Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
+        // add the last PO
+        if ( pLastPo == NULL || !fUseTwoFrames )
+            pLastPo = Aig_ObjChild0Copy(pObj);
+        else
+            pLastPo = Aig_Or( pFrames, pLastPo, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pFrames, pLastPo );
     }
     Aig_ManCleanup( pFrames );
     return pFrames;

src/proof/int/intInt.h

@@ -109,7 +109,7 @@ 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 );
+extern Aig_Man_t *     Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts, int fUseTwoFrames );
 
 /*=== intMan.c ============================================================*/
 extern Inter_Man_t *   Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars );