Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network.

8 files changed, 243 insertions, 49 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;