summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/cegis_unif.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp114
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback