diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-24 18:45:42 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-06-24 18:45:42 -0700 |
| commit | 7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e (patch) | |
| tree | c1c899e41b24c4cf239e8ed5b3dbb7727376fc93 /src/proof/pdr/pdrCore.c | |
| parent | 2f64033b3767ffdb16d8a530d813e39ee53b6e73 (diff) | |
| download | abc-7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e.tar.gz abc-7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e.tar.bz2 abc-7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e.zip | |
Added min-cut-based refinement of gate-level abstraction (command &gla_refine).
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 3cf47a92..f863a881 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -706,6 +706,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, ***********************************************************************/ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) { + if ( pPars->fVerbose ) + { // Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" ); Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut ); @@ -713,6 +715,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) Abc_Print( 1, "Output = %d. ", pPars->iOutput ); Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" ); + } /* Vec_Int_t * vPrioInit = NULL; |