From 2d1792040a8c09a12d70413ceb99bd11bb145c2b Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Sun, 19 Feb 2017 15:57:13 -0800
Subject: working on pdr with wla

---
 src/proof/pdr/pdrIncr.c | 47 ++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 42 insertions(+), 5 deletions(-)

(limited to 'src/proof')

diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index b1f126f4..4f66eeb4 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -66,6 +66,41 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IPdr_ManCheckClauses( Pdr_Man_t * p )
+{
+    Pdr_Set_t * pCubeK;
+    Vec_Ptr_t * vArrayK;
+    int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers)-1;
+    int iStartFrame = 1;
+
+    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
+    {
+        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
+        {
+            RetValue = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 );
+
+            if ( !RetValue ) {
+                printf( "Cube[%d][%d] not inductive!\n", k, j );
+            }
+
+            assert( RetValue == 1 );
+        }
+    }
+
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -83,6 +118,11 @@ Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast )
     Vec_Vec_t * vClausesSaved;
     Pdr_Set_t * pCla;
 
+    if ( Vec_VecSize( p->vClauses ) == 1 )
+        return NULL;
+    if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast )
+        return NULL;
+
     if ( fDropLast )
         vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 );
     else 
@@ -147,9 +187,6 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses )
 
     assert(vClauses);
 
-    printf( "IPdr restore:\n" );
-    IPdr_ManPrintClauses( vClauses, 0, Aig_ManRegNum( p->pAig ) );
-
     Vec_VecFree(p->vClauses);
     p->vClauses = vClauses;
 
@@ -197,8 +234,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p )
     if ( Vec_VecSize(p->vClauses) == 0 )
         Pdr_ManCreateSolver( p, (iFrame = 0) );
     else {
-        iFrame = Vec_VecSize(p->vClauses);
-        Pdr_ManCreateSolver( p, iFrame );
+        iFrame = Vec_VecSize(p->vClauses) - 1;
+        IPdr_ManCheckClauses( p );
     }
     while ( 1 )
     {
-- 
cgit v1.2.3