New command %psinv.

3 files changed, 26 insertions, 0 deletions

diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 20db8f67..78cc16c1 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/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 );
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 0eb6bd81..bd9fe87c 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/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 );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index eef24b83..860462c3 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/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 []