diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-12 18:16:59 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-12 18:16:59 -0600 |
| commit | 1b0aa1c39ff7abe15bbd9305d376d10b007d69d0 (patch) | |
| tree | 987d3afa7231f9a21b22bd20afcdb62ed5c87743 /src/smt | |
| parent | 04114df7dd58bd7391704a94fe98e2935b39130d (diff) | |
Option to use extended rewriter as a preprocessing pass (#1600)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fdd72ba2e..7e2f6c38c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4293,6 +4293,16 @@ void SmtEnginePrivate::processAssertions() { bool noConflict = true; + if (options::extRewPrep()) + { + theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg()); + for (unsigned i = 0; i < d_assertions.size(); ++i) + { + Node a = d_assertions[i]; + d_assertions.replace(i, extr.extendedRewrite(a)); + } + } + // Unconstrained simplification if(options::unconstrainedSimp()) { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl; |