Dump inductive invariant or last interpolant after interpolation.

7 files changed, 108 insertions, 21 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 731f7c84..40d7a90c 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -522,6 +522,7 @@ extern Aig_Man_t *     Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int f
 extern Aig_Man_t *     Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs );
 extern Aig_Man_t *     Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
 extern Aig_Man_t *     Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs );
+extern Aig_Man_t *     Aig_ManDupArray( Vec_Ptr_t * vArray );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index dcd2e477..4c3b2840 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -1295,6 +1295,53 @@ Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG with only one primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray )
+{
+    Aig_Man_t * p, * pNew;
+    Aig_Obj_t * pObj;
+    int i, k;
+    if ( Vec_PtrSize(vArray) == 0 )
+        return NULL;
+    p = Vec_PtrEntry( vArray, 0 );
+    Vec_PtrForEachEntry( Aig_Man_t *, vArray, pNew, k )
+    {
+        assert( Aig_ManRegNum(pNew) == 0 );
+        assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(p) );
+    }
+    // create the new manager
+    pNew = Aig_ManStart( 10000 );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Aig_ManForEachPi( p, pObj, i )
+        Aig_ObjCreatePi(pNew);
+    // create the PIs
+    Vec_PtrForEachEntry( Aig_Man_t *, vArray, p, k )
+    {
+        Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+        Aig_ManForEachPi( p, pObj, i )
+            pObj->pData = Aig_ManPi( pNew, i );
+        Aig_ManForEachNode( p, pObj, i )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        Aig_ManForEachPo( p, pObj, i )
+            Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupSimple(): The check has failed.\n" );
+    return pNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/int/int.h b/src/aig/int/int.h
index 907691ed..4b8d78bb 100644
--- a/src/aig/int/int.h
+++ b/src/aig/int/int.h
@@ -62,6 +62,7 @@ struct Inter_ManParams_t_
     int  fUseBackward;  // perform backward interpolation
     int  fUseSeparate;  // solve each output separately
     int  fDropSatOuts;  // replace by 1 the solved outputs
+    int  fDropInvar;    // dump inductive invariant into file
     int  fVerbose;      // print verbose statistics
     int  iFrameMax;     // the time frame reached
 };
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index 0cd5eb36..3bd111be 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -179,6 +179,8 @@ p->timeCnf += clock() - clk;
             RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
 //            assert( RetValue == 0 );
             Cnf_DataFree( pCnfInter2 );
+            if ( p->vInters )
+                Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) );
         }
         //////////////////////////////////////////
 
@@ -190,7 +192,7 @@ p->timeCnf += clock() - clk;
                 if ( pPars->fVerbose )
                     printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
                 p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p );
+                Inter_ManStop( p, 0 );
                 Inter_CheckStop( pCheck );
                 return -1;
             }
@@ -237,7 +239,7 @@ p->timeCnf += clock() - clk;
                         else if ( RetValue == -1 )
                             printf( "Error: The problem timed out.\n" );
                     }
-                    Inter_ManStop( p );
+                    Inter_ManStop( p, 0 );
                     Inter_CheckStop( pCheck );
                     return 0;
                 }
@@ -260,7 +262,7 @@ p->timeCnf += clock() - clk;
                         printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
                 }
                 p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p );
+                Inter_ManStop( p, 0 );
                 Inter_CheckStop( pCheck );
                 return -1;
             }
@@ -283,7 +285,7 @@ p->timeRwr += clock() - clk;
                 if ( pPars->fVerbose )
                     printf( "The problem is trivially true for all states.\n" );
                 p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p );
+                Inter_ManStop( p, 1 );
                 Inter_CheckStop( pCheck );
                 return 1;
             }
@@ -305,6 +307,8 @@ timeTemp = clock() - clk2;
             
                         Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
                         Cnf_DataFree( pCnfInter2 );
+                        if ( p->vInters )
+                            Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) );
                     }
                 }
                 else
@@ -323,7 +327,7 @@ p->timeEqu += clock() - clk - timeTemp;
                 if ( pPars->fVerbose )
                     printf( "Proved containment of interpolants.\n" );
                 p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p );
