diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 71 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 57 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_module.h | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.cpp | 44 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_pbe.h | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_unif_io.cpp | 25 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 80 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 18 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 225 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 79 |
12 files changed, 523 insertions, 104 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index fbe0da7a8..db9af10b4 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/sygus/cegis.h" +#include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -100,15 +101,47 @@ void Cegis::getTermList(const std::vector<Node>& candidates, bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values) { + // First, decide if this call will apply "conjecture-specific refinement". + // In other words, in some settings, the following method will identify and + // block a class of solutions {candidates -> S} that generalizes the current + // one (given by {candidates -> candidate_values}), such that for each + // candidate_values' in S, we have that {candidates -> candidate_values'} is + // also not a solution for the given conjecture. We may not + // apply this form of refinement if any (relevant) enumerator in candidates is + // "actively generated" (see TermDbSygs::isPassiveEnumerator), since its + // model values are themselves interpreted as classes of solutions. + bool doGen = true; + for (const Node& v : candidates) + { + // if it is relevant to refinement + if (d_refinement_lemma_vars.find(v) != d_refinement_lemma_vars.end()) + { + if (!d_tds->isPassiveEnumerator(v)) + { + doGen = false; + break; + } + } + } NodeManager* nm = NodeManager::currentNM(); bool addedEvalLemmas = false; if (options::sygusRefEval()) { - Trace("cegqi-engine") << " *** Do refinement lemma evaluation..." - << std::endl; + Trace("cegqi-engine") << " *** Do refinement lemma evaluation" + << (doGen ? " with conjecture-specific refinement" + : "") + << "..." << std::endl; // see if any refinement lemma is refuted by evaluation std::vector<Node> cre_lems; - getRefinementEvalLemmas(candidates, candidate_values, cre_lems); + bool ret = + getRefinementEvalLemmas(candidates, candidate_values, cre_lems, doGen); + if (ret && !doGen) + { + Trace("cegqi-engine") << "...(actively enumerated) candidate failed " + "refinement lemma evaluation." + << std::endl; + return true; + } if (!cre_lems.empty()) { for (const Node& lem : cre_lems) @@ -124,7 +157,8 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, add the lemmas below as well, in parallel. */ } } - if (d_eval_unfold != nullptr) + // we only do evaluation unfolding for passive enumerators + if (doGen && d_eval_unfold != nullptr) { Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl; std::vector<Node> eager_terms, eager_vals, eager_exps; @@ -281,6 +315,8 @@ void Cegis::addRefinementLemma(Node lem) } // rewrite with extended rewriter slem = d_tds->getExtRewriter()->extendedRewrite(slem); + // collect all variables in slem + expr::getSymbols(slem, d_refinement_lemma_vars); std::vector<Node> waiting; waiting.push_back(lem); unsigned wcounter = 0; @@ -408,10 +444,10 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars, } bool Cegis::usingRepairConst() { return true; } - -void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, +bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, const std::vector<Node>& ms, - std::vector<Node>& lems) + std::vector<Node>& lems, + bool doGen) { Trace("sygus-cref-eval") << "Cref eval : conjecture has " << d_refinement_lemma_unit.size() << " unit and " @@ -424,6 +460,7 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Node nfalse = nm->mkConst(false); Node neg_guard = d_parent->getGuard().negate(); + bool ret = false; for (unsigned r = 0; r < 2; r++) { std::unordered_set<Node, NodeHashFunction>& rlemmas = @@ -447,6 +484,12 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst<bool>()) { + if (!doGen) + { + // we are not generating the lemmas, instead just return + return true; + } + ret = true; std::vector<Node> msu; std::vector<Node> mexp; msu.insert(msu.end(), ms.begin(), ms.end()); @@ -480,13 +523,12 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, { cre_lem = neg_guard; } - } - if (!cre_lem.isNull() - && std::find(lems.begin(), lems.end(), cre_lem) == lems.end()) - { - Trace("sygus-cref-eval") - << "...produced lemma : " << cre_lem << std::endl; - lems.push_back(cre_lem); + if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end()) + { + Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem + << std::endl; + lems.push_back(cre_lem); + } } } if (!lems.empty()) @@ -494,6 +536,7 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, break; } } + return ret; } bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index c7392b378..7387bd468 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -104,6 +104,8 @@ class Cegis : public SygusModule /** substitution entailed by d_refinement_lemma_unit */ std::vector<Node> d_rl_eval_hds; std::vector<Node> d_rl_vals; + /** all variables appearing in refinement lemmas */ + std::unordered_set<Node, NodeHashFunction> d_refinement_lemma_vars; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); /** add refinement lemma conjunct @@ -150,10 +152,14 @@ class Cegis : public SygusModule * Given a candidate solution ms for candidates vs, this function adds lemmas * to lems based on evaluating the conjecture, instantiated for ms, on lemmas * for previous refinements (d_refinement_lemmas). + * + * Returns true if any such lemma exists. If doGen is false, then the + * lemmas are not generated or added to lems. */ - void getRefinementEvalLemmas(const std::vector<Node>& vs, + bool getRefinementEvalLemmas(const std::vector<Node>& vs, const std::vector<Node>& ms, - std::vector<Node>& lems); + std::vector<Node>& lems, + bool doGen); /** sampler object for the option cegisSample() * * This samples points of the type of the inner variables of the synthesis diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 456f44019..56edc55c6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -86,6 +86,7 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, // Non-unif candidate are themselves the enumerators enums.insert( enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end()); + Valuation& valuation = d_qe->getValuation(); for (const Node& c : d_unif_candidates) { // Collect heads of candidates @@ -95,6 +96,31 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, << "......cand " << c << " with enum hd " << hd << "\n"; enums.push_back(hd); } + // get unification enumerators + for (const Node& e : d_cand_to_strat_pt[c]) + { + for (unsigned index = 0; index < 2; index++) + { + std::vector<Node> uenums; + // get the current unification enumerators + d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index); + if (index == 1 && options::sygusUnifCondIndependent()) + { + Assert(uenums.size() == 1); + Node eu = uenums[0]; + Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); + // If active guard for this enumerator is not true, there are no more + // values for it, and hence we ignore it + Node gstatus = valuation.getSatValue(g); + if (gstatus.isNull() || !gstatus.getConst<bool>()) + { + continue; + } + } + // get the model value of each enumerator + enums.insert(enums.end(), uenums.begin(), uenums.end()); + } + } } } @@ -118,10 +144,15 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, // if we didn't satisfy the specification, there is no way to repair return false; } + // build model value map + std::map<Node, Node> mvMap; + for (unsigned i = 0, size = enums.size(); i < size; i++) + { + mvMap[enums[i]] = enum_values[i]; + } // the unification enumerators (return values, conditions) and their model // values NodeManager* nm = NodeManager::currentNM(); - Valuation& valuation = d_qe->getValuation(); bool addedUnifEnumSymBreakLemma = false; Node cost_lit = d_u_enum_manager.getAssertedLiteral(); std::map<Node, std::vector<Node>> unif_enums[2]; @@ -143,11 +174,7 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, { Assert(unif_enums[index][e].size() == 1); Node eu = unif_enums[index][e][0]; - Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); - // If active guard for this enumerator is not true, there are no more - // values for it, and hence we ignore it - Node gstatus = valuation.getSatValue(g); - if (gstatus.isNull() || !gstatus.getConst<bool>()) + if (mvMap.find(eu) == mvMap.end()) { Trace("cegis") << " " << eu << " -> N/A\n"; unif_enums[index][e].clear(); @@ -157,7 +184,8 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, // get the model value of each enumerator for (const Node& eu : unif_enums[index][e]) { - Node m_eu = d_parent->getModelValue(eu); + Assert(mvMap.find(eu) != mvMap.end()); + Node m_eu = mvMap[eu]; if (Trace.isOn("cegis")) { Trace("cegis") << " " << eu << " -> "; @@ -232,11 +260,16 @@ bool CegisUnif::processConstructCandidates(const std::vector<Node>& enums, if (options::sygusUnifCondIndependent() && !unif_enums[1][e].empty()) { Node eu = unif_enums[1][e][0]; - Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); - Node exp_exc = d_tds->getExplain() - ->getExplanationForEquality(eu, unif_values[1][e][0]) - .negate(); - lems.push_back(nm->mkNode(OR, g.negate(), exp_exc)); + Assert(d_tds->isEnumerator(eu)); + if (d_tds->isPassiveEnumerator(eu)) + { + Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu); + Node exp_exc = + d_tds->getExplain() + ->getExplanationForEquality(eu, unif_values[1][e][0]) + .negate(); + lems.push_back(nm->mkNode(OR, g.negate(), exp_exc)); + } } } } diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index c1b12dfd0..02cf1cdf2 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -71,6 +71,16 @@ class SygusModule */ virtual void getTermList(const std::vector<Node>& candidates, std::vector<Node>& terms) = 0; + /** allow partial model + * + * This method returns true if this module does not require that all + * terms returned by getTermList have "proper" model values when calling + * constructCandidates. A term may have a model value that is not proper + * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model + * values that are not proper are replaced by "null" when calling + * constructCandidates. + */ + virtual bool allowPartialModel() { return false; } /** construct candidate * * This function takes as input: diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 9a6645560..b7e6e0c65 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -415,6 +415,8 @@ void SygusPbe::getTermList(const std::vector<Node>& candidates, } } +bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); } + bool SygusPbe::constructCandidates(const std::vector<Node>& enums, const std::vector<Node>& enum_values, const std::vector<Node>& candidates, @@ -431,10 +433,18 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, Trace("sygus-pbe-enum") << " " << enums[i] << " -> "; TermDbSygus::toStreamSygus("sygus-pbe-enum", enum_values[i]); Trace("sygus-pbe-enum") << std::endl; - unsigned sz = d_tds->getSygusTermSize( enum_values[i] ); - szs.push_back(sz); - if( i==0 || sz<min_term_size ){ - min_term_size = sz; + if (!enum_values[i].isNull()) + { + unsigned sz = d_tds->getSygusTermSize(enum_values[i]); + szs.push_back(sz); + if (i == 0 || sz < min_term_size) + { + min_term_size = sz; + } + } + else + { + szs.push_back(0); } } // Assume two enumerators of types T1 and T2. @@ -448,11 +458,14 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, std::vector<unsigned> enum_consider; for (unsigned i = 0, esize = enums.size(); i < esize; i++) { - Assert(szs[i] >= min_term_size); - int diff = szs[i] - min_term_size; - if (!options::sygusPbeMultiFair() || diff <= diffAllow) + if (!enum_values[i].isNull()) { - enum_consider.push_back( i ); + Assert(szs[i] >= min_term_size); + int diff = szs[i] - min_term_size; + if (!options::sygusPbeMultiFair() || diff <= diffAllow) + { + enum_consider.push_back(i); + } } } @@ -468,14 +481,17 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums, Node c = d_enum_to_candidate[e]; std::vector<Node> enum_lems; d_sygus_unif[c].notifyEnumeration(e, v, enum_lems); - // the lemmas must be guarded by the active guard of the enumerator - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; - for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + if (!enum_lems.empty()) { - enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + // the lemmas must be guarded by the active guard of the enumerator + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + for (unsigned j = 0, size = enum_lems.size(); j < size; j++) + { + enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + } + lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } - lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } } for( unsigned i=0; i<candidates.size(); i++ ){ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 66e19b6c9..b2ad5f63a 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -117,6 +117,11 @@ class SygusPbe : public SygusModule */ void getTermList(const std::vector<Node>& candidates, std::vector<Node>& terms) override; + /** + * PBE allows partial models to handle multiple enumerators if we are not + * using a strictly fair enumeration strategy. + */ + bool allowPartialModel() override; /** construct candidates * * This function attempts to use unification-based approaches for constructing diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index eca88cab8..4fe3cfbed 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -562,7 +562,10 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) // is it excluded for domain-specific reason? std::vector<Node> exp_exc_vec; - if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) + Assert(d_tds->isEnumerator(e)); + bool isPassive = d_tds->isPassiveEnumerator(e); + if (isPassive + && getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec)) { Assert(!exp_exc_vec.empty()); exp_exc = exp_exc_vec.size() == 1 @@ -707,16 +710,20 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) } } - // exclude this value on subsequent iterations - if (exp_exc.isNull()) + if (isPassive) { - // if we did not already explain why this should be excluded, use default - exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v); + // exclude this value on subsequent iterations + if (exp_exc.isNull()) + { + Trace("sygus-sui-enum-lemma") << "Use basic exclusion." << std::endl; + // if we did not already explain why this should be excluded, use default + exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v); + } + exp_exc = exp_exc.negate(); + Trace("sygus-sui-enum-lemma") + << "SygusUnifIo : enumeration exclude lemma : " << exp_exc << std::endl; + lemmas.push_back(exp_exc); } - exp_exc = exp_exc.negate(); - Trace("sygus-sui-enum-lemma") - << "SygusUnifIo : enumeration exclude lemma : " << exp_exc << std::endl; - lemmas.push_back(exp_exc); } bool SygusUnifIo::constructSolution(std::vector<Node>& sols, diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index fde69d196..99f1131fe 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -40,6 +41,7 @@ namespace quantifiers { SynthConjecture::SynthConjecture(QuantifiersEngine* qe) : d_qe(qe), + d_tds(qe->getTermDatabaseSygus()), d_ceg_si(new CegSingleInv(qe, this)), d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), @@ -338,7 +340,14 @@ void SynthConjecture::doCheck(std::vector<Node>& lems) // get the model value of the relevant terms from the master module std::vector<Node> enum_values; - getModelValues(terms, enum_values); + bool fullModel = getEnumeratedValues(terms, enum_values); + + // if the master requires a full model and the model is partial, we fail + if (!d_master->allowPartialModel() && !fullModel) + { + Trace("cegqi-check") << "...partial model, fail." << std::endl; + return; + } if (!constructed_cand) { @@ -442,7 +451,7 @@ void SynthConjecture::doCheck(std::vector<Node>& lems) // eagerly unfold applications of evaluation function Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl; std::map<Node, Node> visited_n; - lem = d_qe->getTermDatabaseSygus()->getEagerUnfold(lem, visited_n); + lem = d_tds->getEagerUnfold(lem, visited_n); // record the instantiation // this is used for remembering the solution recordInstantiation(candidate_values); @@ -534,7 +543,12 @@ void SynthConjecture::doRefine(std::vector<Node>& lems) if (d_ce_sk_var_mvs.empty()) { std::vector<Node> model_values; - getModelValues(d_ce_sk_vars, model_values); + for (const Node& v : d_ce_sk_vars) + { + Node mv = getModelValue(v); + Trace("cegqi-refine") << " " << v << " -> " << mv << std::endl; + model_values.push_back(mv); + } sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); } else @@ -586,30 +600,59 @@ void SynthConjecture::preregisterConjecture(Node q) d_ceg_si->preregisterConjecture(q); } -void SynthConjecture::getModelValues(std::vector<Node>& n, std::vector<Node>& v) +bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n, + std::vector<Node>& v) { + bool ret = true; Trace("cegqi-engine") << " * Value is : "; for (unsigned i = 0; i < n.size(); i++) { - Node nv = getModelValue(n[i]); + Node nv = getEnumeratedValue(n[i]); v.push_back(nv); + ret = ret && !nv.isNull(); if (Trace.isOn("cegqi-engine")) { - TypeNode tn = nv.getType(); - Trace("cegqi-engine") << n[i] << " -> "; + Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv; + TypeNode tn = onv.getType(); std::stringstream ss; - Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv); - Trace("cegqi-engine") << ss.str() << " "; - if (Trace.isOn("cegqi-engine-rr")) + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv); + Trace("cegqi-engine") << n[i] << " -> "; + if (nv.isNull()) { - Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn); - bv = Rewriter::rewrite(bv); - Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + Trace("cegqi-engine") << "[EXC: " << ss.str() << "] "; + } + else + { + Trace("cegqi-engine") << ss.str() << " "; + if (Trace.isOn("cegqi-engine-rr")) + { + Node bv = d_tds->sygusToBuiltin(nv, tn); + bv = Rewriter::rewrite(bv); + Trace("cegqi-engine-rr") << " -> " << bv << std::endl; + } } } - Assert(!nv.isNull()); } Trace("cegqi-engine") << std::endl; + return ret; +} + +Node SynthConjecture::getEnumeratedValue(Node e) +{ + if (e.getAttribute(SygusSymBreakExcAttribute())) + { + // if the current model value of e was excluded by symmetry breaking, then + // it does not have a proper model value that we should consider, thus we + // return null. + return Node::null(); + } + if (d_tds->isPassiveEnumerator(e)) + { + return getModelValue(e); + } + Assert(false); + // management of actively generated enumerators goes here + return getModelValue(e); } Node SynthConjecture::getModelValue(Node n) @@ -692,8 +735,7 @@ void SynthConjecture::printAndContinueStream() { sol = d_cinfo[cprog].d_inst.back(); // add to explanation of exclusion - d_qe->getTermDatabaseSygus()->getExplain()->getExplanationForEquality( - cprog, sol, exp); + d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp); } } Assert(!exp.empty()); @@ -791,7 +833,6 @@ void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map, bool singleInvocation) { NodeManager* nm = NodeManager::currentNM(); - TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); std::vector<Node> sols; std::vector<int> statuses; if (!getSynthSolutionsInternal(sols, statuses, singleInvocation)) @@ -807,7 +848,7 @@ void SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map, if (status != 0) { // convert sygus to builtin here - bsol = sygusDb->sygusToBuiltin(sol, sol.getType()); + bsol = d_tds->sygusToBuiltin(sol, sol.getType()); } // convert to lambda TypeNode tn = d_embed_quant[0][i].getType(); @@ -868,8 +909,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols, { TNode templa = d_ceg_si->getTemplateArg(sf); // make the builtin version of the full solution - TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus(); - sol = sygusDb->sygusToBuiltin(sol, sol.getType()); + sol = d_tds->sygusToBuiltin(sol, sol.getType()); Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl; TNode tsol = sol; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1cbd4e949..694e4a0cb 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -112,9 +112,19 @@ class SynthConjecture void assign(Node q); /** has a conjecture been assigned to this class */ bool isAssigned() { return !d_embed_quant.isNull(); } - /** get model values for terms n, store in vector v */ - void getModelValues(std::vector<Node>& n, std::vector<Node>& v); - /** get model value for term n */ + /** + * Get model values for terms n, store in vector v. This method returns true + * if and only if all values added to v are non-null. + */ + bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v); + /** + * Get model value for term n. If n has a value that was excluded by + * datatypes sygus symmetry breaking, this method returns null. + */ + Node getEnumeratedValue(Node n); + /** + * Get model value for term n. + */ Node getModelValue(Node n); /** get utility for static preprocessing and analysis of conjectures */ @@ -132,6 +142,8 @@ class SynthConjecture private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** term database sygus of d_qe */ + TermDbSygus* d_tds; /** The feasible guard. */ Node d_feasible_guard; /** the decision strategy for the feasible guard */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 56844ec1f..296c10ff6 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -42,8 +42,7 @@ SynthEngine::~SynthEngine() { delete d_conj; } bool SynthEngine::needsCheck(Theory::Effort e) { - return !d_quantEngine->getTheoryEngine()->needCheck() - && e >= Theory::EFFORT_LAST_CALL; + return e >= Theory::EFFORT_LAST_CALL; } QuantifiersModule::QEffort SynthEngine::needsModel(Theory::Effort e) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 1f4e34c1f..23b35cfed 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -343,6 +343,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { } }else{ // no arguments to synthesis functions + d_var_list[tn].clear(); } // register connected types for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) @@ -421,11 +422,51 @@ void TermDbSygus::registerSygusType( TypeNode tn ) { } } +/** A trie indexed by types that assigns unique identifiers to nodes. */ +class TypeNodeIdTrie +{ + public: + /** children of this node */ + std::map<TypeNode, TypeNodeIdTrie> d_children; + /** the data stored at this node */ + std::vector<Node> d_data; + /** add v to this trie, indexed by types */ + void add(Node v, std::vector<TypeNode>& types) + { + TypeNodeIdTrie* tnt = this; + for (unsigned i = 0, size = types.size(); i < size; i++) + { + tnt = &tnt->d_children[types[i]]; + } + tnt->d_data.push_back(v); + } + /** + * Assign each node in this trie an identifier such that + * assign[v1] = assign[v2] iff v1 and v2 are indexed by the same values. + */ + void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount) + { + if (!d_data.empty()) + { + for (const Node& v : d_data) + { + assign[v] = idCount; + } + idCount++; + } + for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children) + { + c.second.assignIds(assign, idCount); + } + } +}; + void TermDbSygus::registerEnumerator(Node e, Node f, SynthConjecture* conj, bool mkActiveGuard, - bool useSymbolicCons) + bool useSymbolicCons, + bool isVarAgnostic) { if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end()) { @@ -441,15 +482,10 @@ void TermDbSygus::registerEnumerator(Node e, NodeManager* nm = NodeManager::currentNM(); if( mkActiveGuard ){ // make the guard - Node eg = Rewriter::rewrite(nm->mkSkolem("eG", nm->booleanType())); - eg = d_quantEngine->getValuation().ensureLiteral( eg ); - AlwaysAssert( !eg.isNull() ); - d_quantEngine->getOutputChannel().requirePhase( eg, true ); - //add immediate lemma - Node lem = nm->mkNode(OR, eg, eg.negate()); - Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem ); - d_enum_to_active_guard[e] = eg; + Node ag = nm->mkSkolem("eG", nm->booleanType()); + // must ensure it is a literal immediately here + ag = d_quantEngine->getValuation().ensureLiteral(ag); + d_enum_to_active_guard[e] = ag; } Trace("sygus-db") << " registering symmetry breaking clauses..." @@ -459,35 +495,47 @@ void TermDbSygus::registerEnumerator(Node e, // breaking lemma templates for each relevant subtype of the grammar std::vector<TypeNode> sf_types; getSubfieldTypes(et, sf_types); + // maps variables to the list of subfield types they occur in + std::map<Node, std::vector<TypeNode> > type_occurs; + std::map<TypeNode, std::vector<Node> >::iterator itv = d_var_list.find(et); + Assert(itv != d_var_list.end()); + for (const Node& v : itv->second) + { + type_occurs[v].clear(); + } // for each type of subfield type of this enumerator for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++) { std::vector<unsigned> rm_indices; TypeNode stn = sf_types[i]; Assert(stn.isDatatype()); - const Datatype& dt = static_cast<DatatypeType>(stn.toType()).getDatatype(); - std::map<TypeNode, unsigned>::iterator itsa = - d_sym_cons_any_constant.find(stn); - if (itsa != d_sym_cons_any_constant.end()) + const Datatype& dt = stn.getDatatype(); + int anyC = getAnyConstantConsNum(stn); + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { - if (!useSymbolicCons) + Expr sop = dt[i].getSygusOp(); + Assert(!sop.isNull()); + bool isAnyC = static_cast<int>(i) == anyC; + Node sopn = Node::fromExpr(sop); + if (type_occurs.find(sopn) != type_occurs.end()) + { + // if it is a variable, store that it occurs in stn + type_occurs[sopn].push_back(stn); + } + else if (isAnyC && !useSymbolicCons) { + // if we are not using the any constant constructor // do not use the symbolic constructor - rm_indices.push_back(itsa->second); + rm_indices.push_back(i); } - else + else if (anyC != -1 && !isAnyC && useSymbolicCons) { - // can remove all other concrete constant constructors - for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + // if we are using the any constant constructor, do not use any + // concrete constant + Node c_op = getConsNumConst(stn, i); + if (!c_op.isNull()) { - if (i != itsa->second) - { - Node c_op = getConsNumConst(stn, i); - if (!c_op.isNull()) - { - rm_indices.push_back(i); - } - } + rm_indices.push_back(i); } } } @@ -515,6 +563,33 @@ void TermDbSygus::registerEnumerator(Node e, } } Trace("sygus-db") << " ...finished" << std::endl; + + d_enum_var_agnostic[e] = isVarAgnostic; + if (isVarAgnostic) + { + // if not done so already, compute type class identifiers for each variable + if (d_var_subclass_id.find(et) == d_var_subclass_id.end()) + { + d_var_subclass_id[et].clear(); + TypeNodeIdTrie tnit; + for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs) + { + tnit.add(to.first, to.second); + } + // 0 is reserved for "no type class id" + unsigned typeIdCount = 1; + tnit.assignIds(d_var_subclass_id[et], typeIdCount); + // assign the list and reverse map to index + for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs) + { + Node v = to.first; + unsigned sc = d_var_subclass_id[et][v]; + Trace("sygus-db") << v << " has subclass id " << sc << std::endl; + d_var_subclass_list_index[et][v] = d_var_subclass_list[et][sc].size(); + d_var_subclass_list[et][sc].push_back(v); + } + } + } } bool TermDbSygus::isEnumerator(Node e) const @@ -561,6 +636,26 @@ bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const return false; } +bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const +{ + std::map<Node, bool>::const_iterator itus = d_enum_var_agnostic.find(e); + if (itus != d_enum_var_agnostic.end()) + { + return itus->second; + } + return false; +} + +bool TermDbSygus::isPassiveEnumerator(Node e) const +{ + if (isVariableAgnosticEnumerator(e)) + { + return false; + } + // other criteria go here + return true; +} + void TermDbSygus::getEnumerators(std::vector<Node>& mts) { for (std::map<Node, SynthConjecture*>::iterator itm = @@ -881,6 +976,82 @@ bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end(); } +unsigned TermDbSygus::getSubclassForVar(TypeNode tn, Node n) const +{ + std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itc = + d_var_subclass_id.find(tn); + if (itc == d_var_subclass_id.end()) + { + Assert(false); + return 0; + } + std::map<Node, unsigned>::const_iterator itcc = itc->second.find(n); + if (itcc == itc->second.end()) + { + Assert(false); + return 0; + } + return itcc->second; +} + +unsigned TermDbSygus::getNumSubclassVars(TypeNode tn, unsigned sc) const +{ + std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator + itv = d_var_subclass_list.find(tn); + if (itv == d_var_subclass_list.end()) + { + Assert(false); + return 0; + } + std::map<unsigned, std::vector<Node> >::const_iterator itvv = + itv->second.find(sc); + if (itvv == itv->second.end()) + { + Assert(false); + return 0; + } + return itvv->second.size(); +} +Node TermDbSygus::getVarSubclassIndex(TypeNode tn, + unsigned sc, + unsigned i) const +{ + std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator + itv = d_var_subclass_list.find(tn); + if (itv == d_var_subclass_list.end()) + { + Assert(false); + return Node::null(); + } + std::map<unsigned, std::vector<Node> >::const_iterator itvv = + itv->second.find(sc); + if (itvv == itv->second.end() || i >= itvv->second.size()) + { + Assert(false); + return Node::null(); + } + return itvv->second[i]; +} + +bool TermDbSygus::getIndexInSubclassForVar(TypeNode tn, + Node v, + unsigned& index) const +{ + std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itv = + d_var_subclass_list_index.find(tn); + if (itv == d_var_subclass_list_index.end()) + { + return false; + } + std::map<Node, unsigned>::const_iterator itvv = itv->second.find(v); + if (itvv == itv->second.end()) + { + return false; + } + index = itvv->second; + return true; +} + bool TermDbSygus::isSymbolicConsApp(Node n) const { if (n.getKind() != APPLY_CONSTRUCTOR) diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index b7bdba3ab..785e8731c 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -69,6 +69,10 @@ class TermDbSygus { * (see d_enum_to_active_guard), * useSymbolicCons : whether we want model values for e to include symbolic * constructors like the "any constant" variable. + * isVarAgnostic : if this flag is true, the enumerator will only generate + * values whose variables are in canonical order (for example, only x1-x2 + * and not x2-x1 will be generated, assuming x1 and x2 are in the same + * "subclass", see getSubclassForVar). * * Notice that enumerator e may not be one-to-one with f in * synthesis-through-unification approaches (e.g. decision tree construction @@ -78,7 +82,8 @@ class TermDbSygus { Node f, SynthConjecture* conj, bool mkActiveGuard = false, - bool useSymbolicCons = false); + bool useSymbolicCons = false, + bool isVarAgnostic = false); /** is e an enumerator registered with this class? */ bool isEnumerator(Node e) const; /** return the conjecture e is associated with */ @@ -89,6 +94,26 @@ class TermDbSygus { Node getActiveGuardForEnumerator(Node e) const; /** are we using symbolic constructors for enumerator e? */ bool usingSymbolicConsForEnumerator(Node e) const; + /** is this enumerator agnostic to variables? */ + bool isVariableAgnosticEnumerator(Node e) const; + /** is this a "passively-generated" enumerator? + * + * A "passively-generated" enumerator is one for which the terms it enumerates + * are obtained by looking at its model value only. For passively-generated + * enumerators, it is the responsibility of the user of that enumerator (say + * a SygusModule) to block the current model value of it before asking for + * another value. By default, the Cegis module uses passively-generated + * enumerators and "conjecture-specific refinement" to rule out models + * for passively-generated enumerators. + * + * On the other hand, an "actively-generated" enumerator is one for which the + * terms it enumerates are not necessarily a subset of the model values the + * enumerator takes. Actively-generated enumerators are centrally managed by + * SynthConjecture. The user of actively-generated enumerators are prohibited + * from influencing its model value. For example, conjecture-specific + * refinement in Cegis is not applied to actively-generated enumerators. + */ + bool isPassiveEnumerator(Node e) const; /** get all registered enumerators */ void getEnumerators(std::vector<Node>& mts); /** Register symmetry breaking lemma @@ -273,6 +298,8 @@ class TermDbSygus { std::map<Node, TypeNode> d_sb_lemma_to_type; /** mapping from symmetry breaking lemmas to size */ std::map<Node, unsigned> d_sb_lemma_to_size; + /** enumerators to whether they are variable agnostic */ + std::map<Node, bool> d_enum_var_agnostic; //------------------------------end enumerators //-----------------------------conversion from sygus to builtin @@ -345,6 +372,17 @@ class TermDbSygus { * for this type. */ std::map<TypeNode, bool> d_has_subterm_sym_cons; + /** + * Map from sygus types and bound variables to their type subclass id. Note + * type class identifiers are computed for each type of registered sygus + * enumerators, but not all sygus types. For details, see getSubclassIdForVar. + */ + std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_id; + /** the list of variables with given subclass */ + std::map<TypeNode, std::map<unsigned, std::vector<Node> > > + d_var_subclass_list; + /** the index of each variable in the above list */ + std::map<TypeNode, std::map<Node, unsigned> > d_var_subclass_list_index; public: // general sygus utilities bool isRegistered(TypeNode tn) const; @@ -390,6 +428,45 @@ class TermDbSygus { * Returns true if any subterm of type tn can be a symbolic constructor. */ bool hasSubtermSymbolicCons(TypeNode tn) const; + //--------------------------------- variable subclasses + /** Get subclass id for variable + * + * This returns the "subclass" identifier for variable v in sygus + * type tn. A subclass identifier groups variables based on the sygus + * types they occur in: + * A -> A + B | C + C | x | y | z | w | u + * B -> y | z + * C -> u + * The variables in this grammar can be grouped according to the sygus types + * they appear in: + * { x,w } occur in A + * { y,z } occur in A,B + * { u } occurs in A,C + * We say that e.g. x, w are in the same subclass. + * + * If this method returns 0, then v is not a variable in sygus type tn. + * Otherwise, this method returns a positive value n, such that + * getSubclassIdForVar[v1] = getSubclassIdForVar[v2] iff v1 and v2 are in the + * same subclass. + * + * The type tn should be the type of an enumerator registered to this + * database, where notice that we do not compute this information for the + * subfield types of the enumerator. + */ + unsigned getSubclassForVar(TypeNode tn, Node v) const; + /** + * Get the number of variable in the subclass with identifier sc for type tn. + */ + unsigned getNumSubclassVars(TypeNode tn, unsigned sc) const; + /** Get the i^th variable in the subclass with identifier sc for type tn */ + Node getVarSubclassIndex(TypeNode tn, unsigned sc, unsigned i) const; + /** + * Get the a variable's index in its subclass list. This method returns true + * iff variable v has been assigned a subclass in tn. It updates index to + * be v's index iff the method returns true. + */ + bool getIndexInSubclassForVar(TypeNode tn, Node v, unsigned& index) const; + //--------------------------------- end variable subclasses /** return whether n is an application of a symbolic constructor */ bool isSymbolicConsApp(Node n) const; /** can construct kind |