diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-30 16:02:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-30 16:02:38 -0600 |
| commit | 8c4788b6356b46df5cede71bcf02c86f0aebe86c (patch) | |
| tree | 5b571eef2f7f776d8274fb7386147d0b0fcb560b | |
| parent | 6112e47d0d93b675fe220438c3828b5b6025dde6 (diff) | |
Make eq chain an aggressive rewrite in extended rewriter (#3679)
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 7 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3656.smt2 | 8 |
3 files changed, 16 insertions, 0 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 0fbd971fd..05e789ce2 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -1137,6 +1137,13 @@ Node ExtendedRewriter::extendedRewriteEqChain( { Assert(ret.getKind() == eqk); + // this rewrite is aggressive; it in fact has the precondition that other + // aggressive rewrites (including BCP) have been applied. + if (!d_aggr) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); TypeNode tn = ret[0].getType(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 799219eec..179c5fe4c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1284,6 +1284,7 @@ set(regress_1_tests regress1/nl/exp_monotone.smt2 regress1/nl/factor_agg_s.smt2 regress1/nl/issue3441.smt2 + regress1/nl/issue3656.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 regress1/nl/metitarski_3_4_2e.smt2 diff --git a/test/regress/regress1/nl/issue3656.smt2 b/test/regress/regress1/nl/issue3656.smt2 new file mode 100644 index 000000000..6de6e26b9 --- /dev/null +++ b/test/regress/regress1/nl/issue3656.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --ext-rew-prep +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun b () Real) +(declare-fun c () Real) +(assert (distinct (and (>= c (* c c c c)) (< c (* c c c c))) (= (* b c) 0.0))) +(check-sat) |