diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 09:47:48 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 09:47:48 -0800 |
| commit | b65ae7349af7de36390ec916701b997cac2a00ed (patch) | |
| tree | 47ce553bcffa963d3debafc0459701a9f6d5ecaa /src/proof/pdr/pdr.h | |
| parent | 79aa1f00d6c00118442a240dab12d100e01fdd03 (diff) | |
| download | abc-b65ae7349af7de36390ec916701b997cac2a00ed.tar.gz abc-b65ae7349af7de36390ec916701b997cac2a00ed.tar.bz2 abc-b65ae7349af7de36390ec916701b997cac2a00ed.zip | |
Enabling multi-output solving in 'pdr'.
Diffstat (limited to 'src/proof/pdr/pdr.h')
| -rw-r--r-- | src/proof/pdr/pdr.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 491477dd..3c40d2d5 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -40,7 +40,7 @@ ABC_NAMESPACE_HEADER_START typedef struct Pdr_Par_t_ Pdr_Par_t; struct Pdr_Par_t_ { - int iOutput; // zero-based number of primary output to solve +// int iOutput; // zero-based number of primary output to solve int nRecycle; // limit on vars for recycling int nFrameMax; // limit on frame count int nConfLimit; // limit on SAT solver conflicts @@ -54,6 +54,8 @@ struct Pdr_Par_t_ int fVerbose; // verbose output` int fVeryVerbose; // very verbose output int fSilent; // totally silent execution + int fSolveAll; // do not stop when found a SAT output + int nFailOuts; // the number of failed outputs int iFrame; // explored up to this frame int RunId; // PDR id in this run int(*pFuncStop)(int); // callback to terminate |