+                Inter_ManStop( p, 1 );
                 Inter_CheckStop( pCheck );
                 return 1;
             }
@@ -331,7 +335,7 @@ p->timeEqu += clock() - clk - timeTemp;
             {
                 printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
                 p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p );
+                Inter_ManStop( p, 1 );
                 Inter_CheckStop( pCheck );
                 return -1;
             }
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index 3eab7883..66ff9578 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -114,7 +114,7 @@ extern Aig_Man_t *     Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int
 /*=== 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 );
+extern void            Inter_ManStop( Inter_Man_t * p, int fProved );
 
 /*=== intM114.c ============================================================*/
 extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut );
diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c
index 2faef198..d6219f6b 100644
--- a/src/aig/int/intMan.c
+++ b/src/aig/int/intMan.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "intInt.h"
+#include "ioa.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -51,7 +52,9 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
     p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
     p->nConfLimit = pPars->nBTLimit;
     p->fVerbose = pPars->fVerbose;
-    p->pAig = pAig;   
+    p->pAig = pAig;
+    if ( pPars->fDropInvar )
+        p->vInters = Vec_PtrAlloc( 100 );
     return p;
 }
 
@@ -68,6 +71,14 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
 ***********************************************************************/
 void Inter_ManClean( Inter_Man_t * p )
 {
+    if ( p->vInters )
+    {
+        Aig_Man_t * pMan;
+        int i;
+        Vec_PtrForEachEntry( Aig_Man_t *, p->vInters, pMan, i )
+            Aig_ManStop( pMan );
+        Vec_PtrClear( p->vInters );
+    }
     if ( p->pCnfInter )
         Cnf_DataFree( p->pCnfInter );
     if ( p->pCnfFrames )
@@ -80,6 +91,29 @@ void Inter_ManClean( Inter_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Writes interpolant into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inter_ManInterDump( Inter_Man_t * p, int fProved )
+{
+    Aig_Man_t * pMan;
+    pMan = Aig_ManDupArray( p->vInters );
+    Ioa_WriteAiger( pMan, "invar.aig", 0, 0 );
+    Aig_ManStop( pMan );
+    if ( fProved )
+        printf( "Inductive invariant is dumped into file \"invar.aig\".\n" );
+    else
+        printf( "Interpolants are dumped into file \"inter.aig\".\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Frees the interpolation manager.]
 
   Description []
@@ -89,7 +123,7 @@ void Inter_ManClean( Inter_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Inter_ManStop( Inter_Man_t * p )
+void Inter_ManStop( Inter_Man_t * p, int fProved )
 {
     if ( p->fVerbose )
     {
@@ -104,26 +138,22 @@ void Inter_ManStop( Inter_Man_t * p )
         ABC_PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
     }
 
+    if ( p->vInters )
+        Inter_ManInterDump( p, fProved );
+
     if ( p->pCnfAig )
         Cnf_DataFree( p->pCnfAig );
-    if ( p->pCnfFrames )
-        Cnf_DataFree( p->pCnfFrames );
-    if ( p->pCnfInter )
-        Cnf_DataFree( p->pCnfInter );
-    Vec_IntFree( p->vVarsAB );
     if ( p->pAigTrans )
         Aig_ManStop( p->pAigTrans );
-    if ( p->pFrames )
-        Aig_ManStop( p->pFrames );
-    if ( p->pInter )
-        Aig_ManStop( p->pInter );
     if ( p->pInterNew )
         Aig_ManStop( p->pInterNew );
+    Inter_ManClean( p );
+    Vec_PtrFreeP( &p->vInters );
+    Vec_IntFreeP( &p->vVarsAB );
     ABC_FREE( p );
 }
 
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a1d32f5b..ed40fee0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -19316,7 +19316,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, "CFTKLrtpomcgbkdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLrtpomcgbkdfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -19403,6 +19403,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fDropSatOuts ^= 1;
             break;
+        case 'f':
+            pPars->fDropInvar ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -19473,7 +19476,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbkdvh]\n" );
+    Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbkdfvh]\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 );
@@ -19491,6 +19494,7 @@ usage:
     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-f     : toggle dumping inductive invariant into a file [default = %s]\n", pPars->fDropInvar? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;