diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-14 07:28:55 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-14 07:28:55 -0600 |
commit | eb6155c5f078a26b7cdddddad6e209fad0f825f8 (patch) | |
tree | be9519b18c6eb61e69af0966c4339c483a534af0 /src/preprocessing | |
parent | 9fd4e5758df5e1085a3d6c80e3a6162d61b36566 (diff) |
Updates to theory preprocess equality (#5776)
This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.
For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.
The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/theory_rewrite_eq.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp index 190b33684..68de75194 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.cpp +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -59,13 +59,9 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) if (it == visited.end()) { - // don't consider Boolean equality - if (cur.getKind() == kind::EQUAL && !cur[0].getType().isBoolean()) + if (cur.getNumChildren()==0) { - // For example, (= x y) ---> (and (>= x y) (<= x y)) - theory::TrustNode trn = te->ppRewriteEquality(cur); - // can make proof producing by using proof generator from trn - visited[cur] = trn.isNull() ? Node(cur) : trn.getNode(); + visited[cur] = cur; } else { @@ -95,6 +91,13 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) { ret = nm->mkNode(cur.getKind(), children); } + if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean()) + { + // For example, (= x y) ---> (and (>= x y) (<= x y)) + theory::TrustNode trn = te->ppRewriteEquality(ret); + // can make proof producing by using proof generator from trn + ret = trn.isNull() ? Node(ret) : trn.getNode(); + } visited[cur] = ret; } } while (!visit.empty()); |