Skip to content

A
abc
Commit cf1106ab by Alan Mishchenko
Options

Adding features for invariant minimization.

parent c3dfec74
Showing with 35 additions and 24 deletions
src/base/wlc/wlcCom.c
...@@ -601,7 +601,7 @@ usage: ...@@ -601,7 +601,7 @@ usage:
******************************************************************************/ ******************************************************************************/
int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv ) 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; int c, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
...@@ -622,7 +622,7 @@ int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -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" ); Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
return 0; return 0;
} }
Pdr_InvPrint( Wlc_AbcGetInv(pAbc) ); Pdr_InvPrint( Wlc_AbcGetInv(pAbc), fVerbose );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: inv_print [-vh]\n" ); Abc_Print( -2, "usage: inv_print [-vh]\n" );
...@@ -646,7 +646,7 @@ usage: ...@@ -646,7 +646,7 @@ usage:
******************************************************************************/ ******************************************************************************/
int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) 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; int c, nFailed, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
...@@ -677,7 +677,7 @@ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -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" ); Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
return 0; return 0;
} }
nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) ); nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose );
if ( nFailed ) if ( nFailed )
printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) );
else else
...@@ -811,8 +811,8 @@ usage: ...@@ -811,8 +811,8 @@ usage:
******************************************************************************/ ******************************************************************************/
int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) 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_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 ); extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
Vec_Int_t * vInv, * vInv2; Vec_Int_t * vInv, * vInv2;
int c, fLits = 0, fVerbose = 0; int c, fLits = 0, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
...@@ -849,9 +849,9 @@ int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -849,9 +849,9 @@ int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
} }
if ( fLits ) if ( fLits )
vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv ); vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv, fVerbose );
else else
vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv ); vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv, fVerbose );
if ( vInv2 ) if ( vInv2 )
Abc_FrameSetInv( vInv2 ); Abc_FrameSetInv( vInv2 );
return 0; return 0;
......
src/proof/pdr/pdrInv.c
...@@ -678,17 +678,20 @@ Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts ) ...@@ -678,17 +678,20 @@ Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts )
Vec_IntFree( vMap ); Vec_IntFree( vMap );
return vStr; 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( "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 ) ); if ( fVerbose )
Vec_IntFree( vCounts ); {
Vec_StrFree( vStr ); 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 nBTLimit = 0;
int i, k, status, nFailed = 0; int i, k, status, nFailed = 0;
...@@ -696,7 +699,7 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ) ...@@ -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 ); Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
// collect cubes // collect cubes
int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0]; int * pCube, * pList = Vec_IntArray(vInv);
// create variables // create variables
Vec_Int_t * vLits = Vec_IntAlloc(100); Vec_Int_t * vLits = Vec_IntAlloc(100);
int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p); int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
...@@ -731,6 +734,8 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ) ...@@ -731,6 +734,8 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
continue; continue;
assert( status == l_True ); assert( status == l_True );
nFailed++; nFailed++;
if ( fVerbose )
printf( "Verification failed for clause %d.\n", i );
} }
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
sat_solver_delete( pSat ); sat_solver_delete( pSat );
...@@ -738,10 +743,11 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ) ...@@ -738,10 +743,11 @@ int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
return nFailed; 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 nBTLimit = 0;
int fCheckProperty = 0; int fCheckProperty = 1;
abctime clk = Abc_Clock();
int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0; int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0;
Vec_Int_t * vRes = NULL; Vec_Int_t * vRes = NULL;
// create SAT solver // create SAT solver
...@@ -827,14 +833,16 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv ) ...@@ -827,14 +833,16 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
break; break;
if ( fCannot ) if ( fCannot )
continue; continue;
if ( fVerbose )
printf( "Removing clause %d.\n", i ); printf( "Removing clause %d.\n", i );
Vec_BitWriteEntry( vRemoved, i, 1 ); Vec_BitWriteEntry( vRemoved, i, 1 );
nRemoved++; nRemoved++;
} }
if ( 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 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 // cleanup cover
if ( !fFailed && nRemoved > 0 ) // finished without timeout and removed some cubes 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 ) ...@@ -853,9 +861,10 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
return vRes; 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; Vec_Int_t * vRes = NULL;
abctime clk = Abc_Clock();
int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0; int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0;
Pdr_ForEachCube( pList, pCube, i ) Pdr_ForEachCube( pList, pCube, i )
{ {
...@@ -864,19 +873,21 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv ) ...@@ -864,19 +873,21 @@ Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv )
{ {
int Save = pCube[k+1]; int Save = pCube[k+1];
pCube[k+1] = -1; pCube[k+1] = -1;
if ( Pdr_InvCheck(p, vInv) ) if ( Pdr_InvCheck(p, vInv, 0) )
{ {
pCube[k+1] = Save; pCube[k+1] = Save;
continue; continue;
} }
if ( fVerbose )
printf( "Removing lit %d from clause %d.\n", k, i ); printf( "Removing lit %d from clause %d.\n", k, i );
nRemoved++; nRemoved++;
} }
} }
if ( 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 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 if ( nRemoved > 0 ) // finished without timeout and removed some lits
{ {
vRes = Vec_IntAlloc( 1000 ); vRes = Vec_IntAlloc( 1000 );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment