theory/quantifiers/sygus/sygus_pbe.h \
theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp \
theory/quantifiers/sygus/ce_guided_single_inv_sol.h \
+ theory/quantifiers/sygus/sygus_eval_unfold.cpp \
+ theory/quantifiers/sygus/sygus_eval_unfold.h \
theory/quantifiers/sygus/sygus_explain.cpp \
theory/quantifiers/sygus/sygus_explain.h \
theory/quantifiers/sygus/sygus_invariance.cpp \
namespace theory {
namespace quantifiers {
-Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) {}
+Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p)
+ : SygusModule(qe, p), d_eval_unfold(nullptr)
+{
+ if (options::sygusEvalUnfold())
+ {
+ d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
+ }
+}
bool Cegis::initialize(Node n,
const std::vector<Node>& candidates,
add the lemmas below as well, in parallel. */
}
}
- if (options::sygusEvalUnfold())
+ if (d_eval_unfold != nullptr)
{
Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl;
std::vector<Node> eager_terms, eager_vals, eager_exps;
{
Trace("cegqi-debug") << " register " << candidates[i] << " -> "
<< candidate_values[i] << std::endl;
- d_tds->registerModelValue(candidates[i],
- candidate_values[i],
- eager_terms,
- eager_vals,
- eager_exps);
+ d_eval_unfold->registerModelValue(candidates[i],
+ candidate_values[i],
+ eager_terms,
+ eager_vals,
+ eager_exps);
}
Trace("cegqi-debug") << "...produced " << eager_terms.size()
<< " evaluation unfold lemmas.\n";
std::vector<Node>& lems) override;
protected:
+ /** the evaluation unfold utility of d_tds */
+ SygusEvalUnfold* d_eval_unfold;
/** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
std::vector<Node> d_base_vars;
/**
--- /dev/null
+/********************* */
+/*! \file sygus_eval_unfold.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 sygus_eval_unfold
+ **/
+
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+SygusEvalUnfold::SygusEvalUnfold(TermDbSygus* tds) : d_tds(tds) {}
+
+void SygusEvalUnfold::registerEvalTerm(Node n)
+{
+ Assert(options::sygusEvalUnfold());
+ // is this an APPLY_UF term with head that is a sygus datatype term?
+ if (n.getKind() != APPLY_UF)
+ {
+ return;
+ }
+ TypeNode tn = n[0].getType();
+ if (!tn.isDatatype())
+ {
+ return;
+ }
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ if (!dt.isSygus())
+ {
+ return;
+ }
+ Node f = n.getOperator();
+ if (n[0].getKind() == APPLY_CONSTRUCTOR)
+ {
+ // constructors should be unfolded and reduced already
+ return;
+ }
+ if (d_eval_processed.find(n) != d_eval_processed.end())
+ {
+ return;
+ }
+ Trace("sygus-eval-unfold")
+ << "SygusEvalUnfold: register eval term : " << n << std::endl;
+ d_eval_processed.insert(n);
+ // is it the sygus evaluation function?
+ Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
+ if (n.getOperator() != eval_op)
+ {
+ return;
+ }
+ // register this evaluation term with its head
+ d_evals[n[0]].push_back(n);
+ Node var_list = Node::fromExpr(dt.getSygusVarList());
+ d_eval_args[n[0]].push_back(std::vector<Node>());
+ for (unsigned j = 1, size = n.getNumChildren(); j < size; j++)
+ {
+ d_eval_args[n[0]].back().push_back(n[j]);
+ }
+ Node a = TermDbSygus::getAnchor(n[0]);
+ d_subterms[a].insert(n[0]);
+}
+
+void SygusEvalUnfold::registerModelValue(Node a,
+ Node v,
+ std::vector<Node>& terms,
+ std::vector<Node>& vals,
+ std::vector<Node>& exps)
+{
+ std::map<Node, std::unordered_set<Node, NodeHashFunction> >::iterator its =
+ d_subterms.find(a);
+ if (its == d_subterms.end())
+ {
+ return;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ SygusExplain* sy_exp = d_tds->getExplain();
+ Trace("sygus-eval-unfold")
+ << "SygusEvalUnfold: " << a << ", has " << its->second.size()
+ << " registered subterms." << std::endl;
+ for (const Node& n : its->second)
+ {
+ Trace("sygus-eval-unfold-debug") << "...process : " << n << std::endl;
+ std::map<Node, std::vector<std::vector<Node> > >::iterator it =
+ d_eval_args.find(n);
+ if (it != d_eval_args.end() && !it->second.empty())
+ {
+ TNode at = a;
+ TNode vt = v;
+ Node vn = n.substitute(at, vt);
+ vn = Rewriter::rewrite(vn);
+ unsigned start = d_node_mv_args_proc[n][vn];
+ // get explanation in terms of testers
+ std::vector<Node> antec_exp;
+ sy_exp->getExplanationForEquality(n, vn, antec_exp);
+ Node antec =
+ antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
+ // Node antec = n.eqNode( vn );
+ TypeNode tn = n.getType();
+ Assert(tn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ Trace("sygus-eval-unfold")
+ << "SygusEvalUnfold: Register model value : " << vn << " for " << n
+ << std::endl;
+ unsigned curr_size = it->second.size();
+ Trace("sygus-eval-unfold")
+ << "...it has " << curr_size << " evaluations, already processed "
+ << start << "." << std::endl;
+ Node bTerm = d_tds->sygusToBuiltin(vn, tn);
+ Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl;
+ std::vector<Node> vars;
+ Node var_list = Node::fromExpr(dt.getSygusVarList());
+ for (const Node& v : var_list)
+ {
+ vars.push_back(v);
+ }
+ // evaluation children
+ std::vector<Node> eval_children;
+ eval_children.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
+ eval_children.push_back(n);
+ // for each evaluation
+ for (unsigned i = start; i < curr_size; i++)
+ {
+ Node res;
+ Node expn;
+ // should we unfold?
+ bool do_unfold = false;
+ if (options::sygusEvalUnfoldBool())
+ {
+ if (bTerm.getKind() == ITE || bTerm.getType().isBoolean())
+ {
+ do_unfold = true;
+ }
+ }
+ if (do_unfold)
+ {
+ // TODO (#1949) : this is replicated for different values, possibly
+ // do better caching
+ std::map<Node, Node> vtm;
+ std::vector<Node> exp;
+ vtm[n] = vn;
+ eval_children.insert(
+ eval_children.end(), it->second[i].begin(), it->second[i].end());
+ Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
+ eval_children.resize(2);
+ res = d_tds->unfold(eval_fun, vtm, exp);
+ expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
+ }
+ else
+ {
+ EvalSygusInvarianceTest esit;
+ eval_children.insert(
+ eval_children.end(), it->second[i].begin(), it->second[i].end());
+ Node conj = nm->mkNode(APPLY_UF, eval_children);
+ eval_children[1] = vn;
+ Node eval_fun = nm->mkNode(APPLY_UF, eval_children);
+ res = d_tds->evaluateWithUnfolding(eval_fun);
+ esit.init(conj, n, res);
+ eval_children.resize(2);
+ eval_children[1] = n;
+
+ // evaluate with minimal explanation
+ std::vector<Node> mexp;
+ sy_exp->getExplanationFor(n, vn, mexp, esit);
+ Assert(!mexp.empty());
+ expn = mexp.size() == 1 ? mexp[0] : nm->mkNode(AND, mexp);
+ }
+ Assert(!res.isNull());
+ terms.push_back(d_evals[n][i]);
+ vals.push_back(res);
+ exps.push_back(expn);
+ Trace("sygus-eval-unfold")
+ << "Conclude : " << d_evals[n][i] << " == " << res << std::endl;
+ Trace("sygus-eval-unfold") << " from " << expn << std::endl;
+ }
+ d_node_mv_args_proc[n][vn] = curr_size;
+ }
+ }
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file sygus_eval_unfold.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 sygus_eval_unfold
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/sygus_invariance.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class TermDbSygus;
+
+/** SygusEvalUnfold
+ *
+ * This class implements techniques for eagerly unfolding sygus evaluation
+ * functions. For example, given sygus datatype type corresponding to grammar:
+ * A -> 0 | 1 | A+A
+ * whose evaluation function is eval, this class adds lemmas that "eagerly
+ * unfold" applications of eval based on the model values of evaluation heads
+ * in refinement lemmas.
+ */
+class SygusEvalUnfold
+{
+ public:
+ SygusEvalUnfold(TermDbSygus* tds);
+ ~SygusEvalUnfold() {}
+ /** register evaluation term
+ *
+ * This is called by TermDatabase, during standard effort calls when a term
+ * n is registered as an equivalence class in the master equality engine.
+ * If this term is of the form:
+ * eval( a, t1, ..., tn )
+ * where a is a symbolic term of sygus datatype type (not a application of a
+ * constructor), then we remember that n is an evaluation function application
+ * for evaluation head a.
+ */
+ void registerEvalTerm(Node n);
+ /** register model value
+ *
+ * This notifies this class that the model value M(a) of an anchor term a is
+ * currently v. Assume in the following that the top symbol of v is some sygus
+ * datatype constructor C_op.
+ *
+ * If we have registered terms eval( a, T1 ), ..., eval( a, Tm ), then we
+ * ensure that for each i=1,...,m, a lemma of one of the two forms is
+ * generated:
+ * [A] a=v => eval( a, Ti ) = [[unfold( eval( v, Ti ) )]]
+ * [B] is-C_op(v) => eval(a, Ti ) = op(eval( a.1, Ti ), ..., eval( a.k, Ti )),
+ * where this corresponds to a "one step folding" of the sygus evaluation
+ * function, i.e. op is a builtin operator encoded by constructor C_op.
+ *
+ * We decide which kind of lemma to send ([A] or [B]) based on the symbol
+ * C_op. If op is an ITE, or if C_op is a Boolean operator, then we add [B].
+ * Otherwise, we add [A]. The intuition of why [B] is better than [A] for the
+ * former is that evaluation unfolding can lead to useful conflict analysis.
+ *
+ * For each lemma C => eval( a, T ) = T' we infer is necessary, we add C to
+ * exps, eval( a, T ) to terms, and T' to vals. The caller should send the
+ * corresponding lemma on the output channel.
+ *
+ * We do the above scheme *for each* selector chain (see d_subterms below)
+ * applied to a.
+ */
+ void registerModelValue(Node a,
+ Node v,
+ std::vector<Node>& exps,
+ std::vector<Node>& terms,
+ std::vector<Node>& vals);
+
+ private:
+ /** sygus term database associated with this utility */
+ TermDbSygus* d_tds;
+ /** the set of evaluation terms we have already processed */
+ std::unordered_set<Node, NodeHashFunction> d_eval_processed;
+ /** map from evaluation heads to evaluation function applications */
+ std::map<Node, std::vector<Node> > d_evals;
+ /**
+ * Map from evaluation function applications to their arguments (minus the
+ * evaluation head). For example, eval(x,0,1) is mapped to { 0, 1 }.
+ */
+ std::map<Node, std::vector<std::vector<Node> > > d_eval_args;
+ /**
+ * For each (a,M(a)) pair, the number of terms in d_evals that we have added
+ * lemmas for
+ */
+ std::map<Node, std::map<Node, unsigned> > d_node_mv_args_proc;
+ /** subterms map
+ *
+ * This maps anchor terms to the set of shared selector chains with
+ * them as an anchor, for example x may map to { x, x.1, x.2, x.1.1 }.
+ */
+ std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_subterms;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
: d_quantEngine(qe),
d_syexp(new SygusExplain(this)),
- d_ext_rw(new ExtendedRewriter(true))
+ d_ext_rw(new ExtendedRewriter(true)),
+ d_eval_unfold(new SygusEvalUnfold(this))
{
d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
}
}
-
-void TermDbSygus::registerEvalTerm( Node n ) {
- if (options::sygusEvalUnfold())
- {
- if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
- TypeNode tn = n[0].getType();
- if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- if( dt.isSygus() ){
- Node f = n.getOperator();
- if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
- if (d_eval_processed.find(n) == d_eval_processed.end())
- {
- Trace("sygus-eager")
- << "TermDbSygus::eager: Register eval term : " << n
- << std::endl;
- d_eval_processed.insert(n);
- d_evals[n[0]].push_back(n);
- TypeNode tn = n[0].getType();
- Assert(tn.isDatatype());
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Node var_list = Node::fromExpr(dt.getSygusVarList());
- Assert(dt.isSygus());
- d_eval_args[n[0]].push_back(std::vector<Node>());
- bool isConst = true;
- for (unsigned j = 1; j < n.getNumChildren(); j++)
- {
- d_eval_args[n[0]].back().push_back(n[j]);
- if (!n[j].isConst())
- {
- isConst = false;
- }
- }
- d_eval_args_const[n[0]].push_back(isConst);
- Node a = getAnchor(n[0]);
- d_subterms[a][n[0]] = true;
- }
- }
- }
- }
- }
- }
-}
-
-void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& terms, std::vector< Node >& vals, std::vector< Node >& exps ) {
- std::map< Node, std::map< Node, bool > >::iterator its = d_subterms.find( a );
- if( its!=d_subterms.end() ){
- Trace("sygus-eager") << "registerModelValue : " << a << ", has " << its->second.size() << " registered subterms." << std::endl;
- for( std::map< Node, bool >::iterator itss = its->second.begin(); itss != its->second.end(); ++itss ){
- Node n = itss->first;
- Trace("sygus-eager-debug") << "...process : " << n << std::endl;
- std::map< Node, std::vector< std::vector< Node > > >::iterator it = d_eval_args.find( n );
- if( it!=d_eval_args.end() && !it->second.empty() ){
- TNode at = a;
- TNode vt = v;
- Node vn = n.substitute( at, vt );
- vn = Rewriter::rewrite( vn );
- unsigned start = d_node_mv_args_proc[n][vn];
- // get explanation in terms of testers
- std::vector< Node > antec_exp;
- d_syexp->getExplanationForEquality(n, vn, antec_exp);
- Node antec = antec_exp.size()==1 ? antec_exp[0] : NodeManager::currentNM()->mkNode( kind::AND, antec_exp );
- //Node antec = n.eqNode( vn );
- TypeNode tn = n.getType();
- Assert( tn.isDatatype() );
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Assert( dt.isSygus() );
- Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
- Trace("sygus-eager") << "...it has " << it->second.size() << " evaluations, already processed " << start << "." << std::endl;
- Node bTerm = sygusToBuiltin( vn, tn );
- Trace("sygus-eager") << "Built-in term : " << bTerm << std::endl;
- std::vector< Node > vars;
- Node var_list = Node::fromExpr( dt.getSygusVarList() );
- for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
- vars.push_back( var_list[j] );
- }
- //evaluation children
- std::vector< Node > eval_children;
- eval_children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
- eval_children.push_back( n );
- //for each evaluation
- for( unsigned i=start; i<it->second.size(); i++ ){
- Node res;
- Node expn;
- // unfold?
- bool do_unfold = false;
- if (options::sygusEvalUnfoldBool())
- {
- if( bTerm.getKind()==ITE || bTerm.getType().isBoolean() ){
- do_unfold = true;
- }
- }
- if( do_unfold ){
- // TODO : this is replicated for different values, possibly do better caching
- std::map< Node, Node > vtm;
- std::vector< Node > exp;
- vtm[n] = vn;
- eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end() );
- Node eval_fun = NodeManager::currentNM()->mkNode( kind::APPLY_UF, eval_children );
- eval_children.resize( 2 );
- res = unfold( eval_fun, vtm, exp );
- expn = exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp );
- }else{
-
- EvalSygusInvarianceTest esit;
- eval_children.insert( eval_children.end(), it->second[i].begin(), it->second[i].end() );
- Node conj =
- NodeManager::currentNM()->mkNode(kind::APPLY_UF, eval_children);
- eval_children[1] = vn;
- Node eval_fun = NodeManager::currentNM()->mkNode( kind::APPLY_UF, eval_children );
- res = evaluateWithUnfolding(eval_fun);
- esit.init(conj, n, res);
- eval_children.resize( 2 );
- eval_children[1] = n;
-
- //evaluate with minimal explanation
- std::vector< Node > mexp;
- d_syexp->getExplanationFor(n, vn, mexp, esit);
- Assert( !mexp.empty() );
- expn = mexp.size()==1 ? mexp[0] : NodeManager::currentNM()->mkNode( kind::AND, mexp );
-
- //if all constant, we can use evaluation to minimize the explanation
- //Assert( i<d_eval_args_const[n].size() );
- //if( d_eval_args_const[n][i] ){
- /*
- std::map< Node, Node > vtm;
- std::map< Node, Node > visited;
- std::map< Node, std::vector< Node > > exp;
- vtm[n] = vn;
- res = crefEvaluate( eval_fun, vtm, visited, exp );
- Assert( !exp[eval_fun].empty() );
- expn = exp[eval_fun].size()==1 ? exp[eval_fun][0] : NodeManager::currentNM()->mkNode( kind::AND, exp[eval_fun] );
- */
- /*
- //otherwise, just do a substitution
- }else{
- Assert( vars.size()==it->second[i].size() );
- res = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() );
- res = Rewriter::rewrite( res );
- expn = antec;
- }
- */
- }
- Assert( !res.isNull() );
- terms.push_back( d_evals[n][i] );
- vals.push_back( res );
- exps.push_back( expn );
- Trace("sygus-eager") << "Conclude : " << d_evals[n][i] << " == " << res << ", cref eval = " << d_eval_args_const[n][i] << std::endl;
- Trace("sygus-eager") << " from " << expn << std::endl;
- }
- d_node_mv_args_proc[n][vn] = it->second.size();
- }
- }
- }
-}
-
Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
if( en.getKind()==kind::APPLY_UF ){
Trace("sygus-db-debug") << "Unfold : " << en << std::endl;
#include <unordered_set>
#include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
#include "theory/quantifiers/sygus/sygus_explain.h"
#include "theory/quantifiers/term_database.h"
SygusExplain* getExplain() { return d_syexp.get(); }
/** get the extended rewrite utility */
ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
+ /** evaluation unfolding utility */
+ SygusEvalUnfold* getEvalUnfold() { return d_eval_unfold.get(); }
//------------------------------end utilities
//------------------------------enumerators
//------------------------------utilities
/** sygus explanation */
std::unique_ptr<SygusExplain> d_syexp;
- /** sygus explanation */
+ /** extended rewriter */
std::unique_ptr<ExtendedRewriter> d_ext_rw;
+ /** evaluation function unfolding utility */
+ std::unique_ptr<SygusEvalUnfold> d_eval_unfold;
//------------------------------end utilities
//------------------------------enumerators
bool considerConst( TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg );
bool considerConst( const Datatype& pdt, TypeNode tnp, Node c, Kind pk, int arg );
int solveForArgument( TypeNode tnp, unsigned cindex, unsigned arg );
-
-//for eager instantiation
- // TODO (as part of #1235) move some of these functions to sygus_explain.h
- private:
- /** the set of evaluation terms we have already processed */
- std::unordered_set<Node, NodeHashFunction> d_eval_processed;
- std::map< Node, std::map< Node, bool > > d_subterms;
- std::map< Node, std::vector< Node > > d_evals;
- std::map< Node, std::vector< std::vector< Node > > > d_eval_args;
- std::map< Node, std::vector< bool > > d_eval_args_const;
- std::map< Node, std::map< Node, unsigned > > d_node_mv_args_proc;
-
public:
- void registerEvalTerm( Node n );
- void registerModelValue( Node n, Node v, std::vector< Node >& exps, std::vector< Node >& terms, std::vector< Node >& vals );
Node unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp = true );
Node unfold( Node en ){
std::map< Node, Node > vtm;
#include "theory/arrays/theory_arrays.h"
#include "theory/datatypes/theory_datatypes.h"
#include "theory/quantifiers/alpha_equivalence.h"
-#include "theory/quantifiers/fmf/ambqi_builder.h"
#include "theory/quantifiers/anti_skolem.h"
-#include "theory/quantifiers/fmf/bounded_integers.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
#include "theory/quantifiers/cegqi/ceg_t_instantiator.h"
+#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
#include "theory/quantifiers/conjecture_generator.h"
+#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/equality_infer.h"
#include "theory/quantifiers/equality_query.h"
#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/fmf/ambqi_builder.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
#include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/inst_propagator.h"
-#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h"
-#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
#include "theory/quantifiers/inst_strategy_enumerative.h"
#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/ematching/instantiation_engine.h"
#include "theory/quantifiers/local_theory_ext.h"
-#include "theory/quantifiers/fmf/model_engine.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/quant_epr.h"
#include "theory/quantifiers/quant_relevance.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/term_database.h"
+#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_database.h"
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
#include "theory/sep/theory_sep.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
{
if (d_sygus_tdb)
{
- d_sygus_tdb->registerEvalTerm(n);
+ d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
}
// added contains also the Node that just have been asserted in this
projects / cvc5.git / commitdiff