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

3 files changed, 90 insertions, 33 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 \