15 files changed, 457 insertions, 68 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a860a5a9..cd5f6e98 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -24985,7 +24985,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTHGaxrmsipdgvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGaxrmsipdgvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25022,6 +25022,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nConfLimit < 0 )
                 goto usage;
             break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nConfGenLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nConfGenLimit < 0 )
+                goto usage;
+            break;
         case 'R':
             if ( globalUtilOptind >= argc )
             {
@@ -25134,13 +25145,14 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCRTHG <num>] [-axrmsipdgvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-axrmsipdgvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
     Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n",       pPars->nRecycle );
     Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n",           pPars->nFrameMax );
     Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n",          pPars->nConfLimit );
+    Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit );
     Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
     Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n",                   pPars->nTimeOut );
     Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n",     pPars->nTimeOutOne );
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 44ec1c57..4fc2f87a 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -143,6 +143,8 @@ extern ABC_DLL void            Abc_FrameSetStatus( int Status );
 extern ABC_DLL void            Abc_FrameSetManDsd( void * pMan );
 extern ABC_DLL void            Abc_FrameSetManDsd2( void * pMan );
 extern ABC_DLL void            Abc_FrameSetInv( Vec_Int_t * vInv );
+extern ABC_DLL void            Abc_FrameSetCnf( Vec_Int_t * vInv );
+extern ABC_DLL void            Abc_FrameSetStr( Vec_Str_t * vInv );
 
 extern ABC_DLL int             Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
 
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 54c97854..16c11288 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -93,6 +93,8 @@ void        Abc_FrameSetStatus( int Status )                 { ABC_FREE( s_Globa
 void        Abc_FrameSetManDsd( void * pMan )                { if (s_GlobalFrame->pManDsd  && s_GlobalFrame->pManDsd  != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd,  0); s_GlobalFrame->pManDsd = pMan;  }
 void        Abc_FrameSetManDsd2( void * pMan )               { if (s_GlobalFrame->pManDsd2 && s_GlobalFrame->pManDsd2 != pMan) If_DsdManFree((If_DsdMan_t *)s_GlobalFrame->pManDsd2, 0); s_GlobalFrame->pManDsd2 = pMan; }
 void        Abc_FrameSetInv( Vec_Int_t * vInv )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
+void        Abc_FrameSetCnf( Vec_Int_t * vCnf )              { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcCnf); s_GlobalFrame->pAbcWlcCnf = vCnf; }
+void        Abc_FrameSetStr( Vec_Str_t * vStr )              { Vec_StrFreeP(&s_GlobalFrame->pAbcWlcStr); s_GlobalFrame->pAbcWlcStr = vStr; }
 
 int         Abc_FrameIsBatchMode()                           { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0;              } 
 
@@ -221,6 +223,8 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     ABC_FREE( p->pCex2 );
     ABC_FREE( p->pCex );
     Vec_IntFreeP( &p->pAbcWlcInv );
+    Vec_IntFreeP( &p->pAbcWlcCnf );
+    Vec_StrFreeP( &p->pAbcWlcStr );
     ABC_FREE( p );
     s_GlobalFrame = NULL;
 }
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index c7535c74..4082bab0 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -129,6 +129,8 @@ struct Abc_Frame_t_
     void *          pAbc85Delay;
     void *          pAbcWlc;
     Vec_Int_t *     pAbcWlcInv;
