From 3119e1e30f8a44eb6236792c69f8cca64c99f7a8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 25 Jan 2017 13:56:16 -0800 Subject: Adding features for invariant minimization. --- src/base/wlc/wlcCom.c | 2 +- src/proof/pdr/pdrInv.c | 102 +++++++++++++++++++++++++++++++++++-------------- 2 files changed, 74 insertions(+), 30 deletions(-) diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index be9ba7f6..2828fea3 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -681,7 +681,7 @@ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nFailed ) printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); else - printf( "Invariant verification passes.\n" ); + printf( "Invariant verification succeeded.\n" ); return 0; usage: Abc_Print( -2, "usage: inv_check [-vh]\n" ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 19e6c90e..bd32953a 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -691,20 +691,17 @@ void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose ) } } -int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) +int Pdr_InvCheck_int( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose, sat_solver * pSat ) { int nBTLimit = 0; - int i, k, status, nFailed = 0; - // create SAT solver - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); - sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + int fCheckProperty = 1; + int i, k, status, nFailed = 0, nFailedOuts = 0; // collect cubes int * pCube, * pList = Vec_IntArray(vInv); // create variables Vec_Int_t * vLits = Vec_IntAlloc(100); - int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p); + int iFoVarBeg = sat_solver_nvars(pSat) - Gia_ManRegNum(p); int iFiVarBeg = 1 + Gia_ManPoNum(p); - assert( Gia_ManPoNum(p) == 1 ); // add cubes Pdr_ForEachCube( pList, pCube, i ) { @@ -713,10 +710,34 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) for ( k = 0; k < pCube[0]; k++ ) if ( pCube[k+1] != -1 ) Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) ); + if ( Vec_IntSize(vLits) == 0 ) + { + Vec_IntFree( vLits ); + return 1; + } // add it to the solver status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ); assert( status == 1 ); } + // verify property output + if ( fCheckProperty ) + { + for ( i = 0; i < Gia_ManPoNum(p); i++ ) + { + Vec_IntFill( vLits, 1, Abc_Var2Lit(1+i, 0) ); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) // timeout + break; + if ( status == l_True ) // sat - property fails + { + if ( fVerbose ) + printf( "Coverage check failed for output %d.\n", i ); + nFailedOuts++; + continue; + } + assert( status == l_False ); // unsat - property holds + } + } // iterate through cubes in the direct order Pdr_ForEachCube( pList, pCube, i ) { @@ -735,12 +756,22 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) assert( status == l_True ); nFailed++; if ( fVerbose ) - printf( "Verification failed for clause %d.\n", i ); + printf( "Inductiveness check failed for clause %d.\n", i ); } + Vec_IntFree( vLits ); + return nFailed + nFailedOuts; +} + +int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) +{ + int RetValue; + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + assert( sat_solver_nvars(pSat) == pCnf->nVars ); Cnf_DataFree( pCnf ); + RetValue = Pdr_InvCheck_int( p, vInv, fVerbose, pSat ); sat_solver_delete( pSat ); - Vec_IntFree( vLits ); - return nFailed; + return RetValue; } Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) @@ -760,8 +791,8 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p); int iFiVarBeg = 1 + Gia_ManPoNum(p); int iAuxVarBeg = sat_solver_nvars(pSat); - assert( Gia_ManPoNum(p) == 1 ); // allocate auxiliary variables + assert( sat_solver_nvars(pSat) == pCnf->nVars ); sat_solver_setnvars( pSat, sat_solver_nvars(pSat) + nCubes ); // add clauses Pdr_ForEachCube( pList, pCube, i ) @@ -785,25 +816,28 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) if ( k != i && !Vec_BitEntry(vRemoved, k) ) // skip this cube and already removed cubes Vec_IntPush( vLits, Abc_Var2Lit(iAuxVarBeg + k, 0) ); // pos aux literal nLits = Vec_IntSize( vLits ); - // check if the property still holds if ( fCheckProperty ) { - Vec_IntPush( vLits, Abc_Var2Lit(1, 0) ); - status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); - if ( status == l_Undef ) // timeout + for ( k = 0; k < Gia_ManPoNum(p); k++ ) { - fFailed = 1; - break; + Vec_IntShrink( vLits, nLits ); + Vec_IntPush( vLits, Abc_Var2Lit(1+k, 0) ); + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) // timeout + { + fFailed = 1; + break; + } + if ( status == l_True ) // sat - property fails + break; + assert( status == l_False ); // unsat - property holds } - if ( status == l_True ) // sat - property fails - { - //printf( "property fails if clause %d is removed\n", i ); + if ( fFailed ) + break; + if ( k < Gia_ManPoNum(p) ) continue; - } - assert( status == l_False ); // unsat - property holds } - // check other clauses fCannot = 0; Pdr_ForEachCube( pList, pCube, n ) @@ -866,6 +900,9 @@ 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; + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat; +// sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); Pdr_ForEachCube( pList, pCube, i ) { nLits += pCube[0]; @@ -873,16 +910,23 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ) { int Save = pCube[k+1]; pCube[k+1] = -1; - if ( Pdr_InvCheck(p, vInv, 0) ) - { + //sat_solver_bookmark( pSat ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( Pdr_InvCheck_int(p, vInv, 0, pSat) ) pCube[k+1] = Save; - continue; + else + { + if ( fVerbose ) + printf( "Removing lit %d from clause %d.\n", k, i ); + nRemoved++; } - if ( fVerbose ) - printf( "Removing lit %d from clause %d.\n", k, i ); - nRemoved++; + sat_solver_delete( pSat ); + //sat_solver_rollback( pSat ); + //sat_solver_bookmark( pSat ); } } + Cnf_DataFree( pCnf ); + //sat_solver_delete( pSat ); if ( nRemoved ) printf( "Invariant minimization reduced %d literals (out of %d). ", nRemoved, nLits ); else -- cgit v1.2.3