Move some generic utilities out of quantifiers (#3139)

10 files changed, 20 insertions, 543 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index bb0cdde83..f7d433078 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -14,7 +14,6 @@
  **/
 
 #include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/term_canonize.h"
 
 using namespace CVC4;
 using namespace std;
@@ -23,7 +22,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
 struct sortTypeOrder {
-  TermCanonize* d_tu;
+  expr::TermCanonize* d_tu;
   bool operator() (TypeNode i, TypeNode j) {
     return d_tu->getIdForType( i )<d_tu->getIdForType( j );
   }
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index b5d68f233..5ef778b8d 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -20,6 +20,8 @@
 
 #include "theory/quantifiers_engine.h"
 
+#include "expr/term_canonize.h"
+
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
@@ -78,7 +80,7 @@ public:
 class AlphaEquivalenceDb
 {
  public:
-  AlphaEquivalenceDb(TermCanonize* tc) : d_tc(tc) {}
+  AlphaEquivalenceDb(expr::TermCanonize* tc) : d_tc(tc) {}
   /** adds quantified formula q to this database
    *
    * This function returns a quantified formula q' that is alpha-equivalent to
@@ -91,7 +93,7 @@ class AlphaEquivalenceDb
   /** a trie per # of variables per type */
   AlphaEquivalenceTypeNode d_ae_typ_trie;
   /** pointer to the term canonize utility */
-  TermCanonize* d_tc;
+  expr::TermCanonize* d_tc;
 };
 
 /**
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 5d1967bb4..d972f2a1c 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -15,9 +15,9 @@
 
 #include "theory/quantifiers/anti_skolem.h"
 
+#include "expr/term_canonize.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_canonize.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace std;
@@ -29,7 +29,7 @@ namespace theory {
 namespace quantifiers {
 
 struct sortTypeOrder {
-  TermCanonize* d_tu;
+  expr::TermCanonize* d_tu;
   bool operator() (TypeNode i, TypeNode j) {
     return d_tu->getIdForType( i )<d_tu->getIdForType( j );
   }
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index c07cae51d..8db0501f5 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -26,182 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
-{
-  std::vector<Node> vars;
-  std::vector<Node> subs;
-  std::map<Node, Node> smap;
-
-  std::vector<std::vector<Node> > visit;
-  std::vector<MatchTrie*> visit_trie;
-  std::vector<int> visit_var_index;
-  std::vector<bool> visit_bound_var;
-
-  visit.push_back(std::vector<Node>{n});
-  visit_trie.push_back(this);
-  visit_var_index.push_back(-1);
-  visit_bound_var.push_back(false);
-  while (!visit.empty())
-  {
-    std::vector<Node> cvisit = visit.back();
-    MatchTrie* curr = visit_trie.back();
-    if (cvisit.empty())
-    {
-      Assert(n
-             == curr->d_data.substitute(
-                    vars.begin(), vars.end(), subs.begin(), subs.end()));
-      Trace("crf-match-debug") << "notify : " << curr->d_data << std::endl;
-      if (!ntm->notify(n, curr->d_data, vars, subs))
-      {
-        return false;
-      }
-      visit.pop_back();
-      visit_trie.pop_back();
-      visit_var_index.pop_back();
-      visit_bound_var.pop_back();
-    }
-    else
-    {
-      Node cn = cvisit.back();
-      Trace("crf-match-debug") << "traverse : " << cn << " at depth "
-                               << visit.size() << std::endl;
-      unsigned index = visit.size() - 1;
-      int vindex = visit_var_index[index];
-      if (vindex == -1)
-      {
-        if (!cn.isVar())
-        {
-          Node op = cn.hasOperator() ? cn.getOperator() : cn;
-          unsigned nchild = cn.hasOperator() ? cn.getNumChildren() : 0;
-          std::map<unsigned, MatchTrie>::iterator itu =
-              curr->d_children[op].find(nchild);
-          if (itu != curr->d_children[op].end())
-          {
-            // recurse on the operator or self
-            cvisit.pop_back();
-            if (cn.hasOperator())
-            {
-              for (const Node& cnc : cn)
-              {
-                cvisit.push_back(cnc);
-              }
-            }
-            Trace("crf-match-debug") << "recurse op : " << op << std::endl;
-            visit.push_back(cvisit);
-            visit_trie.push_back(&itu->second);
-            visit_var_index.push_back(-1);
-            visit_bound_var.push_back(false);
-          }
-        }
-        visit_var_index[index]++;
-      }
-      else
-      {
-        // clean up if we previously bound a variable
-        if (visit_bound_var[index])
-        {
-          Assert(!vars.empty());
-          smap.erase(vars.back());
-          vars.pop_back();
-          subs.pop_back();
-          visit_bound_var[index] = false;
-        }
-
-        if (vindex == static_cast<int>(curr->d_vars.size()))
-        {
-          Trace("crf-match-debug")
-              << "finished checking " << curr->d_vars.size()
-              << " variables at depth " << visit.size() << std::endl;
-          // finished
-          visit.pop_back();
-          visit_trie.pop_back();
-          visit_var_index.pop_back();
-          visit_bound_var.pop_back();
-        }
-        else
-        {
-          Trace("crf-match-debug") << "check variable #" << vindex
-                                   << " at depth " << visit.size() << std::endl;
-          Assert(vindex < static_cast<int>(curr->d_vars.size()));
-          // recurse on variable?
-          Node var = curr->d_vars[vindex];
-          bool recurse = true;
-          // check if it is already bound
-          std::map<Node, Node>::iterator its = smap.find(var);
-          if (its != smap.end())
-          {
-            if (its->second != cn)
-            {
-              recurse = false;
-            }
-          }
-          else if (!var.getType().isSubtypeOf(cn.getType()))
-          {
-            recurse = false;
-          }
-          else
-          {
-            vars.push_back(var);
-            subs.push_back(cn);
-            smap[var] = cn;
-            visit_bound_var[index] = true;
-          }
-          if (recurse)
-          {
-            Trace("crf-match-debug") << "recurse var : " << var << std::endl;
-            cvisit.pop_back();
-            visit.push_back(cvisit);
-            visit_trie.push_back(&curr->d_children[var][0]);
-            visit_var_index.push_back(-1);
-            visit_bound_var.push_back(false);
-          }
-          visit_var_index[index]++;
-        }
-      }
-    }
-  }
-  return true;
-}
-
-void MatchTrie::addTerm(Node n)
-{
-  Assert(!n.isNull());
-  std::vector<Node> visit;
-  visit.push_back(n);
-  MatchTrie* curr = this;
-  while (!visit.empty())
-  {
-    Node cn = visit.back();
-    visit.pop_back();
-    if (cn.hasOperator())
-    {
-      curr = &(curr->d_children[cn.getOperator()][cn.getNumChildren()]);
-      for (const Node& cnc : cn)
-      {
-        visit.push_back(cnc);
-      }
-    }
-    else
-    {
-      if (cn.isVar()
-          && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
-                 == curr->d_vars.end())
-      {
-        curr->d_vars.push_back(cn);
-      }
-      curr = &(curr->d_children[cn][0]);
-    }
-  }
-  curr->d_data = n;
-}
-
-void MatchTrie::clear()
-{
-  d_children.clear();
-  d_vars.clear();
-  d_data = Node::null();
-}
-
 // the number of d_drewrite objects we have allocated (to avoid name conflicts)
 static unsigned drewrite_counter = 0;
 
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h
index af9ac6d87..8f5fa029f 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.h
+++ b/src/theory/quantifiers/candidate_rewrite_filter.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
 
 #include <map>
+#include "expr/match_trie.h"
 #include "theory/quantifiers/dynamic_rewrite.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/sygus_sampler.h"
@@ -28,57 +29,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/** A virtual class for notifications regarding matches. */
-class NotifyMatch
-{
- public:
-  virtual ~NotifyMatch() {}
-  /**
-   * A notification that s is equal to n * { vars -> subs }. This function
-   * should return false if we do not wish to be notified of further matches.
-   */
-  virtual bool notify(Node s,
-                      Node n,
-                      std::vector<Node>& vars,
-                      std::vector<Node>& subs) = 0;
-};
-
-/**
- * A trie (discrimination tree) storing a set of terms S, that can be used to
- * query, for a given term t, all terms s from S that are matchable with t,
- * that is s*sigma = t for some substitution sigma.
- */
-class MatchTrie
-{
- public:
-  /** Get matches
-   *
-   * This calls ntm->notify( n, s, vars, subs ) for each term s stored in this
-   * trie that is matchable with n where s = n * { vars -> subs } for some
-   * vars, subs. This function returns false if one of these calls to notify
-   * returns false.
-   */
-  bool getMatches(Node n, NotifyMatch* ntm);
-  /** Adds node n to this trie */
-  void addTerm(Node n);
-  /** Clear this trie */
-  void clear();
-
- private:
-  /**
-   * The children of this node in the trie. Terms t are indexed by a
-   * depth-first (right to left) traversal on its subterms, where the
-   * top-symbol of t is indexed by:
-   * - (operator, #children) if t has an operator, or
-   * - (t, 0) if t does not have an operator.
-   */
-  std::map<Node, std::map<unsigned, MatchTrie> > d_children;
-  /** The set of variables in the domain of d_children */
-  std::vector<Node> d_vars;
-  /** The data of this node in the trie */
-  Node d_data;
-};
-
 /** candidate rewrite filter
  *
  * This class is responsible for various filtering techniques for candidate
@@ -174,9 +124,9 @@ class CandidateRewriteFilter
    * prevents matches between terms select( x, y ) and select( z, y ) where
    * the type of x and z are different.
    */
-  std::map<TypeNode, MatchTrie> d_match_trie;
+  std::map<TypeNode, expr::MatchTrie> d_match_trie;
   /** Notify class */
-  class CandidateRewriteFilterNotifyMatch : public NotifyMatch
+  class CandidateRewriteFilterNotifyMatch : public expr::NotifyMatch
   {
     CandidateRewriteFilter& d_sse;
 
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 1d9ed1639..2dbc2627b 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -14,11 +14,11 @@
  **/
 
 #include "theory/quantifiers/conjecture_generator.h"
+#include "expr/term_canonize.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/term_canonize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/theory/quantifiers/term_canonize.cpp b/src/theory/quantifiers/term_canonize.cpp
deleted file mode 100644
index 2e9c1d286..000000000
--- a/src/theory/quantifiers/term_canonize.cpp
+++ /dev/null
@@ -1,203 +0,0 @@
-/*********************                                                        */
-/*! \file term_canonize.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of term canonize.
- **/
-
-#include "theory/quantifiers/term_canonize.h"
-
-#include "theory/quantifiers/term_util.h"
-
-using namespace CVC4::kind;
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {}
-
-int TermCanonize::getIdForOperator(Node op)
-{
-  std::map<Node, int>::iterator it = d_op_id.find(op);
-  if (it == d_op_id.end())
-  {
-    d_op_id[op] = d_op_id_count;
-    d_op_id_count++;
-    return d_op_id[op];
-  }
-  return it->second;
-}
-
-int TermCanonize::getIdForType(TypeNode t)
-{
-  std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
-  if (it == d_typ_id.end())
-  {
-    d_typ_id[t] = d_typ_id_count;
-    d_typ_id_count++;
-    return d_typ_id[t];
-  }
-  return it->second;
-}
-
-bool TermCanonize::getTermOrder(Node a, Node b)
-{
-  if (a.getKind() == BOUND_VARIABLE)
-  {
-    if (b.getKind() == BOUND_VARIABLE)
-    {
-      return a.getAttribute(InstVarNumAttribute())
-             < b.getAttribute(InstVarNumAttribute());
-    }
-    return true;
-  }
-  if (b.getKind() != BOUND_VARIABLE)
-  {
-    Node aop = a.hasOperator() ? a.getOperator() : a;
-    Node bop = b.hasOperator() ? b.getOperator() : b;
-    Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
-    Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
-    if (aop == bop)
-    {
-      if (a.getNumChildren() == b.getNumChildren())
-      {
-        for (unsigned i = 0, size = a.getNumChildren(); i < size; i++)
-        {
-          if (a[i] != b[i])
-          {
-            // first distinct child determines the ordering
-            return getTermOrder(a[i], b[i]);
-          }
-        }
-      }
-      else
-      {
-        return aop.getNumChildren() < bop.getNumChildren();
-      }
-    }
-    else
-    {
-      return getIdForOperator(aop) < getIdForOperator(bop);
-    }
-  }
-  return false;
-}
-
-Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i)
-{
-  Assert(!tn.isNull());
-  NodeManager* nm = NodeManager::currentNM();
-  while (d_cn_free_var[tn].size() <= i)
-  {
-    std::stringstream oss;
-    oss << tn;
-    std::string typ_name = oss.str();
-    while (typ_name[0] == '(')
-    {
-      typ_name.erase(typ_name.begin());
-    }
-    std::stringstream os;
-    os << typ_name[0] << i;
-    Node x = nm->mkBoundVar(os.str().c_str(), tn);
-    InstVarNumAttribute ivna;
-    x.setAttribute(ivna, d_cn_free_var[tn].size());
-    d_cn_free_var[tn].push_back(x);
-  }
-  return d_cn_free_var[tn][i];
-}
-
-struct sortTermOrder
-{
-  TermCanonize* d_tu;
-  bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
-};
-
-Node TermCanonize::getCanonicalTerm(TNode n,
-                                    bool apply_torder,
-                                    bool doHoVar,
-                                    std::map<TypeNode, unsigned>& var_count,
-                                    std::map<TNode, Node>& visited)
-{
-  std::map<TNode, Node>::iterator it = visited.find(n);
-  if (it != visited.end())
-  {
-    return it->second;
-  }
-
-  Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
-  if (n.getKind() == BOUND_VARIABLE)
-  {
-    TypeNode tn = n.getType();
-    // allocate variable
-    unsigned vn = var_count[tn];
-    var_count[tn]++;
-    Node fv = getCanonicalFreeVar(tn, vn);
-    visited[n] = fv;
-    Trace("canon-term-debug") << "...allocate variable." << std::endl;
-    return fv;
-  }
-  else if (n.getNumChildren() > 0)
-  {
-    // collect children
-    Trace("canon-term-debug") << "Collect children" << std::endl;
-    std::vector<Node> cchildren;
-    for (const Node& cn : n)
-    {
-      cchildren.push_back(cn);
-    }
-    // if applicable, first sort by term order
-    if (apply_torder && TermUtil::isComm(n.getKind()))
-    {
-      Trace("canon-term-debug")
-          << "Sort based on commutative operator " << n.getKind() << std::endl;
-      sortTermOrder sto;
-      sto.d_tu = this;
-      std::sort(cchildren.begin(), cchildren.end(), sto);
-    }
-    // now make canonical
-    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, doHoVar, var_count, visited);
-    }
-    if (n.getMetaKind() == metakind::PARAMETERIZED)
-    {
-      Node op = n.getOperator();
-      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);
-    }
-    Trace("canon-term-debug")
-        << "...constructing for " << n << "." << std::endl;
-    Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren);
-    Trace("canon-term-debug")
-        << "...constructed " << ret << " for " << n << "." << std::endl;
-    visited[n] = ret;
-    return ret;
-  }
-  Trace("canon-term-debug") << "...return 0-child term." << std::endl;
-  return n;
-}
-
-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, doHoVar, var_count, visited);
-}
-
-}  // namespace quantifiers
-}  // namespace theory
-}  // namespace CVC4
diff --git a/src/theory/quantifiers/term_canonize.h b/src/theory/quantifiers/term_canonize.h
deleted file mode 100644
index 207e6150c..000000000
--- a/src/theory/quantifiers/term_canonize.h
+++ /dev/null
@@ -1,98 +0,0 @@
-/*********************                                                        */
-/*! \file term_canonize.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utilities for constructing canonical terms.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
-
-#include <map>
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** TermCanonize
- *
- * This class contains utilities for canonizing terms with respect to
- * free variables (which are of kind BOUND_VARIABLE). For example, this
- * class infers that terms like f(BOUND_VARIABLE_1) and f(BOUND_VARIABLE_2)
- * are effectively the same term.
- */
-class TermCanonize
-{
- public:
-  TermCanonize();
-  ~TermCanonize() {}
-
-  /** Maps operators to an identifier, useful for ordering. */
-  int getIdForOperator(Node op);
-  /** Maps types to an identifier, useful for ordering. */
-  int getIdForType(TypeNode t);
-  /** get term order
-   *
-   * Returns true if a <= b in the term ordering used by this class. The
-   * term order is determined by the leftmost position in a and b whose
-   * operators o_a and o_b are distinct at that position. Then a <= b iff
-   * getIdForOperator( o_a ) <= getIdForOperator( o_b ).
-   */
-  bool getTermOrder(Node a, Node b);
-  /** get canonical free variable #i of type tn */
-  Node getCanonicalFreeVar(TypeNode tn, unsigned i);
-  /** get canonical term
-   *
-   * 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). 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,
-                        bool doHoVar = true);
-
- private:
-  /** the number of ids we have allocated for operators */
-  int d_op_id_count;
-  /** map from operators to id */
-  std::map<Node, int> d_op_id;
-  /** the number of ids we have allocated for types */
-  int d_typ_id_count;
-  /** map from type to id */
-  std::map<TypeNode, int> d_typ_id;
-  /** free variables for each type */
-  std::map<TypeNode, std::vector<Node> > d_cn_free_var;
-  /** get canonical term
-   *
-   * This is a helper function for getCanonicalTerm above. We maintain a
-   * counter of how many variables we have allocated for each type (var_count),
-   * and a cache of visited nodes (visited).
-   */
-  Node getCanonicalTerm(TNode n,
-                        bool apply_torder,
-                        bool doHoVar,
-                        std::map<TypeNode, unsigned>& var_count,
-                        std::map<TNode, Node>& visited);
-};
-
-}  // namespace quantifiers
-}  // namespace theory
-}  // namespace CVC4
-
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f86d82874..0281f50ec 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers_engine.h"
 