+    Vec_Int_t *     pAbcWlcCnf;
+    Vec_Str_t *     pAbcWlcStr;
     void *          pAbcBac;
     void *          pAbcCba;
     void *          pAbcPla;
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index f3aa6871..7bc7aa39 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/base/wlc/wlcAbs.c \
+    src/base/wlc/wlcAbc.c \
     src/base/wlc/wlcBlast.c \
     src/base/wlc/wlcCom.c \
     src/base/wlc/wlcNtk.c \
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
new file mode 100644
index 00000000..0bf27f7b
--- /dev/null
+++ b/src/base/wlc/wlcAbc.c
@@ -0,0 +1,154 @@
+/**CFile****************************************************************
+
+  FileName    [wlcAbc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Parses several flavors of word-level Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcAbc.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+#include "base/abc/abc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
+{
+    Wlc_Obj_t * pObj;
+    int i, k, nNum, nRange, nBits = 0;
+    Wlc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( pObj->Type != WLC_OBJ_FO )
+            continue;
+        nRange = Wlc_ObjRange(pObj);
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry(vInv, nBits + k);
+            if ( nNum )
+                break;
+        }
+        if ( k == nRange )
+        {
+            nBits += nRange;
+            continue;
+        }
+        printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry( vInv, nBits + k );
+            if ( nNum == 0 )
+                continue;
+            printf( "  [%d] -> %d", k, nNum );
+        }
+        printf( "\n");
+        nBits += nRange;
+    }
+    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
+    assert( Vec_IntSize(vInv) == nBits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
+{
+    Wlc_Obj_t * pObj;
+    int i, k, nNum, nRange, nBits = 0;
+    Abc_Ntk_t * pMainNtk = NULL;
+    Abc_Obj_t * pMainObj, * pMainTemp;
+    char Buffer[5000];
+    // start the network
+    pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+    // duplicate the name and the spec
+    pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);
+    // create primary inputs
+    Wlc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( pObj->Type != WLC_OBJ_FO )
+            continue;
+        nRange = Wlc_ObjRange(pObj);
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry(vInv, nBits + k);
+            if ( nNum )
+                break;
+        }
+        if ( k == nRange )
+        {
+            nBits += nRange;
+            continue;
+        }
+        //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+        for ( k = 0; k < nRange; k++ )
+        {
+            nNum = Vec_IntEntry( vInv, nBits + k );
+            if ( nNum == 0 )
+                continue;
+            //printf( "  [%d] -> %d", k, nNum );
+            pMainObj = Abc_NtkCreatePi( pMainNtk );
+            sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
+            Abc_ObjAssignName( pMainObj, Buffer, NULL );
+
+        }
+        //printf( "\n");
+        nBits += nRange;
+    }
+    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
+    assert( Vec_IntSize(vInv) == nBits );
+    // create node
+    pMainObj = Abc_NtkCreateNode( pMainNtk );
+    Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
+        Abc_ObjAddFanin( pMainObj, pMainTemp );
+    pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
+    // create PO
+    pMainTemp = Abc_NtkCreatePo( pMainNtk );
+    Abc_ObjAddFanin( pMainTemp, pMainObj );
+    Abc_ObjAssignName( pMainTemp, "inv", NULL );
+    return pMainNtk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 426d9bbf..f3e0af8a 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1111,52 +1111,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
     return pNew;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
-{
-    Wlc_Obj_t * pObj;
-    int i, k, nNum, nRange, nBits = 0;
-    Wlc_NtkForEachCi( pNtk, pObj, i )
-    {
-        if ( pObj->Type != WLC_OBJ_FO )
-            continue;
-        nRange = Wlc_ObjRange(pObj);
-        for ( k = 0; k < nRange; k++ )
-        {
-            nNum = Vec_IntEntry(vInv, nBits + k);
-            if ( nNum )
-                break;
-        }
-        if ( k == nRange )
-        {
-            nBits += nRange;
-            continue;
-        }
-        printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
-        for ( k = 0; k < nRange; k++ )
-        {
-            nNum = Vec_IntEntry( vInv, nBits + k );
-            if ( nNum == 0 )
-                continue;
-            printf( "  [%d] -> %d", k, nNum );
-        }
-        printf( "\n");
-        nBits += nRange;
-    }
-    //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
-    assert( Vec_IntSize(vInv) == nBits );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 3f8cc492..1584e346 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -33,6 +33,7 @@ static int  Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPsInv    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandGetInv   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
@@ -40,6 +41,8 @@ static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )
 static inline void        Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )  { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk;             }
 
 static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcInv;                                }
+static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcCnf;                                }
+static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc )                       { return pAbc->pAbcWlcStr;                                }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -63,6 +66,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%ps",         Abc_CommandPs,        0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",      Abc_CommandBlast,     0 );
     Cmd_CommandAdd( pAbc, "Word level", "%psinv",      Abc_CommandPsInv,     0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%getinv",     Abc_CommandGetInv,    0 );
     Cmd_CommandAdd( pAbc, "Word level", "%test",       Abc_CommandTest,      0 );
 }
 
@@ -421,7 +425,68 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
     usage:
     Abc_Print( -2, "usage: %%psinv [-vh]\n" );
-    Abc_Print( -2, "\t         prints inductive invariant statistics\n" );
+    Abc_Print( -2, "\t         prints statistics for inductive invariant\n" );
+    Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose );
+    Abc_Ntk_t * pMainNtk;
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" );
+        return 0;
+    }
+    if ( Wlc_AbcGetNtk(pAbc) == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" );
+        return 0;
+    }
+    if ( Wlc_AbcGetInv(pAbc) == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" );
+        return 0;
+    }
+    // derive the network
+    pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
+    return 0;
+    usage:
+    Abc_Print( -2, "usage: %%getinv [-vh]\n" );
+    Abc_Print( -2, "\t         places invariant found by PDR as the current network in the main-space\n" );
+    Abc_Print( -2, "\t         (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index adbdafca..e4b764a1 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -44,6 +44,7 @@ struct Pdr_Par_t_
     int nRecycle;         // limit on vars for recycling
     int nFrameMax;        // limit on frame count
     int nConfLimit;       // limit on SAT solver conflicts
+    int nConfGenLimit;    // limit on SAT solver conflicts during generalization
     int nRestLimit;       // limit on the number of proof-obligations
     int nTimeOut;         // timeout in seconds
     int nTimeOutGap;      // approximate timeout in seconds since the last change
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 78cc16c1..8e81795b 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -55,6 +55,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->nTimeOut       =       0;  // timeout in seconds
     pPars->nTimeOutGap    =       0;  // timeout in seconds since the last solved
     pPars->nConfLimit     =       0;  // limit on SAT solver conflicts
+    pPars->nConfGenLimit  =       0;  // limit on SAT solver conflicts during generalization
     pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
     pPars->fTwoRounds     =       0;  // use two rounds for generalization
     pPars->fMonoCnf       =       0;  // monolythic CNF
@@ -115,7 +116,7 @@ Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
     // make sure the cube works
     {
     int RetValue;
-    RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
+    RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 );
     assert( RetValue );
     }
 */
