From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 6 Nov 2021 01:26:33 +0000 (-0500)
Subject: Do not use extended rewrites on recursive function definitions (#7549)
X-Git-Tag: cvc5-1.0.0~870
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d93e02dc254fea6c9d56194f21649cc18f29aafe;p=cvc5.git

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.
---

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)