diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-09 13:24:07 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-09 13:24:07 -0800 |
| commit | 40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d (patch) | |
| tree | 7d6e9b334e56967c5867e8d90e4f126a5fb914a1 /src/proof/cec/cecCore.c | |
| parent | 0b89fd387e71aeaf9595190eac2326a796ff6fc6 (diff) | |
| download | abc-40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d.tar.gz abc-40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d.tar.bz2 abc-40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d.zip | |
Experiments with SAT sweeping.
Diffstat (limited to 'src/proof/cec/cecCore.c')
| -rw-r--r-- | src/proof/cec/cecCore.c | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index 22b38cb9..1ae34278 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -348,6 +348,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSil Cec_ManPat_t * pPat; int i, fTimeOut = 0, nMatches = 0; abctime clk, clk2, clkTotal = Abc_Clock(); + if ( pPars->fVerbose ) + printf( "Simulating %d words for %d rounds. SAT solving with %d conflicts.\n", pPars->nWords, pPars->nRounds, pPars->nBTLimit ); // duplicate AIG and transfer equivalence classes Gia_ManRandom( 1 ); @@ -519,6 +521,9 @@ p->timeSat += Abc_Clock() - clk; } } finalize: + if ( pPars->fVerbose ) + printf( "Performed %d SAT calls: P = %d D = %d F = %d\n", + p->nAllProvedS + p->nAllDisprovedS + p->nAllFailedS, p->nAllProvedS, p->nAllDisprovedS, p->nAllFailedS ); if ( p->pPars->fVerbose && p->pAig ) { Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", |