From 40bfe2fb88b4a4dc32fa280e66f66dcefb4a4b1d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 9 Nov 2020 13:24:07 -0800 Subject: Experiments with SAT sweeping. --- src/proof/cec/cecCore.c | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/proof/cec/cecCore.c') 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", -- cgit v1.2.3