diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 20:35:07 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 20:35:07 +0000 |
| commit | 43a09137c2abd4902ce622afa445a9cb59e2352d (patch) | |
| tree | 3086a6af95a29af036a7b28a08fb3fd56d60a051 /src/smt/smt_engine.h | |
| parent | e31f8ec3eeacff9b7818287eaa9b58ebc9cd3958 (diff) | |
Moved some things around in the preprocessor. Now theory preprocessing gets
called before ite simplification unless arithrewriteequality is on
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0873aea96..11f3bdcb9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -163,6 +163,11 @@ class CVC4_PUBLIC SmtEngine { */ bool d_needPostsolve; + /* + * Whether to call theory preprocessing during simplification - on by default* but gets turned off if arithRewriteEq is on + */ + bool d_earlyTheoryPP; + /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */ unsigned long d_timeBudgetCumulative; /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ |