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 \
**/
#include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/term_canonize.h"
using namespace CVC4;
using namespace std;
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 );
}
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;
}
}
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 );
#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;
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 );
}
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(); ){
#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;
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 );
}
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 ){
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;
}
}
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);
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();
}
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));
}
}
}
};
/** 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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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));
}
}
-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 );
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;
#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"
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)),
{
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();
class TermDb;
class TermDbSygus;
class TermUtil;
+ class TermCanonize;
class Instantiate;
class Skolemize;
class TermEnumeration;
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 */
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 */
projects / cvc5.git / commitdiff