From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Oct 2020 18:37:59 +0000 (-0500)
Subject: Apply alpha equivalence to annotated quantified formulas (#5324)
X-Git-Tag: cvc5-1.0.0~2665
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2c9207df7bc8ce88e84ffb51cd5eed0de37283bc;p=cvc5.git

Apply alpha equivalence to annotated quantified formulas (#5324)

Previously, alpha equivalence was not applied to quantified formulas with attributes, likely motivated by keeping alpha equivalent quantified formulas with different user patterns. It's not clear this is a good a idea. Moreover, this also implies that quantified formulas with user-provided names (which happens in e.g. Boogie benchmarks) also do not have alpha equivalence applied.

This makes it so that we apply alpha equivalence regardless of annotations.

FYI @barrettcw
---

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 4bdc6698d..20fcaad49 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -17,12 +17,12 @@
 
 #include "theory/quantifiers_engine.h"
 
-using namespace CVC4;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
 struct sortTypeOrder {
   expr::TermCanonize* d_tu;
   bool operator() (TypeNode i, TypeNode j) {
@@ -142,15 +142,23 @@ Node AlphaEquivalence::reduceQuantifier(Node q)
   Node lem;
   if (ret != q)
   {
-    // do not reduce annotated quantified formulas based on alpha equivalence
-    if (q.getNumChildren() == 2)
+    // lemma ( q <=> d_quant )
+    // Notice that we infer this equivalence regardless of whether q or ret
+    // have annotations (e.g. user patterns, names, etc.).
+    Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
+    Trace("alpha-eq") << "  " << q << std::endl;
+    Trace("alpha-eq") << "  " << ret << std::endl;
+    lem = q.eqNode(ret);
+    if (q.getNumChildren() == 3)
     {
-      // lemma ( q <=> d_quant )
-      Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
-      Trace("alpha-eq") << "  " << q << std::endl;
-      Trace("alpha-eq") << "  " << ret << std::endl;
-      lem = q.eqNode(ret);
+      Notice() << "Ignoring annotated quantified formula based on alpha "
+                  "equivalence: "
+               << q << std::endl;
     }
   }
   return lem;
 }
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4