summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-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
4 files changed, 47 insertions, 29 deletions
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" );
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-25 12:52:50 +0000