diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 114 |
1 files changed, 63 insertions, 51 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 06b552276..a99e726b6 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -73,25 +73,32 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates, { for (const Node& c : candidates) { + // Non-unif candidate are themselves the enumerators if (!d_sygus_unif.usingUnif(c)) { enums.push_back(c); continue; } - Valuation& valuation = d_qe->getValuation(); - for (const Node& e : d_cond_enums) + // Collect heads of candidate + for (const Node& hd : d_sygus_unif.getEvalPointHeads(c)) { - Trace("cegis-unif-debug") << "Check conditional enumerator : " << e - << std::endl; - Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); - Node g = d_enum_to_active_guard[e]; - // Get whether the active guard for this enumerator is set. If so, then - // there may exist more values for it, and hence we add it to enums. - Node gstatus = valuation.getSatValue(g); - if (!gstatus.isNull() && gstatus.getConst<bool>()) - { - enums.push_back(e); - } + Trace("cegis-unif-enum-debug") << "......cand " << c << " with enum hd " + << hd << "\n"; + enums.push_back(hd); + } + } + // Collect condition enumerators + Valuation& valuation = d_qe->getValuation(); + for (const Node& e : d_cond_enums) + { + Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end()); + Node g = d_enum_to_active_guard[e]; + // Get whether the active guard for this enumerator is set. If so, then + // there may exist more values for it, and hence we add it to enums. + Node gstatus = valuation.getSatValue(g); + if (!gstatus.isNull() && gstatus.getConst<bool>()) + { + enums.push_back(e); } } } @@ -102,21 +109,15 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, std::vector<Node>& candidate_values, std::vector<Node>& lems) { - if (addEvalLemmas(enums, enum_values)) - { - Trace("cegis-unif-lemma") << "Added eval lemmas\n"; - return false; - } - unsigned min_term_size = 0; - std::vector<unsigned> enum_consider; NodeManager* nm = NodeManager::currentNM(); Trace("cegis-unif-enum") << "Register new enumerated values :\n"; for (unsigned i = 0, size = enums.size(); i < size; ++i) { - // Only conditional enumerators will be notified to unif utility - if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i]) - == d_cond_enums.end()) + // Non-unif enums (which are the very candidates) should not be notified + if (enums[i] == candidates[i] && !d_sygus_unif.usingUnif(enums[i])) { + Trace("cegis-unif-enum") << " Ignoring non-unif candidate " << enums[i] + << std::endl; continue; } if (Trace.isOn("cegis-unif-enum")) @@ -127,41 +128,43 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, ->toStreamSygus(ss, enum_values[i]); Trace("cegis-unif-enum") << ss.str() << std::endl; } - unsigned sz = d_tds->getSygusTermSize(enum_values[i]); - if (i == 0 || sz < min_term_size) - { - enum_consider.clear(); - min_term_size = sz; - enum_consider.push_back(i); - } - else if (sz == min_term_size) - { - enum_consider.push_back(i); - } - } - // only consider the enumerators that are at minimum size (for fairness) - Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / " - << enums.size() << std::endl; - for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i) - { - unsigned j = enum_consider[i]; - Node e = enums[j], v = enum_values[j]; + Node e = enums[i], v = enum_values[i]; std::vector<Node> enum_lems; d_sygus_unif.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]; + // introduce lemmas to exclude this value of a condition enumerator from + // future consideration + std::map<Node, Node>::iterator it = d_enum_to_active_guard.find(e); + if (it == d_enum_to_active_guard.end()) + { + continue; + } for (unsigned j = 0, size = enum_lems.size(); j < size; ++j) { - enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]); + enum_lems[j] = nm->mkNode(OR, it->second.negate(), enum_lems[j]); } lems.insert(lems.end(), enum_lems.begin(), enum_lems.end()); } - // divide-and-conquer solution bulding for candidates using unif util + // evaluate on refinement lemmas + if (addEvalLemmas(enums, enum_values)) + { + Trace("cegis-unif-lemma") << "Added eval lemmas\n"; + return false; + } + // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector<Node> sols; if (d_sygus_unif.constructSolution(sols)) { candidate_values.insert(candidate_values.end(), sols.begin(), sols.end()); + if (Trace.isOn("cegis-unif")) + { + Trace("cegis-unif") << "* Candidate solutions are:\n"; + for (const Node& sol : sols) + { + Trace("cegis-unif") + << "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n"; + } + Trace("cegis-unif") << "---CegisUnif Engine---\n"; + } return true; } return false; @@ -175,6 +178,7 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars, std::map<Node, std::vector<Node> > eval_pts; Node plem = d_sygus_unif.addRefLemma(lem, eval_pts); d_refinement_lemmas.push_back(plem); + Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n"; // Notify the enumeration manager if there are new evaluation points for (const std::pair<const Node, std::vector<Node> >& ep : eval_pts) { @@ -200,11 +204,14 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe, d_ret_dec(qe->getSatContext(), false), d_curr_guq_val(qe->getSatContext(), 0) { + d_initialized = false; d_tds = d_qe->getTermDatabaseSygus(); } void CegisUnifEnumManager::initialize(const std::vector<Node>& cs) { + Assert(!d_initialized); + d_initialized = true; if (cs.empty()) { return; @@ -234,6 +241,8 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c) for (const Node& ei : eis) { Assert(ei.getType() == ct); + Trace("cegis-unif-enum") << "...for cand " << c << " adding hd " << ei + << " at size " << p.first << "\n"; registerEvalPtAtSize(ct, ei, p.second, p.first); } } @@ -241,12 +250,12 @@ void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c) Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) { - // have we returned our decision in the current SAT context? - if (d_ret_dec.get()) + // are we not initialized or have we returned our decision in the current SAT + // context? + if (!d_initialized || d_ret_dec.get()) { return Node::null(); } - // only call this after initialization if (d_ce_info.empty()) { // if no enumerators, the decision is null @@ -257,7 +266,6 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) bool value; if (!d_qe->getValuation().hasSatValue(lit, value)) { - d_ret_dec = true; priority = 0; return lit; } @@ -267,6 +275,7 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) incrementNumEnumerators(); return getNextDecisionRequest(priority); } + d_ret_dec = true; return Node::null(); } @@ -308,6 +317,8 @@ void CegisUnifEnumManager::incrementNumEnumerators() TypeNode ct = ci.first; for (const Node& ei : ci.second.d_eval_points) { + Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei + << " to new size " << new_size << "\n"; registerEvalPtAtSize(ct, ei, new_lit, new_size); } } @@ -342,6 +353,7 @@ void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct, disj.push_back(ei.eqNode(itc->second.d_enums[i])); } Node lem = NodeManager::currentNM()->mkNode(OR, disj); + Trace("cegis-unif-enum") << "Adding lemma " << lem << "\n"; d_qe->getOutputChannel().lemma(lem); } |