@@ -162,7 +163,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
             }
 
             // check if the clause can be moved to the next frame
-            RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 );
+            RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0 );
             if ( RetValue2 == -1 )
                 return -1;
             if ( !RetValue2 )
@@ -310,7 +311,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     int * pOrder;
     // if there is no induction, return
     *ppCubeMin = NULL;
-    RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
+    RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 );
     if ( RetValue == -1 )
         return -1;
     if ( RetValue == 0 )
@@ -343,7 +344,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
                 continue;
             // try removing this literal
             Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
-            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
             if ( RetValue == -1 )
             {
                 Pdr_SetDeref( pCubeMin );
@@ -381,7 +382,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
                 continue;
             // try removing this literal
             Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
-            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 );
             if ( RetValue == -1 )
             {
                 Pdr_SetDeref( pCubeMin );
@@ -494,7 +495,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             assert( pPred == NULL );
             for ( k = pThis->iFrame; k < kMax; k++ )
             {
-                RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
+                RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0, 0 );
                 if ( RetValue == -1 )
                 {
                     Pdr_OblDeref( pThis );
@@ -659,7 +660,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     p->pPars->iFrame = k;
                     return -1;
                 }
-                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
+                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit, 0 );
                 if ( RetValue == 1 )
                     break;
                 if ( RetValue == -1 )
@@ -911,10 +912,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
     RetValue = Pdr_ManSolveInt( p );
     if ( RetValue == 0 )
         assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
-    if ( RetValue == 1 )
-        Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
-    else
-        Abc_FrameSetInv( NULL );
     if ( p->vCexes )
     {
         assert( p->pAig->vSeqModelVec == NULL );
@@ -922,7 +919,12 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
         p->vCexes = NULL;
     }
     if ( p->pPars->fDumpInv )
