From b65ae7349af7de36390ec916701b997cac2a00ed Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Dec 2012 09:47:48 -0800 Subject: Enabling multi-output solving in 'pdr'. --- src/proof/pdr/pdr.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/proof/pdr/pdr.h') 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 -- cgit v1.2.3