Skip to content

A
abc
Commit 849f1807 by Alan Mishchenko
Options

Adding features for invariant minimization.

parent 876eb5a5
Showing with 92 additions and 19 deletions
src/base/wlc/wlcAbc.c
......@@ -176,7 +176,7 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
/**Function*************************************************************
Synopsis [Translate current network into an interpolant.]
Synopsis [Translate current network into an invariant.]
Description []
......
src/base/wlc/wlcCom.c
......@@ -646,8 +646,8 @@ usage:
******************************************************************************/
int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv );
int c, fVerbose = 0;
extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv );
int c, nFailed, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
......@@ -677,7 +677,11 @@ 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;
}
Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) );
nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) );
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" );
return 0;
usage:
Abc_Print( -2, "usage: inv_check [-vh]\n" );
......@@ -808,13 +812,17 @@ 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 );
Vec_Int_t * vInv, * vInv2;
int c, fVerbose = 0;
int c, fLits = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "lvh" ) ) != EOF )
{
switch ( c )
{
case 'l':
fLits ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -840,14 +848,18 @@ int Abc_CommandInvMin( 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;
}
vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv );
if ( fLits )
vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv );
else
vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv );
if ( vInv2 )
Abc_FrameSetInv( vInv2 );
return 0;
usage:
Abc_Print( -2, "usage: inv_min [-vh]\n" );
Abc_Print( -2, "\t minimizes the number of clauses in the current invariant\n" );
Abc_Print( -2, "usage: inv_min [-lvh]\n" );
Abc_Print( -2, "\t performs minimization of the current invariant\n" );
Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
Abc_Print( -2, "\t-l : toggle minimizing literals rather than clauses [default = %s]\n", fLits? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
......
src/proof/pdr/pdrInv.c
......@@ -688,7 +688,7 @@ void Pdr_InvPrint( Vec_Int_t * vInv )
Vec_StrFree( vStr );
}
void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
{
int nBTLimit = 0;
int i, k, status, nFailed = 0;
......@@ -699,7 +699,6 @@ void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
int * pCube, * pList = Vec_IntArray(vInv), nCubes = pList[0];
// create variables
Vec_Int_t * vLits = Vec_IntAlloc(100);
int nVars = Gia_ManRegNum(p);
int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
int iFiVarBeg = 1 + Gia_ManPoNum(p);
assert( Gia_ManPoNum(p) == 1 );
......@@ -709,7 +708,8 @@ void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
// collect literals
Vec_IntClear( vLits );
for ( k = 0; k < pCube[0]; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
if ( pCube[k+1] != -1 )
Vec_IntPush( vLits, Abc_Var2Lit(iFoVarBeg + Abc_Lit2Var(pCube[k+1]), !Abc_LitIsCompl(pCube[k+1])) );
// add it to the solver
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
assert( status == 1 );
......@@ -720,7 +720,8 @@ void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
// collect cube
Vec_IntClear( vLits );
for ( k = 0; k < pCube[0]; k++ )
Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
if ( pCube[k+1] != -1 )
Vec_IntPush( vLits, Abc_Var2Lit(iFiVarBeg + Abc_Lit2Var(pCube[k+1]), Abc_LitIsCompl(pCube[k+1])) );
// check if this cube intersects with the complement of other cubes in the solver
// if it does not intersect, then it is redundant and can be skipped
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
......@@ -731,18 +732,16 @@ void Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv )
assert( status == l_True );
nFailed++;
}
if ( nFailed )
printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, nCubes );
else
printf( "Invariant verification passes.\n" );
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
Vec_IntFree( vLits );
return nFailed;
}
Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
{
int nBTLimit = 0;
int fCheckProperty = 0;
int n, i, k, status, nLits, fFailed = 0, fCannot = 0, nRemoved = 0;
Vec_Int_t * vRes = NULL;
// create SAT solver
......@@ -752,7 +751,6 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
// create variables
Vec_Int_t * vLits = Vec_IntAlloc(100);
Vec_Bit_t * vRemoved = Vec_BitStart( nCubes );
int nVars = Gia_ManRegNum(p);
int iFoVarBeg = pCnf->nVars - Gia_ManRegNum(p);
int iFiVarBeg = 1 + Gia_ManPoNum(p);
int iAuxVarBeg = sat_solver_nvars(pSat);
......@@ -781,7 +779,26 @@ Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv )
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 );
// try removing other clauses
// 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
{
fFailed = 1;
break;
}
if ( status == l_True ) // sat - property fails
{
//printf( "property fails if clause %d is removed\n", i );
continue;
}
assert( status == l_False ); // unsat - property holds
}
// check other clauses
fCannot = 0;
Pdr_ForEachCube( pList, pCube, n )
{
......@@ -836,6 +853,50 @@ 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 * vRes = NULL;
int i, k, nLits = 0, * pCube, * pList = Vec_IntArray(vInv), nRemoved = 0;
Pdr_ForEachCube( pList, pCube, i )
{
nLits += pCube[0];
for ( k = 0; k < pCube[0]; k++ )
{
int Save = pCube[k+1];
pCube[k+1] = -1;
if ( Pdr_InvCheck(p, vInv) )
{
pCube[k+1] = Save;
continue;
}
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 );
else
printf( "Invariant minimization did not change the invariant.\n" );
if ( nRemoved > 0 ) // finished without timeout and removed some lits
{
vRes = Vec_IntAlloc( 1000 );
Vec_IntPush( vRes, pList[0] );
Pdr_ForEachCube( pList, pCube, i )
{
int nLits = 0;
for ( k = 0; k < pCube[0]; k++ )
if ( pCube[k+1] != -1 )
nLits++;
Vec_IntPush( vRes, nLits );
for ( k = 0; k < pCube[0]; k++ )
if ( pCube[k+1] != -1 )
Vec_IntPush( vRes, pCube[k+1] );
}
Vec_IntPush( vRes, Vec_IntEntryLast(vInv) );
}
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
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