From c4446189a9ca5a187a2ede26a7102866d2c5ae8e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 14 Jan 2016 20:42:22 -0800 Subject: Changes to PDR to compute f-inf clauses and import invariant (or clauses) as a network. --- src/proof/pdr/pdrInv.c | 150 +++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 146 insertions(+), 4 deletions(-) (limited to 'src/proof/pdr/pdrInv.c') 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 /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3