diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-05 16:45:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-05 21:45:13 +0000 |
| commit | 61aa589c4a702ee378c5b3643f4a69373da2d360 (patch) | |
| tree | 4b57160f7aee1ec2c0cb0b1109d5e469e01e86da /test | |
| parent | 7d6d265e4de057510dbb6ae049446f47b047bcb8 (diff) | |
Eliminate a level of nesting of traversals in theory preprocessing (#7345)
This simplifies the theory preprocessor so that it does not rely on the term formula removal to do a nested traversal. Instead, it only relies on its "runCurrent" method.
Notice that this PR essentially replaces TheoryPreprocessor's theoryPreprocess method with TermFormulaRemoval's runInternal method, while adding the required call to rewriteWithProof and preprocessWithProof as post-rewrites. This is far simpler than the previous method, which invoked nested traversals using TermFormulaRemoval::run.
There are two things that will be improved in follow up PRs:
The initial full rewrite step in the theory preprocessor can be merged into the main traversal of theory preprocess (I believe this is why we are slower on nec benchmark than we were previously),
We should eliminate the traversal methods from TermFormulaRemoval altogether, as they are now subsumed by the theory preprocessors main traversal. This will require refactoring how "early ITE removal" works, as this is the only user now of TermFormulaRemoval::run.
Note we should probably performance test this change.
This incidentally fixes #6973, as the previous theory preprocessing code was to blame for that issue.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f322ffafc..b6ccbcc54 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2053,7 +2053,6 @@ set(regress_1_tests regress1/quantifiers/stream-x2014-09-18-unsat.smt2 regress1/quantifiers/sygus-infer-nested.smt2 regress1/quantifiers/sygus-inst-nia-psyco-060.smt2 - regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 regress1/quantifiers/symmetric_unsat_7.smt2 regress1/quantifiers/tpp-unit-fail-qbv.smt2 regress1/quantifiers/var-eq-trigger.smt2 @@ -2824,6 +2823,8 @@ set(regression_disabled_tests # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 + # timeout after changes to theory preprocessing, note is non-linear and does not involve sygus-inst + regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 ### regress1/rels/garbage_collect.cvc.smt2 regress1/sets/setofsets-disequal.smt2 diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 index 4c6fe5c62..36162852f 100644 --- a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --strings-exp +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg (set-logic QF_SLIA) (set-info :status unsat) (declare-fun a () String) |