+#include "expr/term_canonize.h"
 #include "options/quantifiers_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_statistics_registry.h"
@@ -49,7 +50,6 @@
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_canonize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
@@ -81,7 +81,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_builder(nullptr),
       d_qepr(nullptr),
       d_term_util(new quantifiers::TermUtil(this)),
-      d_term_canon(new quantifiers::TermCanonize),
+      d_term_canon(new expr::TermCanonize),
       d_term_db(new quantifiers::TermDb(c, u, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
@@ -330,7 +330,7 @@ quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
 {
   return d_term_util.get();
 }
-quantifiers::TermCanonize* QuantifiersEngine::getTermCanonize() const
+expr::TermCanonize* QuantifiersEngine::getTermCanonize() const
 {
   return d_term_canon.get();
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 61e9053f5..da207c58a 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -36,6 +36,10 @@ namespace CVC4 {
 
 class TheoryEngine;
 
+namespace expr {
+class TermCanonize;
+}
+
 namespace theory {
 
 class QuantifiersEngine;
@@ -47,7 +51,6 @@ namespace quantifiers {
   class TermDb;
   class TermDbSygus;
   class TermUtil;
-  class TermCanonize;
   class Instantiate;
   class Skolemize;
   class TermEnumeration;
@@ -130,7 +133,7 @@ public:
   /** get term utilities */
   quantifiers::TermUtil* getTermUtil() const;
   /** get term canonizer */
-  quantifiers::TermCanonize* getTermCanonize() const;
+  expr::TermCanonize* getTermCanonize() const;
   /** get quantifiers attributes */
   quantifiers::QuantAttributes* getQuantAttributes() const;
   /** get instantiate utility */
@@ -345,7 +348,7 @@ public:
   /** term utilities */
   std::unique_ptr<quantifiers::TermUtil> d_term_util;
   /** term utilities */
-  std::unique_ptr<quantifiers::TermCanonize> d_term_canon;
+  std::unique_ptr<expr::TermCanonize> d_term_canon;
   /** term database */
   std::unique_ptr<quantifiers::TermDb> d_term_db;
   /** sygus term database */