Split term canonize utility to own file and document (#2398)

11 files changed, 333 insertions, 209 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 8b13c9f34..883d81957 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -552,6 +552,8 @@ libcvc4_la_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/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index f9b9e909b..0f9d1acb1 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -14,7 +14,7 @@
  **/
 
 #include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/term_canonize.h"
 
 using namespace CVC4;
 using namespace std;
@@ -23,7 +23,7 @@ using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
 struct sortTypeOrder {
-  TermUtil* d_tu;
+  TermCanonize* d_tu;
   bool operator() (TypeNode i, TypeNode j) {
     return d_tu->getIdForType( i )<d_tu->getIdForType( j );
   }
@@ -100,7 +100,7 @@ Node AlphaEquivalence::reduceQuantifier( Node q ) {
   Assert( q.getKind()==FORALL );
   Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
   //construct canonical quantified formula
-  Node t = d_qe->getTermUtil()->getCanonicalTerm( q[1], true );
+  Node t = d_qe->getTermCanonize()->getCanonicalTerm(q[1], true);
   Trace("aeq") << "  canonical form: " << t << std::endl;
   //compute variable type counts
   std::map< TypeNode, int > typ_count;
@@ -113,7 +113,7 @@ Node AlphaEquivalence::reduceQuantifier( Node q ) {
     }
   }
   sortTypeOrder sto;
-  sto.d_tu = d_qe->getTermUtil();
+  sto.d_tu = d_qe->getTermCanonize();
   std::sort( typs.begin(), typs.end(), sto );
   Trace("aeq-debug") << "  ";
   Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 7fa8b2ff3..08e215d72 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -17,7 +17,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_util.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 {
-  TermUtil* d_tu;
+  TermCanonize* d_tu;
   bool operator() (TypeNode i, TypeNode j) {
     return d_tu->getIdForType( i )<d_tu->getIdForType( j );
   }
@@ -128,7 +128,7 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
             indices[d_ask_types[q][j]].push_back( j );
           }
           sortTypeOrder sto;
-          sto.d_tu = d_quantEngine->getTermUtil();
+          sto.d_tu = d_quantEngine->getTermCanonize();
           std::sort( d_ask_types[q].begin(), d_ask_types[q].end(), sto );
           //increment j on inner loop
           for( unsigned j=0; j<d_ask_types[q].size();  ){
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index a1c132fda..69f89021b 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -15,12 +15,13 @@
 
 #include "theory/quantifiers/conjecture_generator.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"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4;
@@ -92,6 +93,8 @@ ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
       d_fullEffortCount(0),
       d_hasAddedLemma(false)
 {
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
   d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
 
@@ -302,7 +305,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) {
 }
 
 Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) {
-  return d_quantEngine->getTermUtil()->getCanonicalFreeVar( tn, i );
+  return d_quantEngine->getTermCanonize()->getCanonicalFreeVar(tn, i);
 }
 
 bool ConjectureGenerator::isHandledTerm( TNode n ){
@@ -378,11 +381,14 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
         Trace("sg-proc-debug") << "...eqc : " << r << std::endl;
         eqcs.push_back( r );
         if( r.getType().isBoolean() ){
-          if( areEqual( r, getTermUtil()->d_true ) ){
-            d_ground_eqc_map[r] = getTermUtil()->d_true;
+          if (areEqual(r, d_true))
+          {
+            d_ground_eqc_map[r] = d_true;
             d_bool_eqc[0] = r;
-          }else if( areEqual( r, getTermUtil()->d_false ) ){
-            d_ground_eqc_map[r] = getTermUtil()->d_false;
+          }
+          else if (areEqual(r, d_false))
+          {
+            d_ground_eqc_map[r] = d_false;
             d_bool_eqc[1] = r;
           }
         }
@@ -447,7 +453,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
           TNode r = eqcs[i];
           //print out members
           bool firstTime = true;
-          bool isFalse = areEqual( r, getTermUtil()->d_false );
+          bool isFalse = areEqual(r, d_false);
           eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
           while( !eqc_i.isFinished() ){
             TNode n = (*eqc_i);
@@ -531,7 +537,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
               if( d_tge.isRelevantTerm( eq ) ){
                 //make it canonical
                 Trace("sg-proc-debug") << "get canonical " << eq << std::endl;
-                eq = d_quantEngine->getTermUtil()->getCanonicalTerm( eq );
+                eq = d_quantEngine->getTermCanonize()->getCanonicalTerm(eq);
               }else{
                 eq = Node::null();
               }
@@ -678,7 +684,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
                 typ_to_subs_index[it->first] = sum;
                 sum += it->second;
                 for( unsigned i=0; i<it->second; i++ ){
-                  gsubs_vars.push_back( d_quantEngine->getTermUtil()->getCanonicalFreeVar( it->first, i ) );
+                  gsubs_vars.push_back(
+                      d_quantEngine->getTermCanonize()->getCanonicalFreeVar(
+                          it->first, i));
                 }
               }
             }
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 7d4684200..450bd7991 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -287,6 +287,9 @@ private:
   };
   /** get or make eqc info */
   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
+  /** boolean terms */
+  Node d_true;
+  Node d_false;
   /** (universal) equaltity engine */
   eq::EqualityEngine d_uequalityEngine;
   /** pending adds */
diff --git a/src/theory/quantifiers/term_canonize.cpp b/src/theory/quantifiers/term_canonize.cpp
new file mode 100644
index 000000000..d257198d9
--- /dev/null
+++ b/src/theory/quantifiers/term_canonize.cpp
@@ -0,0 +1,199 @@
+/*********************                                                        */
+/*! \file term_canonize.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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,
+                                    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, var_count, visited);
+    }
+    if (n.getMetaKind() == metakind::PARAMETERIZED)
+    {
+      Node op = n.getOperator();
+      op = getCanonicalTerm(op, apply_torder, 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)
+{
+  std::map<TypeNode, unsigned> var_count;
+  std::map<TNode, Node> visited;
+  return getCanonicalTerm(n, apply_torder, 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
new file mode 100644
index 000000000..e23627271
--- /dev/null
+++ b/src/theory/quantifiers/term_canonize.h
@@ -0,0 +1,92 @@
+/*********************                                                        */
+/*! \file term_canonize.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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).
+   * 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);
+
+ 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,
+                        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/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 7d91e9812..d0e6b0247 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -36,10 +36,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermUtil::TermUtil(QuantifiersEngine * qe) :
-d_quantEngine(qe),
-d_op_id_count(0),
-d_typ_id_count(0){
+TermUtil::TermUtil(QuantifiersEngine* qe) : d_quantEngine(qe)
+{
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
@@ -342,168 +340,6 @@ void TermUtil::computeInstConstContainsForQuant(Node q,
   }
 }
 
-int TermUtil::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];
-  }else{
-    return it->second;
-  }
-}
-
-int TermUtil::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];
-  }else{
-    return it->second;
-  }
-}
-
-bool TermUtil::getTermOrder( Node a, Node b ) {
-  if( a.getKind()==BOUND_VARIABLE ){
-    if( b.getKind()==BOUND_VARIABLE ){
-      return a.getAttribute(InstVarNumAttribute())<b.getAttribute(InstVarNumAttribute());
-    }else{
-      return true;
-    }
-  }else 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; i<a.getNumChildren(); 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 TermUtil::getCanonicalFreeVar( TypeNode tn, unsigned i ) {
-  Assert( !tn.isNull() );
-  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 = NodeManager::currentNM()->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 {
-  TermUtil* d_tu;
-  //std::map< Node, std::map< Node, bool > > d_cache;
-  bool operator() (Node i, Node j) {
-    /*
-    //must consult cache since term order is partial?
-    std::map< Node, bool >::iterator it = d_cache[j].find( i );
-    if( it!=d_cache[j].end() && it->second ){
-      return false;
-    }else{
-      bool ret = d_tdb->getTermOrder( i, j );
-      d_cache[i][j] = ret;
-      return ret;
-    }
-    */
-    return d_tu->getTermOrder( i, j );
-  }
-};
-
-//this function makes a canonical representation of a term (
-//  - orders variables left to right
-//  - if apply_torder, then sort direct subterms of commutative operators
-Node TermUtil::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, std::map< TNode, Node >& visited ) {
-  Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
-  if( n.getKind()==BOUND_VARIABLE ){
-    std::map< TNode, TNode >::iterator it = subs.find( n );
-    if( it==subs.end() ){
-      TypeNode tn = n.getType();
-      //allocate variable
-      unsigned vn = var_count[tn];
-      var_count[tn]++;
-      subs[n] = getCanonicalFreeVar( tn, vn );
-      Trace("canon-term-debug") << "...allocate variable." << std::endl;
-      return subs[n];
-    }else{
-      Trace("canon-term-debug") << "...return variable in subs." << std::endl;
-      return it->second;
-    }
-  }else if( n.getNumChildren()>0 ){
-    std::map< TNode, Node >::iterator it = visited.find( n );
-    if( it!=visited.end() ){
-      return it->second;
-    }else{
-      //collect children
-      Trace("canon-term-debug") << "Collect children" << std::endl;
-      std::vector< Node > cchildren;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        cchildren.push_back( n[i] );
-      }
-      //if applicable, first sort by term order
-      if( apply_torder && 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; i<cchildren.size(); i++ ){
-        cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited );
-      }
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        Node op = n.getOperator();
-        if (options::ufHo())
-        {
-          op = getCanonicalTerm(op, var_count, subs, apply_torder, 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;
-    }
-  }else{
-    Trace("canon-term-debug") << "...return 0-child term." << std::endl;
-    return n;
-  }
-}
-
-Node TermUtil::getCanonicalTerm( TNode n, bool apply_torder ){
-  std::map< TypeNode, unsigned > var_count;
-  std::map< TNode, TNode > subs;
-  std::map< TNode, Node > visited;
-  return getCanonicalTerm( n, var_count, subs, apply_torder, visited );
-}
-
 void TermUtil::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) {
   if( inc_delta ){
     Node delta = getVtsDelta( isFree, create );
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 6a5e33f75..bc936e4a3 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -196,33 +196,6 @@ public:
                                                Node n,
                                                std::vector<Node>& vars);
 
-  // for term ordering
- private:
-  /** operator id count */
-  int d_op_id_count;
-  /** map from operators to id */
-  std::map< Node, int > d_op_id;
-  /** type id count */
-  int d_typ_id_count;
-  /** map from type to id */
-  std::map< TypeNode, int > d_typ_id;
-  //free variables
-  std::map< TypeNode, std::vector< Node > > d_cn_free_var;
-  // get canonical term, return null if it contains a term apart from handled signature
-  Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder, 
-                         std::map< TNode, Node >& visited );
-public:
-  /** get id for operator */
-  int getIdForOperator( Node op );
-  /** get id for type */
-  int getIdForType( TypeNode t );
-  /** get term order */
-  bool getTermOrder( Node a, Node b );
-  /** get canonical free variable #i of type tn */
-  Node getCanonicalFreeVar( TypeNode tn, unsigned i );
-  /** get canonical term */
-  Node getCanonicalTerm( TNode n, bool apply_torder = false );
-
 //for virtual term substitution
 private:
   Node d_vts_delta;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 510953035..038fa9e73 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -50,6 +50,7 @@
 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.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,6 +82,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_db(new quantifiers::TermDb(c, u, this)),
       d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
