From 395aaff1ed21b37b49cba1a453a26effb2f4ca59 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Aug 2018 18:32:15 -0500 Subject: [PATCH] Split term canonize utility to own file and document (#2398) --- src/Makefile.am | 2 + src/theory/quantifiers/alpha_equivalence.cpp | 8 +- src/theory/quantifiers/anti_skolem.cpp | 6 +- .../quantifiers/conjecture_generator.cpp | 26 ++- src/theory/quantifiers/conjecture_generator.h | 3 + src/theory/quantifiers/term_canonize.cpp | 199 ++++++++++++++++++ src/theory/quantifiers/term_canonize.h | 92 ++++++++ src/theory/quantifiers/term_util.cpp | 168 +-------------- src/theory/quantifiers/term_util.h | 27 --- src/theory/quantifiers_engine.cpp | 6 + src/theory/quantifiers_engine.h | 5 + 11 files changed, 333 insertions(+), 209 deletions(-) create mode 100644 src/theory/quantifiers/term_canonize.cpp create mode 100644 src/theory/quantifiers/term_canonize.h 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 )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 )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; jmkConst(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; isecond; 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::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::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& var_count, + std::map& visited) +{ + std::map::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 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 var_count; + std::map 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 +#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 d_op_id; + /** the number of ids we have allocated for types */ + int d_typ_id_count; + /** map from type to id */ + std::map d_typ_id; + /** free variables for each type */ + std::map > 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& var_count, + std::map& 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())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; imkNode( 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& 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 d_qepr; /** term utilities */ std::unique_ptr d_term_util; + /** term utilities */ + std::unique_ptr d_term_canon; /** term database */ std::unique_ptr d_term_db; /** sygus term database */ -- 2.30.2