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/smt/process_assertions.cpp | |
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/smt/process_assertions.cpp')
-rw-r--r-- | src/smt/process_assertions.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 0bbc2eeae..6d6c81e3c 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -317,10 +317,7 @@ bool ProcessAssertions::apply(Assertions& as) { d_passes["ho-elim"]->apply(&assertions); } - - // rewrite equalities based on theory-specific rewriting - d_passes["theory-rewrite-eq"]->apply(&assertions); - + // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones @@ -332,6 +329,8 @@ bool ProcessAssertions::apply(Assertions& as) // ensure rewritten d_passes["rewrite"]->apply(&assertions); + // rewrite equalities based on theory-specific rewriting + d_passes["theory-rewrite-eq"]->apply(&assertions); // apply theory preprocess, which includes ITE removal d_passes["theory-preprocess"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may |