+    {
+        Abc_FrameSetCnf( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
+        Abc_FrameSetStr( Pdr_ManDumpString(p) );
+        Abc_FrameSetInv( Pdr_ManCountFlopsInv(p) );
         Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
+    }
     p->tTotal += Abc_Clock() - clk;
     Pdr_ManStop( p );
     pPars->iFrame--;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index bd9fe87c..6a08a150 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -101,6 +101,7 @@ struct Pdr_Man_t_
     Vec_Int_t * vSuppLits; // support literals
     Pdr_Set_t * pCubeJust; // justification
     abctime *   pTime4Outs;// timeout per output
+    Vec_Ptr_t * vInfCubes; // infinity clauses/cubes
     // statistics
     int         nBlocks;   // the number of times blockState was called
     int         nObligs;   // the number of proof obligations derived
@@ -167,8 +168,10 @@ extern Vec_Int_t *     Pdr_ManCountFlopsInv( Pdr_Man_t * p );
 extern void            Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time );
 extern void            Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
 extern void            Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved );
+extern Vec_Str_t *     Pdr_ManDumpString( Pdr_Man_t * p );
 extern void            Pdr_ManReportInvariant( Pdr_Man_t * p );
 extern void            Pdr_ManVerifyInvariant( Pdr_Man_t * p );
+extern Vec_Int_t *     Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce );
 /*=== pdrMan.c ==========================================================*/
 extern Pdr_Man_t *     Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
 extern void            Pdr_ManStop( Pdr_Man_t * p );
@@ -182,7 +185,7 @@ extern Vec_Int_t *     Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, in
 extern void            Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
 extern void            Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
 extern int             Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
-extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit );
+extern int             Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf );
 /*=== pdrTsim.c ==========================================================*/
 extern Pdr_Set_t *     Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
 /*=== pdrUtil.c ==========================================================*/
@@ -197,6 +200,7 @@ extern int             Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
 extern int             Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
 extern int             Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
 extern void            Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
+extern void            Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
 extern int             Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
 extern Pdr_Obl_t *     Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
 extern Pdr_Obl_t *     Pdr_OblRef( Pdr_Obl_t * p );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 860462c3..b548cf68 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -110,11 +110,15 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
     int i, n;
     vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
         for ( n = 0; n < pCube->nLits; n++ )
         {
             assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
             Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
         }
+    }
     return vFlopCount;
 }
 
@@ -202,7 +206,10 @@ int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
     int i, Entry, Counter = 0;
-    vCubes = Pdr_ManCollectCubes( p, kStart );
+    if ( p->vInfCubes == NULL )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
     vFlopCounts = Pdr_ManCountFlops( p, vCubes );
     Vec_IntForEachEntry( vFlopCounts, Entry, i )
         Counter += (Entry > 0);
@@ -338,7 +345,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     Vec_Ptr_t * vCubes;
     Pdr_Set_t * pCube;
     char ** pNamesCi;
-    int i, kStart;
+    int i, kStart, Count = 0;
     // create file
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
@@ -348,9 +355,20 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     } 
     // collect cubes
     kStart = Pdr_ManFindInvariantStart( p );
-    vCubes = Pdr_ManCollectCubes( p, kStart );
+    if ( fProved )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
     Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
 //    Pdr_ManDumpAig( p->pAig, vCubes );
+    // count cubes
+    Count = 0;
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
+        Count++;
+    }
     // collect variable appearances
     vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
@@ -361,7 +379,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
     fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
     fprintf( pFile, ".o 1\n" );
-    fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) );
+    fprintf( pFile, ".p %d\n", Count );
     // output flop names
     pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 );
     if ( pNamesCi )
@@ -377,6 +395,8 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     // output cubes
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {
+        if ( pCube->nRefs == -1 )
+            continue;
         Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
         fprintf( pFile, " 1\n" ); 
     }
@@ -390,6 +410,48 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
         Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
