diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-25 13:47:38 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-25 13:47:38 -0700 |
commit | 1d26d58a17226230b40601c3dc40ef4851827a2e (patch) | |
tree | 847daf199197cc1f2f2f356458f579f60c8ebf9e /src/proof/pdr | |
parent | 58c81ec097d66abdd1ec77853cdcc95f842f12f2 (diff) | |
download | abc-1d26d58a17226230b40601c3dc40ef4851827a2e.tar.gz abc-1d26d58a17226230b40601c3dc40ef4851827a2e.tar.bz2 abc-1d26d58a17226230b40601c3dc40ef4851827a2e.zip |
Adding switch 'pdr -o' to control using property output in induction.
Diffstat (limited to 'src/proof/pdr')
-rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrSat.c | 2 |
3 files changed, 4 insertions, 0 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index e4b764a1..3dffac17 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -63,6 +63,7 @@ struct Pdr_Par_t_ int fSolveAll; // do not stop when found a SAT output int fStoreCex; // enable storing counter-examples in MO mode int fUseBridge; // use bridge interface + int fUsePropOut; // use property output int nFailOuts; // the number of failed outputs int nDropOuts; // the number of timed out outputs int nProveOuts; // the number of proved outputs diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 8e81795b..5b619f4b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -61,6 +61,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fMonoCnf = 0; // monolythic CNF pPars->fDumpInv = 0; // dump inductive invariant pPars->fShortest = 0; // forces bug traces to be shortest + pPars->fUsePropOut = 1; // use property output pPars->fVerbose = 0; // verbose output pPars->fVeryVerbose = 0; // very verbose output pPars->fNotVerbose = 0; // not printing line-by-line progress diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index f3681adb..2e6130aa 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -179,6 +179,8 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) sat_solver * pSat; Aig_Obj_t * pObj; int Lit, RetValue, i; + if ( !p->pPars->fUsePropOut ) + return; pSat = Pdr_ManSolver(p, k); Saig_ManForEachPo( p->pAig, pObj, i ) { |