summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c49
-rw-r--r--src/base/abci/abcDar.c7
-rw-r--r--src/misc/vec/vecPtr.h3
-rw-r--r--src/proof/pdr/pdr.h1
-rw-r--r--src/proof/pdr/pdrCore.c6
-rw-r--r--src/proof/ssw/ssw.h2
-rw-r--r--src/proof/ssw/sswRarity.c67
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmc3.c11
9 files changed, 103 insertions, 44 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c53133d1..56aaed9e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2301,10 +2301,24 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->vCexVec )
{
Abc_Cex_t * pTemp;
+ int nCexes = 0;
+ int Counter = 0;
printf( "\n" );
Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
+ {
+ if ( pTemp == (void *)(ABC_PTRINT_T)1 )
+ {
+ Counter++;
+ continue;
+ }
if ( pTemp )
+ {
+ printf( "%4d : ", ++nCexes );
Abc_CexPrintStats( pTemp );
+ }
+ }
+ if ( Counter )
+ printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
}
}
return 0;
@@ -17749,7 +17763,8 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
int TimeOut;
int fSolveAll;
int fVerbose;
- extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose );
+ int fNotVerbose;
+ extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose );
// set defaults
nFrames = 20;
nWords = 50;
@@ -17760,9 +17775,10 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
TimeOut = 0;
fSolveAll = 0;
fVerbose = 0;
+ fNotVerbose= 0;
// parse command line
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavzh" ) ) != EOF )
{
switch ( c )
{
@@ -17849,6 +17865,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
+ case 'z':
+ fNotVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -17866,13 +17885,18 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
ABC_FREE( pNtk->pSeqModel );
- pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose );
+ pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose );
// pAbc->nFrames = pAbc->pCex->iFrame;
Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
+ if ( pNtk->vSeqModelVec )
+ {
+ Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+ pAbc->nFrames = -1;
+ }
return 0;
usage:
- Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-avh]\n" );
+ Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-avzh]\n" );
Abc_Print( -2, "\t performs random simulation of the sequential miter\n" );
Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
@@ -17883,6 +17907,7 @@ usage:
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
Abc_Print( -2, "\t-a : solve all outputs (do not stop when one is SAT) [default = %s]\n", fSolveAll? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -20781,7 +20806,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, "SFTCDJILadruvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILadruvzh" ) ) != EOF )
{
switch ( c )
{
@@ -20883,6 +20908,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
pPars->fVerbose ^= 1;
break;
+ case 'z':
+ pPars->fNotVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -20941,7 +20969,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-aduvh]\n" );
+ Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-aduvzh]\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 );
@@ -20955,6 +20983,7 @@ usage:
Abc_Print( -2, "\t-d : drops (replaces by 0) satisfiable outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -22337,7 +22366,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwzh" ) ) != EOF )
{
switch ( c )
{
@@ -22433,6 +22462,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'w':
pPars->fVeryVerbose ^= 1;
break;
+ case 'z':
+ pPars->fNotVerbose ^= 1;
+ break;
case 'h':
default:
goto usage;
@@ -22465,7 +22497,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwh]\n" );
+ Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -22483,6 +22515,7 @@ usage:
Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 424ab14c..8ca40bc0 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3273,7 +3273,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
SeeAlso []
***********************************************************************/
-int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose )
+int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose )
{
Aig_Man_t * pMan;
int status, RetValue = -1;
@@ -3284,7 +3284,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
}
pMan = Abc_NtkToDar( pNtk, 0, 1 );
- if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose ) == 0 )
+ if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ) == 0 )
{
if ( pMan->pSeqModel )
{
@@ -3304,6 +3304,9 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
// Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
// nFrames, nWords );
}
+ if ( pNtk->vSeqModelVec )
+ Vec_PtrFreeFree( pNtk->vSeqModelVec );
+ pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
// ABC_PRT( "Time", clock() - clk );
Aig_ManStop( pMan );
return RetValue;
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 9aedbed4..731cf9a1 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -554,7 +554,8 @@ static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
int i;
if ( p == NULL ) return;
Vec_PtrForEachEntry( void *, p, pTemp, i )
- ABC_FREE( pTemp );
+ if ( pTemp != (void *)(ABC_PTRINT_T)1 && pTemp != (void *)(ABC_PTRINT_T)2 )
+ ABC_FREE( pTemp );
Vec_PtrFree( p );
}
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index a815bb30..c2243761 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -53,6 +53,7 @@ struct Pdr_Par_t_
int fSkipGeneral; // skips expensive generalization step
int fVerbose; // verbose output`
int fVeryVerbose; // very verbose output
+ int fNotVerbose; // not printing line by line progress
int fSilent; // totally silent execution
int fSolveAll; // do not stop when found a SAT output
int nFailOuts; // the number of failed outputs
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 46288925..314784d7 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -57,6 +57,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->fShortest = 0; // forces bug traces to be shortest
pPars->fVerbose = 0; // verbose output
pPars->fVeryVerbose = 0; // very verbose output
+ pPars->fNotVerbose = 0; // not printing line-by-line progress
pPars->iFrame = -1; // explored up to this frame
}
@@ -645,8 +646,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
pCex = Pdr_ManDeriveCex(p);
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex );
- Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
- nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
+ if ( !p->pPars->fNotVerbose )
+ Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
+ nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
Pdr_QueueClean( p );
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index 3ddcff37..4858ab89 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -118,7 +118,7 @@ extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_P
extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
/*=== sswRarity.c ===================================================*/
extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose );
+extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose );
/*=== sswSim.c ===================================================*/
extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 19dc3192..da96d218 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -546,7 +546,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
+int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time )
{
Aig_Obj_t * pObj;
int i;
@@ -556,12 +556,33 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
{
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
return 0;
- if ( Vec_PtrEntry(p->vCexes, i) )
+ if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
if ( !Ssw_RarManObjIsConst(p, pObj) )
{
p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
+
+ // remember the one solved
+ if ( pnSolvedNow )
+ {
+ (*pnSolvedNow)++;
+ if ( p->vCexes == NULL )
+ p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
+ assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
+ Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
+ // print final report
+ if ( !fNotVerbose )
+ {
+ int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
+ Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
+ nOutDigits, p->iFailPo, iFrame,
+ nOutDigits, *pnSolvedNow,
+ nOutDigits, Saig_ManPoNum(p->pAig) );
+ Abc_PrintTime( 1, "Time", Time );
+ }
+ continue;
+ }
return 1;
}
}
@@ -697,7 +718,6 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
p->vUpdConst = Vec_PtrAlloc( 100 );
p->vUpdClass = Vec_PtrAlloc( 100 );
p->vPatBests = Vec_IntAlloc( 100 );
- p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
return p;
}
@@ -714,7 +734,13 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
***********************************************************************/
static void Ssw_RarManStop( Ssw_RarMan_t * p )
{
- Vec_PtrFreeP( &p->vCexes );
+// Vec_PtrFreeP( &p->vCexes );
+ if ( p->vCexes )
+ {
+ assert( p->pAig->vSeqModelVec == NULL );
+ p->pAig->vSeqModelVec = p->vCexes;
+ p->vCexes = NULL;
+ }
if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
Vec_IntFreeP( &p->vInits );
Vec_IntFreeP( &p->vPatBests );
@@ -897,7 +923,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
SeeAlso []
***********************************************************************/
-int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose )
+int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose )
{
int fTryBmc = 0;
int fMiter = 1;
@@ -905,7 +931,6 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
int r, f = -1;
clock_t clk, clkTotal = clock();
clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
- int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int nNumRestart = 0;
int nSavedSeed = nRandSeed;
int RetValue = -1;
@@ -913,6 +938,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
int nSolved = 0;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
+ ABC_FREE( pAig->pSeqModel );
// consider the case of empty AIG
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
@@ -945,13 +971,13 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
for ( f = 0; f < nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
- if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
+ if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, fSolveAll ? &nSolved : NULL, r * p->nFrames + f, fNotVerbose, clock() - clkTotal) )
{
+ RetValue = 0;
if ( !fSolveAll )
{
if ( fVerbose ) Abc_Print( 1, "\n" );
// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
- ABC_FREE( pAig->pSeqModel );
Ssw_RarManPrepareRandom( nSavedSeed );
if ( fVerbose )
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
@@ -959,23 +985,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
- RetValue = 0;
goto finish;
}
- else
- {
- nSolved++;
- assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
- Vec_PtrWriteEntry( p->vCexes, p->iFailPo, p->vCexes );
- // print final report
- ABC_FREE( pAig->pSeqModel );
- Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
- nOutDigits, p->iFailPo, r * p->nFrames + f,
- nOutDigits, nSolved, nOutDigits, Saig_ManPoNum(p->pAig) );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
- RetValue = 0;
- }
-
}
// check timeout
if ( TimeOut && clock() > nTimeToStop )
@@ -985,6 +996,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
Abc_Print( 1, "Reached timeout (%d sec).\n", TimeOut );
goto finish;
}
+ // check if all outputs are solved by now
+ if ( fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
+ goto finish;
}
// get initialization patterns
if ( nRestart && r == nRestart )
@@ -1012,7 +1026,7 @@ finish:
if ( nSolved )
{
if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" );
- Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart, nSolved );
+ Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", nFrames, nNumRestart * nRestart + r, nNumRestart, nSolved, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
else if ( r == nRounds && f == nFrames )
@@ -1041,10 +1055,11 @@ finish:
int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fVerbose )
{
int fSolveAll = 0;
+ int fNotVerbose = 0;
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
- RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose );
+ RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose );
// save counter-example
Abc_CexFree( p->pCexSeq );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
@@ -1128,7 +1143,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
for ( f = 0; f < nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
- if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
+ if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, NULL, -1, -1, 0) )
{
if ( !fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 7cc5637b..bac4a2dd 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -54,6 +54,7 @@ struct Saig_ParBmc_t_
int nFfToAddMax; // max number of flops to add during CBA
int fSkipRand; // skip random decisions
int fVerbose; // verbose
+ int fNotVerbose; // skip line-by-line print-out
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 7ca5c7ba..cd965c06 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1305,6 +1305,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->fSolveAll = 0; // stops on the first SAT instance
p->fDropSatOuts = 0; // replace sat outputs by constant 0
p->fVerbose = 0; // verbose
+ p->fNotVerbose = 0; // skip line-by-line print-out
p->iFrame = -1; // explored up to this frame
p->nFailOuts = 0; // the number of failed outputs
}
@@ -1425,8 +1426,9 @@ clkOther += clock() - clk2;
return 0;
}
pPars->nFailOuts++;
- Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
- nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
+ if ( !pPars->fNotVerbose )
+ Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
+ nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
@@ -1498,8 +1500,9 @@ clkOther += clock() - clk2;
return 0;
}
pPars->nFailOuts++;
- Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
- nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
+ if ( !pPars->fNotVerbose )
+ Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
+ nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 03:12:40 +0000