+{
+    int fUseSupp = 1;
+    Vec_Str_t * vStr;
+    Vec_Int_t * vFlopCounts;
+    Vec_Ptr_t * vCubes;
+    Pdr_Set_t * pCube;
+    int i, kStart;
+    vStr = Vec_StrAlloc( 1000 );
+    // collect cubes
+    kStart = Pdr_ManFindInvariantStart( p );
+    if ( p->vInfCubes == NULL )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
+    Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+    // collect variable appearances
+    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
+    // output cubes
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
+        Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
+    }
+    Vec_IntFreeP( &vFlopCounts );
+    Vec_PtrFree( vCubes );
+    Vec_StrPush( vStr, '\0' );
+    return vStr;
+}
+
 
 /**Function*************************************************************
 
@@ -469,6 +531,86 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
     Vec_PtrFree( vCubes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
+{
+    sat_solver * pSat;
+    Vec_Int_t * vLits;
+    Pdr_Set_t * pCube;
+    int i, kThis, RetValue, fChanges = 0, Counter = 0;
+    // create solver with the cubes
+    kThis = Vec_PtrSize(p->vSolvers);
+    pSat  = Pdr_ManCreateSolver( p, kThis );
+    // add the clauses
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
+        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+        assert( RetValue );
+        sat_solver_compress( pSat );
+    }
+    // check each clause
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+        if ( RetValue != l_False ) // mark as non-inductive
+        {
+            pCube->nRefs = -1;
+            fChanges = 1;
+        }
+        else
+            Counter++;
+    }
+    //printf( "Clauses = %d.\n", Counter );
+    //sat_solver_delete( pSat );
+    return fChanges;
+}
+Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
+{
+    Vec_Int_t * vResult;
+    Vec_Ptr_t * vCubes;
+    Pdr_Set_t * pCube;
+    int i, v, kStart;
+    abctime clk = Abc_Clock();
+    // collect cubes used in the inductive invariant
+    kStart = Pdr_ManFindInvariantStart( p );
+    vCubes = Pdr_ManCollectCubes( p, kStart );
+    // refine as long as there are changes
+    if ( fReduce )
+        while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) );
+    // collect remaining clauses
+    vResult = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vResult, 0 );
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        Vec_IntAddToEntry( vResult, 0, 1 );
+        Vec_IntPush( vResult, pCube->nLits );
+        for ( v = 0; v < pCube->nLits; v++ )
+            Vec_IntPush( vResult, pCube->Lits[v] );
+    }
+    //Vec_PtrFree( vCubes );
+    Vec_PtrFreeP( &p->vInfCubes );
+    p->vInfCubes = vCubes;
+    return vResult;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 9a73b697..b58c479b 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -163,6 +163,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_IntFree( p->vCi2Rem   );  // CIs to be removed
     Vec_IntFree( p->vRes      );  // final result
     Vec_IntFree( p->vSuppLits );  // support literals
+    Vec_PtrFreeP( &p->vInfCubes );
     ABC_FREE( p->pCubeJust );
     ABC_FREE( p->pTime4Outs );
     if ( p->vCexes )
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 244d0311..f3681adb 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -283,7 +283,7 @@ int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
   SeeAlso     []
 
 ***********************************************************************/
-int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit )
+int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit, int fTryConf )
 { 
     int fUseLit = 1;
     int fLitUsed = 0;
@@ -329,10 +329,15 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
         // solve 
         clk = Abc_Clock();
         Limit = sat_solver_set_runtime_limit( pSat, Pdr_ManTimeLimit(p) );
-        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), fTryConf ? p->pPars->nConfGenLimit : nConfLimit, 0, 0, 0 );
         sat_solver_set_runtime_limit( pSat, Limit );
         if ( RetValue == l_Undef )
-            return -1;
+        {
+            if ( fTryConf && p->pPars->nConfGenLimit )
+                RetValue = l_True;
+            else
+                return -1;
+        }
 /*
         if ( RetValue == l_True )
         {
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 1536c1cc..53a8a54a 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -251,6 +251,46 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
+{
+    char * pBuff;
+    int i, k = 0, Entry;
+    pBuff = ABC_ALLOC( char, nRegs + 1 );
+    for ( i = 0; i < nRegs; i++ )
+        pBuff[i] = '-';
+    pBuff[i] = 0;
+    for ( i = 0; i < p->nLits; i++ )
+    {
+        if ( p->Lits[i] == -1 )
+            continue;
+        pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
+    }
+    if ( vFlopCounts )
+    {
+        // skip some literals
+        Vec_IntForEachEntry( vFlopCounts, Entry, i )
+            if ( Entry ) 
+                pBuff[k++] = pBuff[i];
+        pBuff[k] = 0;
+    }
+    Vec_StrPushBuffer( vStr, pBuff, k );
+    Vec_StrPush( vStr, ' ' );
+    Vec_StrPush( vStr, '0' );
+    Vec_StrPush( vStr, '\n' );
+    ABC_FREE( pBuff );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Return 1 if pOld set-theoretically contains pNew.]
 
   Description []