New command %psinv.

src/base/main/main.h

@@ -142,6 +142,7 @@ extern ABC_DLL void            Abc_FrameSetNFrames( int nFrames );
 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 int             Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
 

src/base/main/mainFrame.c

@@ -64,8 +64,8 @@ void *      Abc_FrameReadManDd()                             { if ( s_GlobalFram
 #endif
 void *      Abc_FrameReadManDec()                            { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart();                                        return s_GlobalFrame->pManDec; } 
 void *      Abc_FrameReadManDsd()                            { return s_GlobalFrame->pManDsd;      } 
-void *      Abc_FrameReadManDsd2()                           { return s_GlobalFrame->pManDsd2;     } 
-char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );   } 
+void *      Abc_FrameReadManDsd2()                           { return s_GlobalFrame->pManDsd2;     }
+char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagReadByName( s_GlobalFrame, pFlag );   }
 
 int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFrame->nFrames;      }               
 int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFrame->Status;       }               
@@ -92,6 +92,7 @@ void        Abc_FrameSetNFrames( int nFrames )               { ABC_FREE( s_Globa
 void        Abc_FrameSetStatus( int Status )                 { ABC_FREE( s_GlobalFrame->pCex ); s_GlobalFrame->Status = Status;   }
 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; }
 
 int         Abc_FrameIsBatchMode()                           { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0;              } 
 
@@ -219,6 +220,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     ABC_FREE( p->pDrivingCell );
     ABC_FREE( p->pCex2 );
     ABC_FREE( p->pCex );
+    Vec_IntFreeP( &p->pAbcWlcInv );
     ABC_FREE( p );
     s_GlobalFrame = NULL;
 }

src/base/main/mainInt.h

@@ -128,6 +128,7 @@ struct Abc_Frame_t_
     void *          pAbc85Best;
     void *          pAbc85Delay;
     void *          pAbcWlc;
+    Vec_Int_t *     pAbcWlcInv;
     void *          pAbcBac;
     void *          pAbcCba;
     void *          pAbcPla;

src/base/wlc/wlcBlast.c

@@ -1027,6 +1027,51 @@ 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                                ///

src/base/wlc/wlcCom.c

@@ -32,12 +32,15 @@ static int  Abc_CommandReadWlc  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 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_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;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(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;                                }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -59,6 +62,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%write",      Abc_CommandWriteWlc,  0 );
     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", "%test",       Abc_CommandTest,      0 );
 }
 
@@ -379,6 +383,56 @@ usage:
   SeeAlso     []
 
 ******************************************************************************/
+int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
+    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_CommandPsInv(): There is no current design.\n" );
+        return 0;
+    }
+    if ( Wlc_AbcGetNtk(pAbc) == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" );
+        return 0;
+    }
+    Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose );
+    return 0;
+    usage:
+    Abc_Print( -2, "usage: %%psinv [-vh]\n" );
+    Abc_Print( -2, "\t         prints inductive invariant statistics\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_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );

src/proof/pdr/pdrCore.c

@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "pdrInt.h"
+#include "base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -910,6 +911,10 @@ 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 );

src/proof/pdr/pdrInt.h

@@ -163,6 +163,7 @@ extern sat_solver *    Pdr_ManNewSolver( sat_solver * pSat, Pdr_Man_t * p, int k
 /*=== pdrCore.c ==========================================================*/
 extern int             Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet );
 /*=== pdrInv.c ==========================================================*/
+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 );

src/proof/pdr/pdrInv.c

@@ -168,6 +168,26 @@ Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Pdr_ManCountFlopsInv( Pdr_Man_t * p )
+{
+    int kStart = Pdr_ManFindInvariantStart(p);
+    Vec_Ptr_t *vCubes = Pdr_ManCollectCubes(p, kStart);
+    Vec_Int_t * vInv = Pdr_ManCountFlops( p, vCubes );
+    Vec_PtrFree(vCubes);
+    return vInv;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of variables used in the clauses.]
 
   Description []