Minor improvement to term canonizer (#3123)

diff --git a/src/theory/quantifiers/term_canonize.cpp b/src/theory/quantifiers/term_canonize.cpp
index 9817da5a1917bc2e3aff32b097fde4389c6d8de8..2e9c1d2867a81aab7ec22070371144356d54dffe 100644 (file)
--- a/src/theory/quantifiers/term_canonize.cpp
+++ b/src/theory/quantifiers/term_canonize.cpp
@@ -122,6 +122,7 @@ struct sortTermOrder
 
 Node TermCanonize::getCanonicalTerm(TNode n,
                                     bool apply_torder,
+                                    bool doHoVar,
                                     std::map<TypeNode, unsigned>& var_count,
                                     std::map<TNode, Node>& visited)
 {
@@ -165,13 +166,16 @@ Node TermCanonize::getCanonicalTerm(TNode n,
     Trace("canon-term-debug") << "Make canonical children" << std::endl;
     for (unsigned i = 0, size = cchildren.size(); i < size; i++)
     {
-      cchildren[i] =
-          getCanonicalTerm(cchildren[i], apply_torder, var_count, visited);
+      cchildren[i] = getCanonicalTerm(
+          cchildren[i], apply_torder, doHoVar, var_count, visited);
     }
     if (n.getMetaKind() == metakind::PARAMETERIZED)
     {
       Node op = n.getOperator();
-      op = getCanonicalTerm(op, apply_torder, var_count, visited);
+      if (doHoVar)
+      {
+        op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
+      }
       Trace("canon-term-debug") << "Insert operator " << op << std::endl;
       cchildren.insert(cchildren.begin(), op);
     }
@@ -187,11 +191,11 @@ Node TermCanonize::getCanonicalTerm(TNode n,
   return n;
 }
 
-Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder)
+Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
 {
   std::map<TypeNode, unsigned> var_count;
   std::map<TNode, Node> visited;
-  return getCanonicalTerm(n, apply_torder, var_count, visited);
+  return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
 }
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/term_canonize.h b/src/theory/quantifiers/term_canonize.h
index 8f7b8722e3673facf041f46ce45b60b6ad259abe..207e6150cee4a578012e420ebb780d31b978dedc 100644 (file)
--- a/src/theory/quantifiers/term_canonize.h
+++ b/src/theory/quantifiers/term_canonize.h
@@ -55,12 +55,17 @@ class TermCanonize
    *
    * This returns a canonical (alpha-equivalent) version of n, where
    * bound variables in n may be replaced by other ones, and arguments of
-   * commutative operators of n may be sorted (if apply_torder is true).
+   * commutative operators of n may be sorted (if apply_torder is true). If
+   * doHoVar is true, we also canonicalize bound variables that occur in
+   * operators.
+   *
    * In detail, we replace bound variables in n so the the leftmost occurrence
    * of a bound variable for type T is the first canonical free variable for T,
    * the second leftmost is the second, and so on, for each type T.
    */
-  Node getCanonicalTerm(TNode n, bool apply_torder = false);
+  Node getCanonicalTerm(TNode n,
+                        bool apply_torder = false,
+                        bool doHoVar = true);
 
  private:
   /** the number of ids we have allocated for operators */
@@ -81,6 +86,7 @@ class TermCanonize
    */
   Node getCanonicalTerm(TNode n,
                         bool apply_torder,
+                        bool doHoVar,
                         std::map<TypeNode, unsigned>& var_count,
                         std::map<TNode, Node>& visited);
 };