working on pdr with wla

src/base/wlc/wlcAbs.c

@@ -323,7 +323,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
     Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
     Pdr_ManSetDefaultParams( pPdrPars );
     pPdrPars->fVerbose   = pPars->fPdrVerbose;
-    pPdrPars->fVeryVerbose = 1;
+    pPdrPars->fVeryVerbose = 0;
     
     // perform refinement iterations
     for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
@@ -368,14 +368,10 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         pAig = Gia_ManToAigSimple( pGia );
 
         pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
+
         if ( vClauses ) {
-            if ( Vec_VecSize( vClauses) == 1 ) {
-                Vec_VecFree( vClauses );
-                vClauses = NULL;
-            } else {
-                assert( Vec_VecSize( vClauses) >= 2 ); 
-                IPdr_ManRestore(pPdr, vClauses);
-            }
+            assert( Vec_VecSize( vClauses) >= 2 ); 
+            IPdr_ManRestore( pPdr, vClauses );
         }
 
         RetValue = IPdr_ManSolveInt( pPdr );
@@ -406,7 +402,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         }
 
         // spurious CEX, continue solving
-        vClauses = IPdr_ManSaveClauses( pPdr, 0 );
+        vClauses = IPdr_ManSaveClauses( pPdr, 1 );
         Pdr_ManStop( pPdr );
 
         // update the set of objects to be un-abstracted
@@ -465,7 +461,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
     //pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
     //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
     pPdrPars->fVerbose   = pPars->fPdrVerbose;
-    pPdrPars->fVeryVerbose = 1;
+    pPdrPars->fVeryVerbose = 0;
     // perform refinement iterations
     for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
     {

src/proof/pdr/pdrIncr.c

@@ -77,12 +77,52 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
   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    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast )
 {
     int i, k;
     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 )
     {