summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaCex.c108
-rw-r--r--src/base/io/io.c28
-rw-r--r--src/sat/bmc/bmc.h2
-rw-r--r--src/sat/bmc/bmcCexCare.c17
4 files changed, 145 insertions, 10 deletions
diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c
index 88e8c717..edd5c87d 100644
--- a/src/aig/gia/giaCex.c
+++ b/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 ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index b047bf92..11b1fa57 100644
--- a/src/base/io/io.c
+++ b/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;
}
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 1d5180f3..71a33595 100644
--- a/src/sat/bmc/bmc.h
+++ b/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 );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index cc3e85ea..8db92444 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/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*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-12 22:33:03 +0000