@@ -335,6 +337,10 @@ quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
 {
   return d_term_util.get();
 }
+quantifiers::TermCanonize* QuantifiersEngine::getTermCanonize() const
+{
+  return d_term_canon.get();
+}
 quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
 {
   return d_quant_attr.get();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index aabca1640..662803323 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -47,6 +47,7 @@ namespace quantifiers {
   class TermDb;
   class TermDbSygus;
   class TermUtil;
+  class TermCanonize;
   class Instantiate;
   class Skolemize;
   class TermEnumeration;
@@ -129,6 +130,8 @@ public:
   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
   /** get term utilities */
   quantifiers::TermUtil* getTermUtil() const;
+  /** get term canonizer */
+  quantifiers::TermCanonize* getTermCanonize() const;
   /** get quantifiers attributes */
   quantifiers::QuantAttributes* getQuantAttributes() const;
   /** get instantiate utility */
@@ -344,6 +347,8 @@ public:
   std::unique_ptr<quantifiers::QuantEPR> d_qepr;
   /** term utilities */
   std::unique_ptr<quantifiers::TermUtil> d_term_util;
+  /** term utilities */
+  std::unique_ptr<quantifiers::TermCanonize> d_term_canon;
   /** term database */
   std::unique_ptr<quantifiers::TermDb> d_term_db;
   /** sygus term database */