From cf1106aba8d940a6d9d5f410b6773c24bdf0d393 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 24 Jan 2017 22:28:28 -0800 Subject: Adding features for invariant minimization. --- src/base/wlc/wlcCom.c | 16 ++++++++-------- src/proof/pdr/pdrInv.c | 43 +++++++++++++++++++++++++++---------------- 2 files changed, 35 insertions(+), 24 deletions(-) (limited to 'src') diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 85b3b35d..be9ba7f6 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -601,7 +601,7 @@ usage: ******************************************************************************/ int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Pdr_InvPrint( Vec_Int_t * vInv ); + extern void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose ); int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -622,7 +622,7 @@ int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" ); return 0; } - Pdr_InvPrint( Wlc_AbcGetInv(pAbc) ); + Pdr_InvPrint( Wlc_AbcGetInv(pAbc), fVerbose ); return 0; usage: Abc_Print( -2, "usage: inv_print [-vh]\n" ); @@ -646,7 +646,7 @@ usage: ******************************************************************************/ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ); + extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); int c, nFailed, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -677,7 +677,7 @@ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" ); return 0; } - nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) ); + nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose ); if ( nFailed ) printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); else @@ -811,8 +811,8 @@ usage: ******************************************************************************/ int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv ); - extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv ); + extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); + extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); Vec_Int_t * vInv, * vInv2; int c, fLits = 0, fVerbose = 0; Extra_UtilGetoptReset(); @@ -849,9 +849,9 @@ int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } if ( fLits ) - vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv ); + vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv, fVerbose ); else - vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv ); + vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv, fVerbose ); if ( vInv2 ) Abc_FrameSetInv( vInv2 ); return 0; diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 8cfc7450..19e6c90e 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -678,17 +678,20 @@ Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts ) Vec_IntFree( vMap ); return vStr; } -void Pdr_InvPrint( Vec_Int_t * vInv ) +void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose ) { - Vec_Int_t * vCounts = Pdr_InvCounts( vInv ); - Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts ); printf( "Invariant contains %d clauses with %d literals and %d flops (out of %d).\n", Vec_IntEntry(vInv, 0), Vec_IntSize(vInv)-Vec_IntEntry(vInv, 0)-2, Pdr_InvUsedFlopNum(vInv), Vec_IntEntryLast(vInv) ); - printf( "%s", Vec_StrArray( vStr ) ); - Vec_IntFree( vCounts ); - Vec_StrFree( vStr ); + if ( fVerbose ) + { + Vec_Int_t * vCounts = Pdr_InvCounts( vInv ); + Vec_Str_t * vStr = Pdr_InvPrintStr( vInv, vCounts ); + printf( "%s", Vec_StrArray( vStr ) ); + Vec_IntFree( vCounts ); + Vec_StrFree( vStr ); + } } -int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ) +int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) { int nBTLimit = 0; int i, k, status, nFailed = 0; @@ -696,7 +699,7 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ) Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); // collect cubes - int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0]; + int * pCube, * pList = Vec_IntArray(vInv); // create variables Vec_Int_t * vLits = Vec_IntAlloc(100); int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p); @@ -731,6 +734,8 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ) continue; assert( status == l_True ); nFailed++; + if ( fVerbose ) + printf( "Verification failed for clause %d.\n", i ); } Cnf_DataFree( pCnf ); sat_solver_delete( pSat ); @@ -738,10 +743,11 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ) return nFailed; } -Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv ) +Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) { int nBTLimit = 0; - int fCheckProperty = 0; + int fCheckProperty = 1; + abctime clk = Abc_Clock(); int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0; Vec_Int_t * vRes = NULL; // create SAT solver @@ -827,14 +833,16 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv ) break; if ( fCannot ) continue; + if ( fVerbose ) printf( "Removing clause %d.\n", i ); Vec_BitWriteEntry( vRemoved, i, 1 ); nRemoved++; } if ( nRemoved ) - printf( "Invariant minimization reduced %d clauses (out of %d).\n", nRemoved, nCubes ); + printf( "Invariant minimization reduced %d clauses (out of %d). ", nRemoved, nCubes ); else - printf( "Invariant minimization did not change the invariant.\n" ); + printf( "Invariant minimization did not change the invariant. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // cleanup cover if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes { @@ -853,9 +861,10 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv ) return vRes; } -Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv ) +Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) { Vec_Int_t * vRes = NULL; + abctime clk = Abc_Clock(); int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0; Pdr_ForEachCube( pList, pCube, i ) { @@ -864,19 +873,21 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv ) { int Save = pCube[k+1]; pCube[k+1] = -1; - if ( Pdr_InvCheck(p, vInv) ) + if ( Pdr_InvCheck(p, vInv, 0) ) { pCube[k+1] = Save; continue; } + if ( fVerbose ) printf( "Removing lit %d from clause %d.\n", k, i ); nRemoved++; } } if ( nRemoved ) - printf( "Invariant minimization reduced %d literals (out of %d).\n", nRemoved, nLits ); + printf( "Invariant minimization reduced %d literals (out of %d). ", nRemoved, nLits ); else - printf( "Invariant minimization did not change the invariant.\n" ); + printf( "Invariant minimization did not change the invariant. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( nRemoved > 0 ) // finished without timeout and removed some lits { vRes = Vec_IntAlloc( 1000 ); -- cgit v1.2.3