summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c30
-rw-r--r--src/misc/util/utilCex.c5
-rw-r--r--src/proof/pdr/pdrCore.c2
-rw-r--r--src/sat/bmc/bmc.h2
-rw-r--r--src/sat/bmc/bmcBmc3.c130
-rw-r--r--src/sat/bmc/bmcICheck.c5
-rw-r--r--src/sat/bmc/bmcMulti.c52
7 files changed, 174 insertions, 52 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 69e8ed84..0ac0b7cf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32439,8 +32439,10 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->TimeOutGlo = 30;
pPars->TimeOutLoc = 2;
pPars->TimeOutInc = 100;
+ pPars->TimeOutGap = 0;
+ pPars->TimePerOut = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "TLMsdvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "TLMGHsdvwh" ) ) != EOF )
{
switch ( c )
{
@@ -32477,6 +32479,28 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->TimeOutInc <= 0 )
goto usage;
break;
+ case 'G':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->TimeOutGap = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->TimeOutGap <= 0 )
+ goto usage;
+ break;
+ case 'H':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->TimePerOut = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->TimePerOut <= 0 )
+ goto usage;
+ break;
case 's':
pPars->fUseSyn ^= 1;
break;
@@ -32507,11 +32531,13 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &mprove [-TLM num] [-sdvwh]\n" );
+ Abc_Print( -2, "usage: &mprove [-TLMGH num] [-sdvwh]\n" );
Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" );
Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", pPars->TimeOutGlo );
Abc_Print( -2, "\t-L num : approximate local runtime limit in seconds [default = %d]\n", pPars->TimeOutLoc );
Abc_Print( -2, "\t-M num : percentage of local runtime limit increase [default = %d]\n", pPars->TimeOutInc );
+ Abc_Print( -2, "\t-G num : approximate gap runtime limit in seconds [default = %d]\n", pPars->TimeOutGap );
+ Abc_Print( -2, "\t-H num : timeout per output in miliseconds [default = %d]\n", pPars->TimePerOut );
Abc_Print( -2, "\t-s : toggle using combinational synthesis [default = %s]\n", pPars->fUseSyn? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping invariant into a file [default = %s]\n", pPars->fDumpFinal? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index b0ce66be..1399f55d 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -351,7 +351,10 @@ void Abc_CexFreeP( Abc_Cex_t ** p )
{
if ( *p == NULL )
return;
- ABC_FREE( *p );
+ if ( *p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
+ *p = NULL;
+ else
+ ABC_FREE( *p );
}
/**Function*************************************************************
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 55c40c1e..50616fee 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -879,7 +879,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
abctime clk = Abc_Clock();
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
pPars->nTimeOutOne = 0;
- if ( pPars->nTimeOutOne )
+ if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
if ( pPars->fVerbose )
{
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 5d45c562..0cfc9b37 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -100,6 +100,8 @@ struct Bmc_MulPar_t_
int TimeOutGlo;
int TimeOutLoc;
int TimeOutInc;
+ int TimeOutGap;
+ int TimePerOut;
int fUseSyn;
int fDumpFinal;
int fVerbose;
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 16ed2b0b..72fbcc21 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1350,6 +1350,26 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit )
+{
+ if ( Lit == 0 )
+ return l_False;
+ if ( Lit == 1 )
+ return l_True;
+ return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+}
+
+/**Function*************************************************************
+
Synopsis [Bounded model checking engine.]
Description []
@@ -1363,7 +1383,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
- Abc_Cex_t * pCexNew;
+ Abc_Cex_t * pCexNew, * pCexNew0;
unsigned * pInfo;
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
@@ -1371,7 +1391,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
abctime clk, clk2, clkOther = 0, clkTotal = Abc_Clock();
abctime nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
abctime nTimeToStopNG, nTimeToStop;
- if ( pPars->nTimeOutOne )
+ if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
pPars->nTimeOutOne = 0;
@@ -1446,6 +1466,37 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
}
if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
continue;
+ // create CNF upfront
+ if ( pPars->fSolveAll )
+ {
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ if ( i >= Saig_ManPoNum(pAig) )
+ break;
+ // check for timeout
+ if ( pPars->nTimeOutGap && pPars->timeLastSolved && Abc_Clock() > pPars->timeLastSolved + pPars->nTimeOutGap * CLOCKS_PER_SEC )
+ {
+ Abc_Print( 1, "Reached gap timeout (%d seconds).\n", pPars->nTimeOutGap );
+ goto finish;
+ }
+ if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+ {
+ if ( !pPars->fSilent )
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
+ goto finish;
+ }
+ // skip solved outputs
+ if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
+ continue;
+ // skip output whose time has run out
+ if ( p->pTime4Outs && p->pTime4Outs[i] == 0 )
+ continue;
+ // add constraints for this output
+clk2 = Abc_Clock();
+ Saig_ManBmcCreateCnf( p, pObj, f );
+clkOther += Abc_Clock() - clk2;
+ }
+ }
// solve SAT
clk = Abc_Clock();
Saig_ManForEachPo( pAig, pObj, i )
@@ -1474,45 +1525,6 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
clk2 = Abc_Clock();
Lit = Saig_ManBmcCreateCnf( p, pObj, f );
clkOther += Abc_Clock() - clk2;
- if ( Lit == 0 )
- continue;
- if ( Lit == 1 )
- {
- RetValue = 0;
- if ( !pPars->fSolveAll )
- {
- Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
- Abc_Print( 1, "Output %d is trivially SAT in frame %d.\n", i, f );
- ABC_FREE( pAig->pSeqModel );
- pAig->pSeqModel = pCex;
- goto finish;
- }
- pPars->nFailOuts++;
- 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) );
- pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
- if ( p->pPars->fUseBridge )
- {
- Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
- Abc_CexFree( pCexNew );
- pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1;
- }
- Vec_PtrWriteEntry( p->vCexes, i, pCexNew );
- if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
- {
- Abc_Print( 1, "Quitting due to callback on fail.\n" );
- goto finish;
- }
- // reset the timeout
- pPars->timeLastSolved = Abc_Clock();
- nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
- if ( nTimeToStop )
- sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
- continue;
- }
// solve this output
fUnfinished = 0;
sat_solver_compress( p->pSat );
@@ -1523,7 +1535,8 @@ clk2 = Abc_Clock();
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 );
+// 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 );
+ status = Saig_ManCallSolver( p, Lit );
if ( p->pTime4Outs )
{
abctime timeSince = Abc_Clock() - clkOne;
@@ -1535,7 +1548,7 @@ clk2 = Abc_Clock();
if ( status == l_False )
{
nTimeUnsat += Abc_Clock() - clk2;
- if ( 1 )
+ if ( Lit != 0 )
{
// add final unit clause
Lit = lit_neg( Lit );
@@ -1591,15 +1604,18 @@ nTimeSat += Abc_Clock() - clk2;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
+ pCexNew0 = NULL;
if ( p->pPars->fUseBridge )
{
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
- Abc_CexFree( pCexNew );
+ //Abc_CexFree( pCexNew );
+ pCexNew0 = pCexNew;
pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1;
}
Vec_PtrWriteEntry( p->vCexes, i, pCexNew );
if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
{
+ Abc_CexFreeP( &pCexNew0 );
Abc_Print( 1, "Quitting due to callback on fail.\n" );
goto finish;
}
@@ -1608,6 +1624,32 @@ nTimeSat += Abc_Clock() - clk2;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
if ( nTimeToStop )
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
+
+ // check if other outputs failed under the same counter-example
+ Saig_ManForEachPo( pAig, pObj, k )
+ {
+ if ( k >= Saig_ManPoNum(pAig) )
+ break;
+ // skip solved outputs
+ if ( p->vCexes && Vec_PtrEntry(p->vCexes, k) )
+ continue;
+ // check if this output is solved
+ Lit = Saig_ManBmcCreateCnf( p, pObj, f );
+ if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
+ continue;
+ // write entry
+ pPars->nFailOuts++;
+ if ( !pPars->fNotVerbose )
+ Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
+ nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
+ // report to the bridge
+ if ( p->pPars->fUseBridge )
+ Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
+ // remember solved output
+ Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
+ }
+ Abc_CexFreeP( &pCexNew0 );
+ Abc_CexFree( pCexNew );
}
else
{
diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c
index 4376c336..17408e78 100644
--- a/src/sat/bmc/bmcICheck.c
+++ b/src/sat/bmc/bmcICheck.c
@@ -94,6 +94,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
Vec_Int_t * vLits;
Gia_Obj_t * pObj, * pObj0, * pObj1;
int i, k, iVar0, iVar1, iVarOut;
+ int VarShift = 0;
// start the SAT solver
pSat = sat_solver_new();
@@ -108,6 +109,8 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
// load the last timeframe
Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
+ VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p);
+
// add XOR clauses
Gia_ManForEachPo( p, pObj, i )
{
@@ -141,6 +144,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] );
// lift CNF again
Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars );
+ VarShift += pCnf->nVars;
// stitch the clauses
Gia_ManForEachRi( pMiter, pObj, i )
{
@@ -173,6 +177,7 @@ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pC
assert( 0 );
}
// sat_solver_compress( pSat );
+ Cnf_DataLiftGia( pCnf, pMiter, -VarShift );
Vec_IntFree( vLits );
return pSat;
}
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 35029034..cf04ab62 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -75,6 +75,34 @@ Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut,
/**Function*************************************************************
+ Synopsis [Counts the number of constant 0 POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManCountConst0PosGia( Gia_Man_t * p )
+{
+ Gia_Obj_t * pObj;
+ int i, Counter = 0;
+ Gia_ManForEachPo( p, pObj, i )
+ Counter += (Gia_ObjFaninLit0p(p, pObj) == 0);
+ return Counter;
+}
+int Gia_ManCountConst0Pos( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ Saig_ManForEachPo( p, pObj, i )
+ Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p));
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -138,18 +166,23 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Vec_Ptr_t * vCexes;
Aig_Man_t * pTemp;
abctime clkStart = Abc_Clock();
- int nTimeToStop = pPars->TimeOutGlo ? pPars->TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
+ abctime nTimeToStop = pPars->TimeOutGlo ? Abc_Clock() + pPars->TimeOutGlo * CLOCKS_PER_SEC : 0;
int nTotalPo = Saig_ManPoNum(p);
int nTotalSize = Aig_ManObjNum(p);
int TimeOutLoc = pPars->TimeOutLoc;
int i, RetValue = -1;
if ( pPars->fVerbose )
- printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n", pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
+ printf( "MultiProve parameters: Global timeout = %d sec. Local timeout = %d sec. Time increase = %d %%.\n",
+ pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
+ if ( pPars->fVerbose )
+ printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n",
+ pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose );
// create output map
vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
vCexes = Vec_PtrStart( Saig_ManPoNum(p) ); // maps solved outputs into their CEXes (or markers)
for ( i = 0; i < 1000; i++ )
{
+ int nSolved = Vec_PtrCountZero(vCexes);
// perform SIM3
Ssw_RarSetDefaultParams( pParsSim );
pParsSim->fSolveAll = 1;
@@ -157,6 +190,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
pParsSim->fSilent = !pPars->fVeryVerbose;
pParsSim->TimeOut = TimeOutLoc;
pParsSim->nRandSeed = (i * 17) % 500;
+ pParsSim->nWords = 5;
RetValue *= Ssw_RarSimulate( p, pParsSim );
// sort outputs
if ( p->vSeqModelVec )
@@ -173,7 +207,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
// check timeout
- if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
+ if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
@@ -185,6 +219,7 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
pParsBmc->fNotVerbose = 1;
pParsBmc->fSilent = !pPars->fVeryVerbose;
pParsBmc->nTimeOut = TimeOutLoc;
+ pParsBmc->nTimeOutOne = pPars->TimePerOut;
RetValue *= Saig_ManBmcScalable( p, pParsBmc );
if ( pPars->fVeryVerbose )
Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n",
@@ -204,12 +239,19 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
// check timeout
- if ( nTimeToStop && TimeOutLoc * CLOCKS_PER_SEC + Abc_Clock() > nTimeToStop )
+ if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
{
printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
break;
}
+ // check gap timeout
+ if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) )
+ {
+ printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap );
+ break;
+ }
+
// synthesize
if ( pPars->fUseSyn )
{
@@ -223,6 +265,8 @@ Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100;
}
Vec_IntFree( vOutMap );
+ if ( pPars->fVerbose )
+ printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) );
if ( pPars->fDumpFinal )
{
char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-16 20:43:13 +0000