diff options
Diffstat (limited to 'src/theory/quantifiers/term_util.h')
-rw-r--r-- | src/theory/quantifiers/term_util.h | 27 |
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; |