diff options
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/fun_def_evaluator.cpp | 96 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 29 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 139 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_eval_unfold.h | 43 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_rl.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_strat.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 41 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 119 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 25 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/type_info.cpp | 16 |
13 files changed, 335 insertions, 196 deletions
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index 376d0eb47..8eb0ef686 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/fun_def_evaluator.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/rewriter.h" @@ -53,6 +54,8 @@ Node FunDefEvaluator::evaluate(Node n) const Assert(Rewriter::rewrite(n) == n); Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); + std::unordered_map<TNode, unsigned, TNodeHashFunction> funDefCount; + std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator itCount; std::unordered_map<TNode, Node, TNodeHashFunction> visited; std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; std::map<Node, FunDefInfo>::const_iterator itf; @@ -75,6 +78,13 @@ Node FunDefEvaluator::evaluate(Node n) const Trace("fd-eval-debug") << "constant " << cur << std::endl; visited[cur] = cur; } + else if (cur.getKind() == ITE) + { + Trace("fd-eval-debug") << "ITE " << cur << std::endl; + visited[cur] = Node::null(); + visit.push_back(cur); + visit.push_back(cur[0]); + } else { Trace("fd-eval-debug") << "recurse " << cur << std::endl; @@ -102,6 +112,34 @@ Node FunDefEvaluator::evaluate(Node n) const { children.push_back(cur.getOperator()); } + else if (ck == ITE) + { + // get evaluation of condition + it = visited.find(cur[0]); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + if (!it->second.isConst()) + { + Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of " + "ITE to const, FAIL\n"; + return Node::null(); + } + // pick child to evaluate depending on condition eval + unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2; + Trace("fd-eval-debug2") + << "FunDefEvaluator: result of ITE condition : " + << it->second.getConst<bool>() << "\n"; + // the result will be the result of evaluation the child + visited[cur] = cur[childIdxToEval]; + // push back self and child. The child will be evaluated first and + // result will be the result of evaluation child + visit.push_back(cur); + visit.push_back(cur[childIdxToEval]); + Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : " + << cur[childIdxToEval] << "\n"; + continue; + } + unsigned child CVC4_UNUSED = 0; for (const Node& cn : cur) { it = visited.find(cn); @@ -109,20 +147,37 @@ Node FunDefEvaluator::evaluate(Node n) const Assert(!it->second.isNull()); childChanged = childChanged || cn != it->second; children.push_back(it->second); + Trace("fd-eval-debug2") << "argument " << child++ + << " eval : " << it->second << std::endl; } if (cur.getKind() == APPLY_UF) { // need to evaluate it f = cur.getOperator(); + Trace("fd-eval-debug2") + << "FunDefEvaluator: need to eval " << f << "\n"; itf = d_funDefMap.find(f); - if (itf == d_funDefMap.end()) + itCount = funDefCount.find(f); + if (itCount == funDefCount.end()) { - Trace("fd-eval") << "FunDefEvaluator: no definition for " << f - << ", FAIL" << std::endl; + funDefCount[f] = 0; + itCount = funDefCount.find(f); + } + if (itf == d_funDefMap.end() + || itCount->second > options::sygusRecFunEvalLimit()) + { + Trace("fd-eval") + << "FunDefEvaluator: " + << (itf == d_funDefMap.end() ? "no definition for " + : "too many evals for ") + << f << ", FAIL" << std::endl; return Node::null(); } + ++funDefCount[f]; // get the function definition Node sbody = itf->second.d_body; + Trace("fd-eval-debug2") + << "FunDefEvaluator: definition: " << sbody << "\n"; const std::vector<Node>& args = itf->second.d_args; if (!args.empty()) { @@ -131,6 +186,17 @@ Node FunDefEvaluator::evaluate(Node n) const args.begin(), args.end(), children.begin(), children.end()); // rewrite it sbody = Rewriter::rewrite(sbody); + if (Trace.isOn("fd-eval-debug2")) + { + Trace("fd-eval-debug2") + << "FunDefEvaluator: evaluation with args:\n"; + for (const Node& child : children) + { + Trace("fd-eval-debug2") << "..." << child << "\n"; + } + Trace("fd-eval-debug2") + << "FunDefEvaluator: results in " << sbody << "\n"; + } } // our result is the result of the body visited[cur] = sbody; @@ -139,6 +205,8 @@ Node FunDefEvaluator::evaluate(Node n) const // evaluating the body. if (!sbody.isConst()) { + Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur + << " from body " << sbody << "\n"; visit.push_back(cur); visit.push_back(sbody); } @@ -150,25 +218,35 @@ Node FunDefEvaluator::evaluate(Node n) const ret = nm->mkNode(cur.getKind(), children); ret = Rewriter::rewrite(ret); } + Trace("fd-eval-debug2") << "built from arguments " << ret << "\n"; visited[cur] = ret; } } else if (cur != curEval && !curEval.isConst()) { Trace("fd-eval-debug") << "from body " << cur << std::endl; + Trace("fd-eval-debug") << "and eval " << curEval << std::endl; // we had to evaluate our body, which should have a definition now it = visited.find(curEval); - Assert(it != visited.end()); - // our definition is the result of the body - visited[cur] = it->second; + if (it == visited.end()) + { + Trace("fd-eval-debug2") << "eval without definition\n"; + // this is the case where curEval was not a constant but it was + // irreducible, for example (DT_SYGUS_EVAL e args) + visited[cur] = curEval; + } + else + { + Trace("fd-eval-debug2") + << "eval with definition " << it->second << "\n"; + visited[cur] = it->second; } } + } } while (!visit.empty()); + Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n"; Assert(visited.find(n) != visited.end()); Assert(!visited.find(n)->second.isNull()); - Assert(visited.find(n)->second.isConst()); - Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n] - << std::endl; return visited[n]; } diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index aa0af6f1d..c806bb1e7 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -31,12 +31,9 @@ namespace theory { namespace quantifiers { Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p) - : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false) + : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false) { - if (options::sygusEvalUnfold()) - { - d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold(); - } + d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold(); } bool Cegis::initialize(Node conj, @@ -80,7 +77,7 @@ bool Cegis::processInitialize(Node conj, for (unsigned i = 0; i < csize; i++) { Trace("cegis") << "...register enumerator " << candidates[i]; - bool do_repair_const = false; + bool useSymCons = false; if (options::sygusRepairConst()) { TypeNode ctn = candidates[i].getType(); @@ -88,15 +85,15 @@ bool Cegis::processInitialize(Node conj, SygusTypeInfo& cti = d_tds->getTypeInfo(ctn); if (cti.hasSubtermSymbolicCons()) { - do_repair_const = true; - // remember that we are doing grammar-based repair - d_using_gr_repair = true; - Trace("cegis") << " (using repair)"; + useSymCons = true; + // remember that we are using symbolic constructors + d_usingSymCons = true; + Trace("cegis") << " (using symbolic constructors)"; } } Trace("cegis") << std::endl; d_tds->registerEnumerator( - candidates[i], candidates[i], d_parent, erole, do_repair_const); + candidates[i], candidates[i], d_parent, erole, useSymCons); } return true; } @@ -135,7 +132,10 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, } NodeManager* nm = NodeManager::currentNM(); bool addedEvalLemmas = false; - if (options::sygusRefEval()) + // Refinement evaluation should not be done for grammars with symbolic + // constructors. + bool doRefEval = options::sygusRefEval() && !d_usingSymCons; + if (doRefEval) { Trace("cegqi-engine") << " *** Do refinement lemma evaluation" << (doGen ? " with conjecture-specific refinement" @@ -169,7 +169,8 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, } } // we only do evaluation unfolding for passive enumerators - if (doGen && d_eval_unfold != nullptr) + bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons; + if (doEvalUnfold) { Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl; std::vector<Node> eager_terms, eager_vals, eager_exps; @@ -239,7 +240,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, } } // if we are using grammar-based repair - if (d_using_gr_repair) + if (d_usingSymCons && options::sygusRepairConst()) { SygusRepairConst* src = d_parent->getRepairConst(); Assert(src != nullptr); diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 08cf98c99..adaecc7f6 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -204,15 +204,15 @@ class Cegis : public SygusModule */ std::unordered_set<unsigned> d_cegis_sample_refine; - //---------------------------------for sygus repair - /** are we using grammar-based repair? + //---------------------------------for symbolic constructors + /** are we using symbolic constants? * * This flag is set ot true if at least one of the enumerators allocated * by this class has been configured to allow model values with symbolic * constructors, such as the "any constant" constructor. */ - bool d_using_gr_repair; - //---------------------------------end for sygus repair + bool d_usingSymCons; + //---------------------------------end for symbolic constructors }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 472a82e29..e4c23977e 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -996,6 +996,10 @@ bool SygusEnumerator::TermEnumMasterInterp::initialize(SygusEnumerator* se, Node SygusEnumerator::TermEnumMasterInterp::getCurrent() { return *d_te; } bool SygusEnumerator::TermEnumMasterInterp::increment() { + if (d_te.isFinished()) + { + return false; + } SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn]; Node curr = getCurrent(); tc.addTerm(curr); diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 5286ab6f7..42ddbbb7d 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -14,7 +14,9 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" +#include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace std; @@ -101,6 +103,10 @@ void SygusEvalUnfold::registerModelValue(Node a, antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp); // Node antec = n.eqNode( vn ); TypeNode tn = n.getType(); + // Check if the sygus type has any symbolic constructors. This will + // impact how the unfolding is computed below. + SygusTypeInfo& sti = d_tds->getTypeInfo(tn); + bool hasSymCons = sti.hasSubtermSymbolicCons(); // n occurs as an evaluation head, thus it has sygus datatype type Assert(tn.isDatatype()); const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); @@ -148,7 +154,7 @@ void SygusEvalUnfold::registerModelValue(Node a, do_unfold = true; } } - if (do_unfold) + if (do_unfold || hasSymCons) { // note that this is replicated for different values std::map<Node, Node> vtm; @@ -158,7 +164,10 @@ void SygusEvalUnfold::registerModelValue(Node a, eval_children.end(), it->second[i].begin(), it->second[i].end()); Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); eval_children.resize(1); - res = d_tds->unfold(eval_fun, vtm, exp); + // If we explicitly asked to unfold, we use single step, otherwise + // we use multi step. + res = unfold(eval_fun, vtm, exp, true, !do_unfold); + Trace("sygus-eval-unfold") << "Unfold returns " << res << std::endl; expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); } else @@ -170,6 +179,8 @@ void SygusEvalUnfold::registerModelValue(Node a, eval_children[0] = vn; Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children); res = d_tds->evaluateWithUnfolding(eval_fun); + Trace("sygus-eval-unfold") + << "Evaluate with unfolding returns " << res << std::endl; esit.init(conj, n, res); eval_children.resize(1); eval_children[0] = n; @@ -193,6 +204,130 @@ void SygusEvalUnfold::registerModelValue(Node a, } } +Node SygusEvalUnfold::unfold(Node en, + std::map<Node, Node>& vtm, + std::vector<Node>& exp, + bool track_exp, + bool doRec) +{ + if (en.getKind() != DT_SYGUS_EVAL) + { + Assert(en.isConst()); + return en; + } + Trace("sygus-eval-unfold-debug") + << "Unfold : " << en << ", track exp is " << track_exp << ", doRec is " + << doRec << std::endl; + Node ev = en[0]; + if (track_exp) + { + std::map<Node, Node>::iterator itv = vtm.find(en[0]); + Assert(itv != vtm.end()); + if (itv != vtm.end()) + { + ev = itv->second; + } + Assert(en[0].getType() == ev.getType()); + Assert(ev.isConst()); + } + Trace("sygus-eval-unfold-debug") + << "Unfold model value is : " << ev << std::endl; + AlwaysAssert(ev.getKind() == APPLY_CONSTRUCTOR); + std::vector<Node> args; + for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++) + { + args.push_back(en[i]); + } + + TypeNode headType = en[0].getType(); + Type headTypeT = headType.toType(); + NodeManager* nm = NodeManager::currentNM(); + const Datatype& dt = headType.getDatatype(); + unsigned i = datatypes::utils::indexOf(ev.getOperator()); + if (track_exp) + { + // explanation + Node ee = + nm->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]); + if (std::find(exp.begin(), exp.end(), ee) == exp.end()) + { + exp.push_back(ee); + } + } + // if we are a symbolic constructor, unfolding returns the subterm itself + Node sop = Node::fromExpr(dt[i].getSygusOp()); + if (sop.getAttribute(SygusAnyConstAttribute())) + { + Trace("sygus-eval-unfold-debug") + << "...it is an any-constant constructor" << std::endl; + Assert(dt[i].getNumArgs() == 1); + // If the argument to evaluate is itself concrete, then we use its + // argument; otherwise we return its selector. + if (en[0].getKind() == APPLY_CONSTRUCTOR) + { + Trace("sygus-eval-unfold-debug") + << "...return (from constructor) " << en[0][0] << std::endl; + return en[0][0]; + } + else + { + Node ret = nm->mkNode( + APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, 0), en[0]); + Trace("sygus-eval-unfold-debug") + << "...return (from constructor) " << ret << std::endl; + return ret; + } + } + + Assert(!dt.isParametric()); + std::map<int, Node> pre; + for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) + { + std::vector<Node> cc; + Node s; + // get the j^th subfield of en + if (en[0].getKind() == APPLY_CONSTRUCTOR) + { + // if it is a concrete constructor application, as an optimization, + // just return the argument + s = en[0][j]; + } + else + { + s = nm->mkNode( + APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, j), en[0]); + } + cc.push_back(s); + if (track_exp) + { + // update vtm map + vtm[s] = ev[j]; + } + cc.insert(cc.end(), args.begin(), args.end()); + Node argj = nm->mkNode(DT_SYGUS_EVAL, cc); + if (doRec) + { + Trace("sygus-eval-unfold-debug") << "Recurse on " << s << std::endl; + // evaluate recursively + argj = unfold(argj, vtm, exp, track_exp, doRec); + } + pre[j] = argj; + } + Node ret = d_tds->mkGeneric(dt, i, pre); + // apply the appropriate substitution to ret + ret = datatypes::utils::applySygusArgs(dt, sop, ret, args); + // rewrite + ret = Rewriter::rewrite(ret); + return ret; +} + +Node SygusEvalUnfold::unfold(Node en) +{ + std::map<Node, Node> vtm; + std::vector<Node> exp; + return unfold(en, vtm, exp, false, false); +} + } // 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 index adc54c6a7..50b361fc4 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -83,6 +83,49 @@ class SygusEvalUnfold std::vector<Node>& exps, std::vector<Node>& terms, std::vector<Node>& vals); + /** unfold + * + * This method is called when a sygus term d (typically a variable for a SyGuS + * enumerator) has a model value specified by the map vtm. The argument en + * is an application of kind DT_SYGUS_EVAL, i.e. eval( d, c1, ..., cm ). + * Typically, d is a shared selector chain, although it may also be a + * non-constant application of a constructor. + * + * If doRec is false, this method returns the one-step unfolding of this + * evaluation function application. An example of a one step unfolding is: + * eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) ) + * + * This function does this unfolding for a (possibly symbolic) evaluation + * head, where the argument "variable to model" vtm stores the model value of + * variables from this head. This allows us to track an explanation of the + * unfolding in the vector exp when track_exp is true. + * + * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then + * this method applied to eval( d, t ) will return + * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp. + * + * If the argument doRec is true, we do a multi-step unfolding instead of + * a single-step unfolding. For example, if vtm[d] = C_+( C_x(), C_0() ), + * then this method applied to eval(d,5) will return 5+0 = 0. + * + * Furthermore, notice that any-constant constructors are *never* expanded to + * their concrete model values. This means that the multi-step unfolding when + * vtm[d] = C_+( C_x(), any_constant(n) ), then this method applied to + * eval(d,5) will return 5 + d.2.1, where the latter term is a shared selector + * chain. In other words, this unfolding elaborates the connection between + * the builtin integer field d.2.1 of d and the builtin interpretation of + * this sygus term, for the given argument. + */ + Node unfold(Node en, + std::map<Node, Node>& vtm, + std::vector<Node>& exp, + bool track_exp = true, + bool doRec = false); + /** + * Same as above, but without explanation tracking. This is used for concrete + * evaluation heads + */ + Node unfold(Node en); private: /** sygus term database associated with this utility */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 3f09a4346..5d4aaf7ae 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -105,7 +105,8 @@ Node SygusUnifRl::purifyLemma(Node n, { TNode cand = n[0]; Node tmp = n.substitute(cand, it->second); - nv = d_tds->evaluateWithUnfolding(tmp); + // should be concrete, can just use the rewriter + nv = Rewriter::rewrite(tmp); Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << tmp << " is " << nv << "\n"; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index e74068ace..07997221f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_unif_strat.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/sygus_unif.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -258,7 +259,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren); Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..." << std::endl; - eut = d_qe->getTermDatabaseSygus()->unfold(eut); + eut = d_qe->getTermDatabaseSygus()->getEvalUnfold()->unfold(eut); Trace("sygus-unif-debug2") << " ...got " << eut; Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 6e69715ef..da4275365 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -591,7 +591,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Trace("cegqi-debug") << "...squery : " << squery << std::endl; squery = Rewriter::rewrite(squery); Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl; - Assert(squery.isConst() && squery.getConst<bool>()); + Assert(options::sygusRecFun() + || (squery.isConst() && squery.getConst<bool>())); #endif return false; } @@ -711,7 +712,7 @@ void SynthConjecture::doRefine(std::vector<Node>& lems) base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end()); Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; - base_lem = Rewriter::rewrite(base_lem); + base_lem = d_tds->rewriteNode(base_lem); Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem << "..." << std::endl; d_master->registerRefinementLemma(sk_vars, base_lem, lems); diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 9f6954416..4a708e66c 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -276,28 +276,29 @@ void SynthEngine::registerQuantifier(Node q) { Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q << std::endl; - if (d_quantEngine->getOwner(q) == this) + if (d_quantEngine->getOwner(q) != this) { - Trace("cegqi") << "Register conjecture : " << q << std::endl; - if (options::sygusQePreproc()) - { - d_waiting_conj.push_back(q); - } - else - { - // assign it now - assignConjecture(q); - } + return; } - if (options::sygusRecFun()) + if (d_quantEngine->getQuantAttributes()->isFunDef(q)) { - if (d_quantEngine->getQuantAttributes()->isFunDef(q)) - { - // If it is a recursive function definition, add it to the function - // definition evaluator class. - FunDefEvaluator* fde = d_tds->getFunDefEvaluator(); - fde->assertDefinition(q); - } + Assert(options::sygusRecFun()); + // If it is a recursive function definition, add it to the function + // definition evaluator class. + Trace("cegqi") << "Registering function definition : " << q << "\n"; + FunDefEvaluator* fde = d_tds->getFunDefEvaluator(); + fde->assertDefinition(q); + return; + } + Trace("cegqi") << "Register conjecture : " << q << std::endl; + if (options::sygusQePreproc()) + { + d_waiting_conj.push_back(q); + } + else + { + // assign it now + assignConjecture(q); } } @@ -321,8 +322,6 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) bool addedLemma = false; for (const Node& lem : cclems) { - Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem - << std::endl; if (d_quantEngine->addLemma(lem)) { ++(d_statistics.d_cegqi_lemmas_ce); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 79b4c9caa..d664a462d 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -741,9 +741,9 @@ Node TermDbSygus::rewriteNode(Node n) const { return fres; } - // It may have failed, in which case there are undefined symbols in res. - // In this case, we revert to the result of rewriting in the return - // statement below. + // It may have failed, in which case there are undefined symbols in res or + // we reached the limit of evaluations. In this case, we revert to the + // result of rewriting in the return statement below. } } return res; @@ -953,107 +953,6 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) { } } -Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) { - if (en.getKind() != DT_SYGUS_EVAL) - { - Assert(en.isConst()); - return en; - } - Trace("sygus-db-debug") << "Unfold : " << en << std::endl; - Node ev = en[0]; - if (track_exp) - { - std::map<Node, Node>::iterator itv = vtm.find(en[0]); - Assert(itv != vtm.end()); - if (itv != vtm.end()) - { - ev = itv->second; - } - Assert(en[0].getType() == ev.getType()); - Assert(ev.isConst()); - } - Assert(ev.getKind() == kind::APPLY_CONSTRUCTOR); - std::vector<Node> args; - for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++) - { - args.push_back(en[i]); - } - - Type headType = en[0].getType().toType(); - NodeManager* nm = NodeManager::currentNM(); - const Datatype& dt = static_cast<DatatypeType>(headType).getDatatype(); - unsigned i = datatypes::utils::indexOf(ev.getOperator()); - if (track_exp) - { - // explanation - Node ee = nm->mkNode( - kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]); - if (std::find(exp.begin(), exp.end(), ee) == exp.end()) - { - exp.push_back(ee); - } - } - // if we are a symbolic constructor, unfolding returns the subterm itself - Node sop = Node::fromExpr(dt[i].getSygusOp()); - if (sop.getAttribute(SygusAnyConstAttribute())) - { - Trace("sygus-db-debug") << "...it is an any-constant constructor" - << std::endl; - Assert(dt[i].getNumArgs() == 1); - if (en[0].getKind() == APPLY_CONSTRUCTOR) - { - return en[0][0]; - } - else - { - return nm->mkNode( - APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]); - } - } - - Assert(!dt.isParametric()); - std::map<int, Node> pre; - for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) - { - std::vector<Node> cc; - Node s; - // get the j^th subfield of en - if (en[0].getKind() == kind::APPLY_CONSTRUCTOR) - { - // if it is a concrete constructor application, as an optimization, - // just return the argument - s = en[0][j]; - } - else - { - s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, - dt[i].getSelectorInternal(headType, j), - en[0]); - } - cc.push_back(s); - if (track_exp) - { - // update vtm map - vtm[s] = ev[j]; - } - cc.insert(cc.end(), args.begin(), args.end()); - pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc); - } - Node ret = mkGeneric(dt, i, pre); - // apply the appropriate substitution to ret - ret = datatypes::utils::applySygusArgs(dt, sop, ret, args); - // rewrite - ret = Rewriter::rewrite(ret); - return ret; -} - -Node TermDbSygus::unfold(Node en) -{ - std::map<Node, Node> vtm; - std::vector<Node> exp; - return unfold(en, vtm, exp, false); -} - Node TermDbSygus::evaluateBuiltin(TypeNode tn, Node bn, std::vector<Node>& args, @@ -1105,6 +1004,8 @@ Node TermDbSygus::evaluateWithUnfolding( Trace("dt-eval-unfold-debug") << "Optimize: evaluate constant head " << ret << std::endl; // can just do direct evaluation here + // notice we prefer this code to the rewriter since it may use + // the evaluator std::vector<Node> args; bool success = true; for (unsigned i = 1, nchild = ret.getNumChildren(); i < nchild; i++) @@ -1127,7 +1028,7 @@ Node TermDbSygus::evaluateWithUnfolding( return rete; } } - ret = unfold( ret ); + ret = d_eval_unfold->unfold(ret); } if( ret.getNumChildren()>0 ){ std::vector< Node > children; @@ -1136,7 +1037,7 @@ Node TermDbSygus::evaluateWithUnfolding( } bool childChanged = false; for( unsigned i=0; i<ret.getNumChildren(); i++ ){ - Node nc = evaluateWithUnfolding( ret[i], visited ); + Node nc = evaluateWithUnfolding(ret[i], visited); childChanged = childChanged || nc!=ret[i]; children.push_back( nc ); } @@ -1152,9 +1053,10 @@ Node TermDbSygus::evaluateWithUnfolding( } } -Node TermDbSygus::evaluateWithUnfolding( Node n ) { +Node TermDbSygus::evaluateWithUnfolding(Node n) +{ std::unordered_map<Node, Node, NodeHashFunction> visited; - return evaluateWithUnfolding( n, visited ); + return evaluateWithUnfolding(n, visited); } bool TermDbSygus::isEvaluationPoint(Node n) const @@ -1180,4 +1082,3 @@ bool TermDbSygus::isEvaluationPoint(Node n) const }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 0ec883537..76b5039f6 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -453,31 +453,6 @@ class TermDbSygus { static Node getAnchor( Node n ); static unsigned getAnchorDepth( Node n ); - public: - /** unfold - * - * This method returns the one-step unfolding of an evaluation function - * application. An example of a one step unfolding is: - * eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) ) - * - * This function does this unfolding for a (possibly symbolic) evaluation - * head, where the argument "variable to model" vtm stores the model value of - * variables from this head. This allows us to track an explanation of the - * unfolding in the vector exp when track_exp is true. - * - * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then - * this method applied to eval( d, t ) will return - * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp. - */ - Node unfold(Node en, - std::map<Node, Node>& vtm, - std::vector<Node>& exp, - bool track_exp = true); - /** - * Same as above, but without explanation tracking. This is used for concrete - * evaluation heads - */ - Node unfold(Node en); }; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 1ff0457c4..71ccd60c9 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -140,17 +140,17 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn) d_sym_cons_any_constant = i; d_has_subterm_sym_cons = true; } - // TODO (as part of #1170): we still do not properly catch type - // errors in sygus grammars for arguments of builtin operators. - // The challenge is that we easily ask for expected argument types of - // builtin operators e.g. PLUS. Hence the call to mkGeneric below - // will throw a type exception. d_ops[n] = i; d_arg_ops[i] = n; Trace("sygus-db") << std::endl; - // ensure that terms that this constructor encodes are - // of the type specified in the datatype. This will fail if - // e.g. bitvector-and is a constructor of an integer grammar. + // We must properly catch type errors in sygus grammars for arguments of + // builtin operators. The challenge is that we easily ask for expected + // argument types of builtin operators e.g. PLUS. Hence we use a call to + // mkGeneric below. This ensures that terms that this constructor encodes + // are of the type specified in the datatype. This will fail if + // e.g. bitvector-and is a constructor of an integer grammar. Our (version + // 2) SyGuS parser ensures that sygus constructors are built from well-typed + // terms, so the term created by mkGeneric will also be well-typed here. Node g = tds->mkGeneric(dt, i); TypeNode gtn = g.getType(); AlwaysAssert(gtn.isSubtypeOf(btn)) |