Move some generic utilities out of quantifiers (#3139)

16 files changed, 340 insertions, 265 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 028a5ab21..68c22daef 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -591,8 +591,6 @@ libcvc4_add_sources(
   theory/quantifiers/sygus/term_database_sygus.h
   theory/quantifiers/sygus_sampler.cpp
   theory/quantifiers/sygus_sampler.h
-  theory/quantifiers/term_canonize.cpp
-  theory/quantifiers/term_canonize.h
   theory/quantifiers/term_database.cpp
   theory/quantifiers/term_database.h
   theory/quantifiers/term_enumeration.cpp
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 61ab7b3fb..300af8e8c 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -16,6 +16,8 @@ libcvc4_add_sources(
   expr_stream.h
   kind_map.h
   matcher.h
+  match_trie.cpp
+  match_trie.h
   node.cpp
   node.h
   node_algorithm.cpp
@@ -37,6 +39,8 @@ libcvc4_add_sources(
   pickler.h
   symbol_table.cpp
   symbol_table.h
+  term_canonize.cpp
+  term_canonize.h
   type.cpp
   type.h
   type_checker.h
diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp
new file mode 100644
index 000000000..363c78c9e
--- /dev/null
+++ b/src/expr/match_trie.cpp
@@ -0,0 +1,199 @@
+/*********************                                                        */
+/*! \file match_trie.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 Implements a match trie, also known as a discrimination tree.
+ **/
+
+#include "expr/match_trie.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace expr {
+
+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("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("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("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("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("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("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();
+}
+
+}  // namespace expr
+}  // namespace CVC4
diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h
new file mode 100644
index 000000000..ea8be44d9
--- /dev/null
+++ b/src/expr/match_trie.h
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file match_trie.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Andres Noetzli
+ ** 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 Implements a match trie, also known as a discrimination tree.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__MATCH_TRIE_H
+#define CVC4__EXPR__MATCH_TRIE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+/** 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;
+};
+
+}  // namespace expr
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
diff --git a/src/theory/quantifiers/term_canonize.cpp b/src/expr/term_canonize.cpp
index 2e9c1d286..d9a5f6e1a 100644
--- a/src/theory/quantifiers/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -12,15 +12,15 @@
  ** \brief Implementation of term canonize.
  **/
 
-#include "theory/quantifiers/term_canonize.h"
+#include "expr/term_canonize.h"
 
+// TODO #1216: move the code in this include
 #include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
 
 namespace CVC4 {
-namespace theory {
-namespace quantifiers {
+namespace expr {
 
 TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {}
 
@@ -54,8 +54,7 @@ bool TermCanonize::getTermOrder(Node a, Node b)
   {
     if (b.getKind() == BOUND_VARIABLE)
     {
-      return a.getAttribute(InstVarNumAttribute())
-             < b.getAttribute(InstVarNumAttribute());
+      return getIndexForFreeVariable(a) < getIndexForFreeVariable(b);
     }
     return true;
   }
@@ -107,13 +106,22 @@ Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i)
     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_fvIndex[x] = d_cn_free_var[tn].size();
     d_cn_free_var[tn].push_back(x);
   }
   return d_cn_free_var[tn][i];
 }
 
+size_t TermCanonize::getIndexForFreeVariable(Node v) const
+{
+  std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
+  if (it == d_fvIndex.end())
+  {
+    return 0;
+  }
+  return it->second;
+}
+
 struct sortTermOrder
 {
   TermCanonize* d_tu;
@@ -154,7 +162,7 @@ Node TermCanonize::getCanonicalTerm(TNode n,
       cchildren.push_back(cn);
     }
     // if applicable, first sort by term order
-    if (apply_torder && TermUtil::isComm(n.getKind()))
+    if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
     {
       Trace("canon-term-debug")
           << "Sort based on commutative operator " << n.getKind() << std::endl;
@@ -198,6 +206,5 @@ Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
   return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
 }
 
-}  // namespace quantifiers
-}  // namespace theory
+}  // namespace expr
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/term_canonize.h b/src/expr/term_canonize.h
index 207e6150c..6049cd804 100644
--- a/src/theory/quantifiers/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -14,15 +14,14 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H
+#ifndef CVC4__EXPR__TERM_CANONIZE_H
+#define CVC4__EXPR__TERM_CANONIZE_H
 
 #include <map>
 #include "expr/node.h"
 
 namespace CVC4 {
-namespace theory {
-namespace quantifiers {
+namespace expr {
 
 /** TermCanonize
  *
@@ -78,6 +77,15 @@ class TermCanonize
   std::map<TypeNode, int> d_typ_id;
   /** free variables for each type */
   std::map<TypeNode, std::vector<Node> > d_cn_free_var;
+  /**
+   * Map from each free variable above to their index in their respective vector
+   */
+  std::map<Node, size_t> d_fvIndex;
+  /**
+   * Return the range of the free variable in the above map, or 0 if it does not
+   * exist.
+   */
+  size_t getIndexForFreeVariable(Node v) const;
   /** get canonical term
    *
    * This is a helper function for getCanonicalTerm above. We maintain a
@@ -91,8 +99,7 @@ class TermCanonize
                         std::map<TNode, Node>& visited);
 };
 
-}  // namespace quantifiers
-}  // namespace theory
+}  // namespace expr
 }  // namespace CVC4
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */
+#endif /* CVC4__EXPR__TERM_CANONIZE_H */
diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h
index 07a545723..deb1accd7 100644
--- a/src/preprocessing/passes/symmetry_detect.h
+++ b/src/preprocessing/passes/symmetry_detect.h
@@ -21,7 +21,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "theory/quantifiers/term_canonize.h"
+#include "expr/term_canonize.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -242,7 +242,7 @@ class SymmetryDetect
   Node d_falseNode;
 
   /** term canonizer (for quantified formulas) */
-  theory::quantifiers::TermCanonize d_tcanon;
+  expr::TermCanonize d_tcanon;
 
   /** Cache for partitions */
   std::map<Node, Partition> d_term_partition;
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 3eb27c2f7..6d6e8fb27 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -15,6 +15,7 @@
 
 #include "preprocessing/passes/synth_rew_rules.h"
 
+#include "expr/term_canonize.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -22,7 +23,6 @@
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
-#include "theory/quantifiers/term_canonize.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
@@ -218,7 +218,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   std::vector<Node> cterms;
   // canonical terms for each type
   std::map<TypeNode, std::vector<Node> > t_cterms;
-  theory::quantifiers::TermCanonize tcanon;
+  expr::TermCanonize tcanon;
   for (unsigned i = 0, nterms = terms.size(); i < nterms; i++)
   {
     Node n = terms[i];
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_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 */