diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-17 19:07:22 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-17 19:07:22 +0200 |
commit | 3fc5f5df9a887469cdd9183ca5793578cfb773cb (patch) | |
tree | b7d4dec8f62ac5fb69f5563ab688ec75c60e9997 /src | |
parent | 490f664c35d717d5bd01f43f3026fb2abf3e99ff (diff) |
Do extended rewrite on results of quantifier elimination. (#2119)
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5d9f08343..69c0dab9c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5743,6 +5743,9 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) }else{ ret_n = NodeManager::currentNM()->mkConst(n_e.getKind() != kind::EXISTS); } + // do extended rewrite to minimize the size of the formula aggressively + theory::quantifiers::ExtendedRewriter extr(true); + ret_n = extr.extendedRewrite(ret_n); return ret_n.toExpr(); }else { return NodeManager::currentNM() |