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

1 files changed, 4 insertions, 4 deletions

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 );