diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-05 20:26:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-06 01:26:33 +0000 |
| commit | d93e02dc254fea6c9d56194f21649cc18f29aafe (patch) | |
| tree | e21dd0bafa7c8f843a224e03361f2119de5d55da | |
| parent | 733ab2f6b9430b2ae5824e2614de5811a60033f3 (diff) | |
Do not use extended rewrites on recursive function definitions (#7549)
Leads to potential non-idempotent behavior in the rewriter.
The issue cannot be replicated on master, but this safe guards this case anyways.
Fixes #5278.
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2 | 7 |
4 files changed, 17 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 52e90e26e..88c6cd96f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -550,8 +550,13 @@ Node QuantifiersRewriter::computeProcessTerms2( return ret; } -Node QuantifiersRewriter::computeExtendedRewrite(Node q) +Node QuantifiersRewriter::computeExtendedRewrite(Node q, const QAttributes& qa) { + // do not apply to recursive functions + if (qa.isFunDef()) + { + return q; + } Node body = q[1]; // apply extended rewriter Node bodyr = Rewriter::callExtendedRewrite(body); @@ -1888,7 +1893,7 @@ Node QuantifiersRewriter::computeOperation(Node f, } else if (computeOption == COMPUTE_EXT_REWRITE) { - return computeExtendedRewrite(f); + return computeExtendedRewrite(f, qa); } else if (computeOption == COMPUTE_PROCESS_TERMS) { diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 6a7eb5158..8b3cbb522 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -293,9 +293,9 @@ class QuantifiersRewriter : public TheoryRewriter /** compute extended rewrite * * This returns the result of applying the extended rewriter on the body - * of quantified formula q. + * of quantified formula q with attributes qa. */ - static Node computeExtendedRewrite(Node q); + static Node computeExtendedRewrite(Node q, const QAttributes& qa); //------------------------------------- end extended rewrite /** * Return true if we should do operation computeOption on quantified formula diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f6e52eb34..b0b19315e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1966,6 +1966,7 @@ set(regress_1_tests regress1/quantifiers/issue4813-qe-quant.smt2 regress1/quantifiers/issue4849-nqe.smt2 regress1/quantifiers/issue5019-cegqi-i.smt2 + regress1/quantifiers/issue5278-ext-rewrite-rec.smt2 regress1/quantifiers/issue5279-nqe.smt2 regress1/quantifiers/issue5288-vts-real-int.smt2 regress1/quantifiers/issue5365-nqe.smt2 diff --git a/test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2 b/test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2 new file mode 100644 index 000000000..9313d9f5d --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --fmf-fun --ext-rewrite-quant -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((a 0)) (((b) (c)))) +(define-funs-rec ((d ((x a)) Bool)) ((is-b x))) +(check-sat) |