summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c18
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmc3.c19
3 files changed, 28 insertions, 10 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d82c1f80..a498761e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -21505,7 +21505,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLaxdruvzh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdruvzh" ) ) != EOF )
{
switch ( c )
{
@@ -21650,6 +21650,15 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
pLogFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
+ case 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-W\" should be followed by a file name.\n" );
+ goto usage;
+ }
+ pPars->pLogFileName = argv[globalUtilOptind];
+ globalUtilOptind++;
+ break;
case 'a':
pPars->fSolveAll ^= 1;
break;
@@ -21728,7 +21737,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-L file] [-axduvzh]\n" );
+ Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axduvzh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
@@ -21740,9 +21749,10 @@ usage:
Abc_Print( -2, "\t-J num : the number of timeframes to jump (0 = not used) [default = %d]\n", pPars->nFramesJump );
Abc_Print( -2, "\t-I num : the number of PIs to abstract [default = %d]\n", pPars->nPisAbstract );
Abc_Print( -2, "\t-P num : the max number of learned clauses to keep (0=unused) [default = %d]\n", pPars->nLearnedStart );
- Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta );
- Abc_Print( -2, "\t-R num : percentage to keep for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
+ Abc_Print( -2, "\t-Q num : delta value for learned clause removal [default = %d]\n", pPars->nLearnedDelta );
+ Abc_Print( -2, "\t-R num : percentage to keep for learned clause removal [default = %d]\n", pPars->nLearnedPerce );
Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
+ Abc_Print( -2, "\t-W file: the log file name with per-output details [default = %s]\n", pPars->pLogFileName ? pPars->pLogFileName : "no logging" );
Abc_Print( -2, "\t-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", pPars->fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dropping (replacing by 0) SAT outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index b3e2d8e8..0bc7bb3f 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
int nLearnedPerce; // ratio of learned clause limit
int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
+ char * pLogFileName; // log file name
int fSilent; // completely silent
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 14371d60..90706f6f 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1392,13 +1392,16 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew, * pCexNew0;
+ FILE * pLogFile = NULL;
unsigned * pInfo;
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int i, f, k, Lit, status;
- abctime clk, clk2, clkOther = 0, clkTotal = Abc_Clock();
+ abctime clk, clk2, clkSatRun, clkOther = 0, clkTotal = Abc_Clock();
abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
abctime nTimeToStopNG, nTimeToStop;
+ if ( pPars->pLogFileName )
+ pLogFile = fopen( pPars->pLogFileName, "wb" );
if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
@@ -1542,15 +1545,17 @@ clkOther += Abc_Clock() - clk2;
// solve this output
fUnfinished = 0;
sat_solver_compress( p->pSat );
-clk2 = Abc_Clock();
if ( p->pTime4Outs )
{
assert( p->pTime4Outs[i] > 0 );
clkOne = Abc_Clock();
sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
}
-// status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+clk2 = Abc_Clock();
status = Saig_ManCallSolver( p, Lit );
+clkSatRun = Abc_Clock() - clk2;
+ if ( pLogFile )
+ fprintf( pLogFile, "Frame %5d Output %5d Time(ms) %8d\n", f, i, Lit < 2 ? 0 : clkSatRun );
if ( p->pTime4Outs )
{
abctime timeSince = Abc_Clock() - clkOne;
@@ -1561,7 +1566,7 @@ clk2 = Abc_Clock();
}
if ( status == l_False )
{
-nTimeUnsat += Abc_Clock() - clk2;
+nTimeUnsat += clkSatRun;
if ( Lit != 0 )
{
// add final unit clause
@@ -1584,7 +1589,7 @@ nTimeUnsat += Abc_Clock() - clk2;
}
else if ( status == l_True )
{
-nTimeSat += Abc_Clock() - clk2;
+nTimeSat += clkSatRun;
RetValue = 0;
fFirst = 0;
if ( !pPars->fSolveAll )
@@ -1671,7 +1676,7 @@ nTimeSat += Abc_Clock() - clk2;
}
else
{
-nTimeUndec += Abc_Clock() - clk2;
+nTimeUndec += clkSatRun;
assert( status == l_Undef );
if ( pPars->nFramesJump )
{
@@ -1735,6 +1740,8 @@ finish:
}
Saig_Bmc3ManStop( p );
fflush( stdout );
+ if ( pLogFile )
+ fclose( pLogFile );
return RetValue;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-10 23:48:49 +0000