From: Mathias Preiner Date: Sun, 11 Oct 2020 18:10:16 +0000 (-0700) Subject: SyGuS instantiation modes (#5228) X-Git-Tag: cvc5-1.0.0~2725 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d49a4413c819f6dee337ac7c53b6f6c6b510377;p=cvc5.git SyGuS instantiation modes (#5228) This PR adds three instantiation modes to the SyGuS instantiation module. --- diff --git a/src/expr/node.h b/src/expr/node.h index 7ae56d313..bb014bbaf 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1417,7 +1417,7 @@ NodeTemplate::substitute(Iterator1 nodesBegin, Assert(std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd)) << "Substitution iterator ranges must be equal size"; - Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this)); + Iterator1 j = std::find(nodesBegin, nodesEnd, TNode(*this)); if(j != nodesEnd) { Iterator2 b = replacementsBegin; std::advance(b, std::distance(nodesBegin, j)); diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 2a5faf9f7..d29052042 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -2023,3 +2023,21 @@ header = "options/quantifiers_options.h" [[option.mode.BOTH]] name = "both" help = "combines minimal and maximal ." + +[[option]] + name = "sygusInstMode" + category = "regular" + long = "sygus-inst-mode=MODE" + type = "SygusInstMode" + default = "PRIORITY_INST" + help = "select instantiation lemma mode" + help_mode = "SyGuS instantiation lemma modes." +[[option.mode.PRIORITY_INST]] + name = "priority-inst" + help = "add instantiation lemmas first, add evaluation unfolding if instantiation fails." +[[option.mode.PRIORITY_EVAL]] + name = "priority-eval" + help = "add evaluation unfolding lemma first, add instantiation lemma if unfolding lemmas already added." +[[option.mode.INTERLEAVE]] + name = "interleave" + help = "add instantiation and evaluation unfolding lemmas in the same step." diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index e2aeee1b6..119cd925c 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -182,7 +182,6 @@ void addSpecialValues( SygusInst::SygusInst(QuantifiersEngine* qe) : QuantifiersModule(qe), - d_lemma_cache(qe->getUserContext()), d_ce_lemma_added(qe->getUserContext()), d_global_terms(qe->getUserContext()), d_notified_assertions(qe->getUserContext()) @@ -245,14 +244,20 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) TermDbSygus* db = d_quantEngine->getTermDatabaseSygus(); SygusExplain syexplain(db); NodeManager* nm = NodeManager::currentNM(); + options::SygusInstMode mode = options::sygusInstMode(); for (const Node& q : d_active_quant) { - std::vector terms; - for (const Node& var : q[0]) + const std::vector& inst_constants = d_inst_constants.at(q); + const std::vector& dt_evals = d_var_eval.at(q); + Assert(inst_constants.size() == dt_evals.size()); + Assert(inst_constants.size() == q[0].getNumChildren()); + + std::vector terms, eval_unfold_lemmas; + for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i) { - Node dt_var = d_inst_constants[var]; - Node dt_eval = d_var_eval[var]; + Node dt_var = inst_constants[i]; + Node dt_eval = dt_evals[i]; Node value = model->getValue(dt_var); Node t = datatypes::utils::sygusToBuiltin(value); terms.push_back(t); @@ -270,22 +275,43 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e) exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp), dt_eval.eqNode(t)); } + eval_unfold_lemmas.push_back(lem); + } - if (d_lemma_cache.find(lem) == d_lemma_cache.end()) + if (mode == options::SygusInstMode::PRIORITY_INST) + { + if (!inst->addInstantiation(q, terms)) { - Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl; - d_quantEngine->addLemma(lem, false); - d_lemma_cache.insert(lem); + sendEvalUnfoldLemmas(eval_unfold_lemmas); } } - - if (inst->addInstantiation(q, terms)) + else if (mode == options::SygusInstMode::PRIORITY_EVAL) + { + if (!sendEvalUnfoldLemmas(eval_unfold_lemmas)) + { + inst->addInstantiation(q, terms); + } + } + else { - Trace("sygus-inst") << "Instantiate " << q << std::endl; + Assert(mode == options::SygusInstMode::INTERLEAVE); + inst->addInstantiation(q, terms); + sendEvalUnfoldLemmas(eval_unfold_lemmas); } } } +bool SygusInst::sendEvalUnfoldLemmas(const std::vector& lemmas) +{ + bool added_lemma = false; + for (const Node& lem : lemmas) + { + Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl; + added_lemma |= d_quantEngine->addLemma(lem); + } + return added_lemma; +} + bool SygusInst::checkCompleteFor(Node q) { return d_inactive_quant.find(q) != d_inactive_quant.end(); @@ -440,6 +466,10 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) { Assert(q[0].getNumChildren() == types.size()); Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end()); + Assert(d_inst_constants.find(q) == d_inst_constants.end()); + Assert(d_var_eval.find(q) == d_var_eval.end()); + + Trace("sygus-inst") << "Register CE Lemma for " << q << std::endl; /* Generate counterexample lemma for 'q'. */ NodeManager* nm = NodeManager::currentNM(); @@ -448,8 +478,8 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype * instantiation constant ic_i with type types[i] and wrap each ic_i in * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */ - std::vector vars; std::vector evals; + std::vector inst_constants; for (size_t i = 0, size = types.size(); i < size; ++i) { TypeNode tn = types[i]; @@ -459,6 +489,7 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) Node ic = nm->mkInstConstant(tn); InstConstantAttribute ica; ic.setAttribute(ica, q); + Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl; db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION); @@ -470,13 +501,13 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) } Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args); - d_inst_constants.emplace(std::make_pair(var, ic)); - d_var_eval.emplace(std::make_pair(var, eval)); - - vars.push_back(var); + inst_constants.push_back(ic); evals.push_back(eval); } + d_inst_constants.emplace(q, inst_constants); + d_var_eval.emplace(q, evals); + Node lit = getCeLiteral(q); d_quantEngine->addRequirePhase(lit, true); @@ -496,7 +527,7 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */ Node body = - q[1].substitute(vars.begin(), vars.end(), evals.begin(), evals.end()); + q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end()); Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate()); lem = Rewriter::rewrite(lem); diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index c95c6a026..0358b4984 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -99,11 +99,17 @@ class SygusInst : public QuantifiersModule * preRegisterQuantifier() call.*/ void addCeLemma(Node q); - /* Maps bound variables to corresponding instantiation constants. */ - std::unordered_map d_inst_constants; + /* Send evaluation unfolding lemmas and cache them. + * Returns true if a new lemma (not cached) was added, and false otherwise. + */ + bool sendEvalUnfoldLemmas(const std::vector& lemmas); + + /* Maps quantifiers to a vector of instantiation constants. */ + std::unordered_map, NodeHashFunction> + d_inst_constants; - /* Maps bound variables to corresponding DT_SYGUS_EVAL term. */ - std::unordered_map d_var_eval; + /* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */ + std::unordered_map, NodeHashFunction> d_var_eval; /* Maps quantified formulas to registered counterexample literals. */ std::unordered_map d_ce_lits; @@ -118,9 +124,6 @@ class SygusInst : public QuantifiersModule /* Currently inactive quantifiers. */ std::unordered_set d_inactive_quant; - /* Evaluation unfolding lemma. */ - context::CDHashSet d_lemma_cache; - /* Registered counterexample lemma cache. */ std::unordered_map d_ce_lemmas;