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

1 files changed, 146 insertions, 4 deletions

diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 860462c3..b548cf68 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -110,11 +110,15 @@ Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
     int i, n;
     vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
         for ( n = 0; n < pCube->nLits; n++ )
         {
             assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
             Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
         }
+    }
     return vFlopCount;
 }
 
@@ -202,7 +206,10 @@ int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
     int i, Entry, Counter = 0;
-    vCubes = Pdr_ManCollectCubes( p, kStart );
+    if ( p->vInfCubes == NULL )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
     vFlopCounts = Pdr_ManCountFlops( p, vCubes );
     Vec_IntForEachEntry( vFlopCounts, Entry, i )
         Counter += (Entry > 0);
@@ -338,7 +345,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     Vec_Ptr_t * vCubes;
     Pdr_Set_t * pCube;
     char ** pNamesCi;
-    int i, kStart;
+    int i, kStart, Count = 0;
     // create file
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
@@ -348,9 +355,20 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     } 
     // collect cubes
     kStart = Pdr_ManFindInvariantStart( p );
-    vCubes = Pdr_ManCollectCubes( p, kStart );
+    if ( fProved )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
     Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
 //    Pdr_ManDumpAig( p->pAig, vCubes );
+    // count cubes
+    Count = 0;
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
+        Count++;
+    }
     // collect variable appearances
     vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
@@ -361,7 +379,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
     fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
     fprintf( pFile, ".o 1\n" );
-    fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) );
+    fprintf( pFile, ".p %d\n", Count );
     // output flop names
     pNamesCi = Abc_NtkCollectCioNames( Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ), 0 );
     if ( pNamesCi )
@@ -377,6 +395,8 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     // output cubes
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {
+        if ( pCube->nRefs == -1 )
+            continue;
         Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
         fprintf( pFile, " 1\n" ); 
     }
@@ -390,6 +410,48 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
         Abc_Print( 1, "Clauses of the last timeframe were written into file \"%s\".\n", pFileName );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
+{
+    int fUseSupp = 1;
+    Vec_Str_t * vStr;
+    Vec_Int_t * vFlopCounts;
+    Vec_Ptr_t * vCubes;
+    Pdr_Set_t * pCube;
+    int i, kStart;
+    vStr = Vec_StrAlloc( 1000 );
+    // collect cubes
+    kStart = Pdr_ManFindInvariantStart( p );
+    if ( p->vInfCubes == NULL )
+        vCubes = Pdr_ManCollectCubes( p, kStart );
+    else
+        vCubes = Vec_PtrDup( p->vInfCubes );
+    Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+    // collect variable appearances
+    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
+    // output cubes
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 )
+            continue;
+        Pdr_SetPrintStr( vStr, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );  
+    }
+    Vec_IntFreeP( &vFlopCounts );
+    Vec_PtrFree( vCubes );
+    Vec_StrPush( vStr, '\0' );
+    return vStr;
+}
+
 
 /**Function*************************************************************
 
@@ -469,6 +531,86 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
     Vec_PtrFree( vCubes );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pdr_ManDeriveMarkNonInductive( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
+{
+    sat_solver * pSat;
+    Vec_Int_t * vLits;
+    Pdr_Set_t * pCube;
+    int i, kThis, RetValue, fChanges = 0, Counter = 0;
+    // create solver with the cubes
+    kThis = Vec_PtrSize(p->vSolvers);
+    pSat  = Pdr_ManCreateSolver( p, kThis );
+    // add the clauses
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
+        RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+        assert( RetValue );
+        sat_solver_compress( pSat );
+    }
+    // check each clause
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
+        if ( RetValue != l_False ) // mark as non-inductive
+        {
+            pCube->nRefs = -1;
+            fChanges = 1;
+        }
+        else
+            Counter++;
+    }
+    //printf( "Clauses = %d.\n", Counter );
+    //sat_solver_delete( pSat );
+    return fChanges;
+}
+Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce )
+{
+    Vec_Int_t * vResult;
+    Vec_Ptr_t * vCubes;
+    Pdr_Set_t * pCube;
+    int i, v, kStart;
+    abctime clk = Abc_Clock();
+    // collect cubes used in the inductive invariant
+    kStart = Pdr_ManFindInvariantStart( p );
+    vCubes = Pdr_ManCollectCubes( p, kStart );
+    // refine as long as there are changes
+    if ( fReduce )
+        while ( Pdr_ManDeriveMarkNonInductive(p, vCubes) );
+    // collect remaining clauses
+    vResult = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vResult, 0 );
+    Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
+    {
+        if ( pCube->nRefs == -1 ) // skip non-inductive
+            continue;
+        Vec_IntAddToEntry( vResult, 0, 1 );
+        Vec_IntPush( vResult, pCube->nLits );
+        for ( v = 0; v < pCube->nLits; v++ )
+            Vec_IntPush( vResult, pCube->Lits[v] );
+    }
+    //Vec_PtrFree( vCubes );
+    Vec_PtrFreeP( &p->vInfCubes );
+    p->vInfCubes = vCubes;
+    return vResult;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////