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 4bdc6698dfddb7a08a7ce3a5ea5095e9107e3db0..20fcaad490a7baa226bfa3f5b7889d53cef0d5bc 100644 (file)
--- 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