Skip to content

A
abc
Commit e639e8fd by Alan Mishchenko
Options

Integrating SAT-based CEX minimization.

parent c618cee6
Showing with 145 additions and 10 deletions
src/aig/gia/giaCex.c
......@@ -422,8 +422,8 @@ Gia_Man_t * Gia_ManFramesForCexMin( Gia_Man_t * p, int nFrames )
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
pFrames = Gia_ManCleanup( pTemp = pFrames );
printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
//printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
// Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
Gia_ManStop( pTemp );
return pFrames;
}
......@@ -499,6 +499,110 @@ void Gia_ManMinCex( Gia_Man_t * p, Abc_Cex_t * pCex )
Gia_ManStop( pFrames );
}
Abc_Cex_t * Bmc_CexCareDeriveCex( Abc_Cex_t * pCex, int iFirstVar, int * pLits, int nLits )
{
Abc_Cex_t * pCexMin; int i;
pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 );
pCexMin->iPo = pCex->iPo;
pCexMin->iFrame = pCex->iFrame;
for ( i = 0; i < nLits; i++ )
{
int PiNum = Abc_Lit2Var(pLits[i]) - iFirstVar;
assert( PiNum >= 0 && PiNum < pCex->nBits - pCex->nRegs );
Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + PiNum );
}
return pCexMin;
}
Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose )
{
abctime clk = Abc_Clock();
int n, i, iFirstVar, iLit, status;
Vec_Int_t * vLits;
sat_solver * pSat;
Cnf_Dat_t * pCnf;
int nFinal, * pFinal;
Abc_Cex_t * pCexBest = NULL;
int CountBest = 0;
Gia_Man_t * pFrames;
// CEX minimization
clk = Abc_Clock();
pCexBest = Bmc_CexCareMinimizeAig( p, Gia_ManPiNum(p), pCex, 1, 1, fVerbose );
for ( i = pCexBest->nRegs; i < pCexBest->nBits; i++ )
CountBest += Abc_InfoHasBit(pCexBest->pData, i);
if ( fVerbose )
{
printf( "Care bits = %d. ", CountBest );
Abc_PrintTime( 1, "Non-SAT-based CEX minimization", Abc_Clock() - clk );
}
// SAT instance
clk = Abc_Clock();
pFrames = Gia_ManFramesForCexMin( p, pCex->iFrame + 1 );
pCnf = (Cnf_Dat_t*)Mf_ManGenerateCnf( pFrames, 8, 0, 0, 0, 0 );
iFirstVar = pCnf->nVars - (pCex->iFrame+1) * pCex->nPis;
pSat = (sat_solver*)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
iLit = Abc_Var2Lit( 1, 1 );
status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
assert( status );
// create literals
vLits = Vec_IntAlloc( 100 );
for ( i = pCex->nRegs; i < pCex->nBits; i++ )
Vec_IntPush( vLits, Abc_Var2Lit(iFirstVar + i - pCex->nRegs, !Abc_InfoHasBit(pCex->pData, i)) );
if ( fVerbose )
Abc_PrintTime( 1, "Constructing SAT solver", Abc_Clock() - clk );
for ( n = 0; n < 2; n++ )
{
if ( n ) Vec_IntReverseOrder( vLits );
// SAT-based minimization
clk = Abc_Clock();
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
nFinal = sat_solver_final( pSat, &pFinal );
if ( fVerbose )
{
printf( "Status %s Selected %5d assumptions out of %5d. ", status == l_False ? "OK ":"BUG", nFinal, Vec_IntSize(vLits) );
Abc_PrintTime( 1, "Analyze_final", Abc_Clock() - clk );
}
if ( CountBest > nFinal )
{
CountBest = nFinal;
ABC_FREE( pCexBest );
pCexBest = Bmc_CexCareDeriveCex( pCex, iFirstVar, pFinal, nFinal );
}
if ( !fHighEffort )
continue;
// SAT-based minimization
clk = Abc_Clock();
nFinal = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits), 0 );
if ( fVerbose )
{
printf( "Status %s Selected %5d assumptions out of %5d. ", status == l_False ? "OK ":"BUG", nFinal, Vec_IntSize(vLits) );
Abc_PrintTime( 1, "LEXUNSAT ", Abc_Clock() - clk );
}
if ( CountBest > nFinal )
{
CountBest = nFinal;
ABC_FREE( pCexBest );
pCexBest = Bmc_CexCareDeriveCex( pCex, iFirstVar, Vec_IntArray(vLits), nFinal );
}
}
if ( fVerbose )
{
printf( "Final : " );
Bmc_CexPrint( pCexBest, pCexBest->nPis, 0 );
}
// cleanup
Vec_IntFree( vLits );
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pFrames );
return pCexBest;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/io/io.c
......@@ -2310,6 +2310,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
char * pFileName;
int c, fNames = 0;
int fMinimize = 0;
int fUseSatBased = 0;
int fHighEffort = 0;
int fUseOldMin = 0;
int fCheckCex = 0;
int forceSeq = 0;
......@@ -2318,7 +2320,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "snmocafvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafvh" ) ) != EOF )
{
switch ( c )
{
......@@ -2331,6 +2333,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
case 'm':
fMinimize ^= 1;
break;
case 'u':
fUseSatBased ^= 1;
break;
case 'e':
fHighEffort ^= 1;
break;
case 'o':
fUseOldMin ^= 1;
break;
......@@ -2419,6 +2427,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
if ( fCheckCex )
Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
}
else if ( fUseSatBased )
pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
else
pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose );
Aig_ManStop( pAig );
......@@ -2477,19 +2487,21 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: write_cex [-snmocfvh] <file>\n" );
fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
fprintf( pAbc->Err, "usage: write_cex [-snmueocfvh] <file>\n" );
fprintf( pAbc->Err, "\t saves counter-example (CEX) derived by \"sat\", \"iprove\", \"dprove\", etc\n" );
fprintf( pAbc->Err, "\t the output file <file> contains values for each PI in natural order\n" );
fprintf( pAbc->Err, "\t-s : always report a sequential CEX (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
fprintf( pAbc->Err, "\t-m : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
fprintf( pAbc->Err, "\t-o : use old counter-example minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
fprintf( pAbc->Err, "\t-c : check generated counter-example using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
fprintf( pAbc->Err, "\t-u : use SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" );
fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" );
fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s].\n", fAiger? "yes": "no" );
fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" );
fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
fprintf( pAbc->Err, "\t<file> : the name of the file to write\n" );
return 1;
}
......
src/sat/bmc/bmc.h
......@@ -217,6 +217,8 @@ extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t *
extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
extern Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
/*=== bmcCexCut.c ==========================================================*/
extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
......
src/sat/bmc/bmcCexCare.c
......@@ -430,6 +430,23 @@ Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex,
Gia_ManStop( pGia );
return pCexMin;
}
Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose )
{
Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
Abc_Cex_t * pCexMin = Bmc_CexCareSatBasedMinimizeAig( pGia, pCex, fHighEffort, fVerbose );
if ( pCexMin == NULL )
{
Gia_ManStop( pGia );
return NULL;
}
// verify and return
if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
printf( "Counter-example verification has failed.\n" );
else if ( fCheck )
printf( "Counter-example verification succeeded.\n" );
Gia_ManStop( pGia );
return pCexMin;
}
/**Function*************************************************************
......
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