Enabling two-timeframe property check in the interpolation procedure.

4 files changed, 31 insertions, 20 deletions

diff --git a/src/proof/int/int.h b/src/proof/int/int.h
index a93e3c93..97d628b4 100644
--- a/src/proof/int/int.h
+++ b/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
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index 69ca5044..cfab05dc 100644
--- a/src/proof/int/intCore.c
+++ b/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 )
         {
diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c
index 7c5231b7..186f1c54 100644
--- a/src/proof/int/intFrames.c
+++ b/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;
diff --git a/src/proof/int/intInt.h b/src/proof/int/intInt.h
index b7f7a2a7..85b9bfa2 100644
--- a/src/proof/int/intInt.h
+++ b/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 );