From caf65a13994dc1d39cc31a8cea76c6a7fddb338c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 May 2018 14:09:12 -0500 Subject: [PATCH] Refactor sygus eval unfold (#1946) --- src/Makefile.am | 2 + src/theory/quantifiers/sygus/cegis.cpp | 21 +- src/theory/quantifiers/sygus/cegis.h | 2 + .../quantifiers/sygus/sygus_eval_unfold.cpp | 199 ++++++++++++++++++ .../quantifiers/sygus/sygus_eval_unfold.h | 116 ++++++++++ .../quantifiers/sygus/term_database_sygus.cpp | 159 +------------- .../quantifiers/sygus/term_database_sygus.h | 21 +- src/theory/quantifiers_engine.cpp | 21 +- 8 files changed, 352 insertions(+), 189 deletions(-) create mode 100644 src/theory/quantifiers/sygus/sygus_eval_unfold.cpp create mode 100644 src/theory/quantifiers/sygus/sygus_eval_unfold.h diff --git a/src/Makefile.am b/src/Makefile.am index 569bc3c48..aa4487c42 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -481,6 +481,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index ec17294f9..fc41c7561 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -28,7 +28,14 @@ namespace CVC4 { 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& candidates, @@ -100,7 +107,7 @@ bool Cegis::addEvalLemmas(const std::vector& 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 eager_terms, eager_vals, eager_exps; @@ -108,11 +115,11 @@ bool Cegis::addEvalLemmas(const std::vector& candidates, { 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"; diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index e5ee6bc56..70f3ce8b6 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -65,6 +65,8 @@ class Cegis : public SygusModule std::vector& 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 d_base_vars; /** diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp new file mode 100644 index 000000000..09df1eeab --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -0,0 +1,199 @@ +/********************* */ +/*! \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(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()); + 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& terms, + std::vector& vals, + std::vector& exps) +{ + std::map >::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 > >::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 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(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 vars; + Node var_list = Node::fromExpr(dt.getSygusVarList()); + for (const Node& v : var_list) + { + vars.push_back(v); + } + // evaluation children + std::vector 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 vtm; + std::vector 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 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 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h new file mode 100644 index 000000000..94f37c845 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \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 +#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& exps, + std::vector& terms, + std::vector& vals); + + private: + /** sygus term database associated with this utility */ + TermDbSygus* d_tds; + /** the set of evaluation terms we have already processed */ + std::unordered_set d_eval_processed; + /** map from evaluation heads to evaluation function applications */ + std::map > 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 > > d_eval_args; + /** + * For each (a,M(a)) pair, the number of terms in d_evals that we have added + * lemmas for + */ + std::map > 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 > d_subterms; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 5efa1198b..37a8ae382 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -34,7 +34,8 @@ namespace quantifiers { 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 ); @@ -1287,162 +1288,6 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { } } - -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()); - 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 eval_children; - eval_children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) ); - eval_children.push_back( n ); - //for each evaluation - for( unsigned i=start; isecond.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 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; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index d53e436e0..9f370cd15 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -20,6 +20,7 @@ #include #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" @@ -52,6 +53,8 @@ class TermDbSygus { 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 @@ -210,8 +213,10 @@ class TermDbSygus { //------------------------------utilities /** sygus explanation */ std::unique_ptr d_syexp; - /** sygus explanation */ + /** extended rewriter */ std::unique_ptr d_ext_rw; + /** evaluation function unfolding utility */ + std::unique_ptr d_eval_unfold; //------------------------------end utilities //------------------------------enumerators @@ -344,21 +349,7 @@ public: // for symmetry breaking 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 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; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index b5f179822..3746c2e1c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -20,24 +20,24 @@ #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" @@ -47,11 +47,12 @@ #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" @@ -847,7 +848,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within { 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 -- 2.30.2