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

1 files changed, 0 insertions, 27 deletions

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;