<< hd << "\n";
enums.push_back(hd);
}
- // for each decision tree strategy allocated for c (these are referenced
- // by strategy points in d_cand_to_strat_pt[c])
- for (const Node& e : d_cand_to_strat_pt[c])
- {
- std::vector<Node> cenums;
- // also get the current conditional enumerators
- d_u_enum_manager.getCondEnumeratorsForStrategyPt(e, cenums);
- for (const Node& ce : cenums)
- {
- d_cenum_to_strat_pt[ce] = e;
- }
- // conditional enumerators are also part of list
- enums.insert(enums.end(), cenums.begin(), cenums.end());
- }
}
}
std::vector<Node>& candidate_values,
std::vector<Node>& lems)
{
- // build the values of the condition enumerators for each strategy point
- std::map<Node, std::vector<Node>> condition_map;
- Trace("cegis-unif-enum") << "Register new enumerated values :\n";
- // keep track of the relation between conditional enums and their values
- NodePairMap cenum_to_value;
- for (unsigned i = 0, size = enums.size(); i < size; ++i)
+ if (Trace.isOn("cegis-unif-enum"))
{
- // 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") << " Evaluation heads :\n";
+ for (unsigned i = 0, size = enums.size(); i < size; ++i)
{
- Trace("cegis-unif-enum") << " Ignoring non-unif candidate " << enums[i]
- << std::endl;
- continue;
- }
- if (Trace.isOn("cegis-unif-enum"))
- {
- Trace("cegis-unif-enum") << " " << enums[i] << " -> ";
+ Trace("cegis-unif-enum") << " " << enums[i] << " -> ";
std::stringstream ss;
Printer::getPrinter(options::outputLanguage())
->toStreamSygus(ss, enum_values[i]);
Trace("cegis-unif-enum") << ss.str() << std::endl;
}
- Node e = enums[i], v = enum_values[i];
- std::map<Node, Node>::iterator itc = d_cenum_to_strat_pt.find(e);
- if (itc != d_cenum_to_strat_pt.end())
- {
- cenum_to_value[e] = v;
- Trace("cegis-unif-enum") << " ...this is a condition for " << e << "\n";
- // it is the value of a current condition
- condition_map[itc->second].push_back(v);
- }
}
// evaluate on refinement lemmas
if (addEvalLemmas(enums, enum_values))
{
return false;
}
- // inform the unif utility that we are using these conditions
- for (const std::pair<const Node, std::vector<Node>> cs : condition_map)
+ // the unification enumerators (return values, conditions) and their model
+ // values
+ NodeManager* nm = NodeManager::currentNM();
+ bool addedUnifEnumSymBreakLemma = false;
+ std::map<Node, std::vector<Node>> unif_enums[2];
+ std::map<Node, std::vector<Node>> unif_values[2];
+ for (const Node& c : candidates)
+ {
+ // for each decision tree strategy allocated for c (these are referenced
+ // by strategy points in d_cand_to_strat_pt[c])
+ for (const Node& e : d_cand_to_strat_pt[c])
+ {
+ for (unsigned index = 0; index < 2; index++)
+ {
+ Trace("cegis-unif-enum")
+ << " " << (index == 0 ? "Return values" : "Conditions") << " for "
+ << e << ":\n";
+ // get the current unification enumerators
+ d_u_enum_manager.getEnumeratorsForStrategyPt(
+ e, unif_enums[index][e], index);
+ // get the model value of each enumerator
+ for (const Node& eu : unif_enums[index][e])
+ {
+ Node m_eu = d_parent->getModelValue(eu);
+ if (Trace.isOn("cegis-unif-enum"))
+ {
+ Trace("cegis-unif-enum") << " " << eu << " -> ";
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, m_eu);
+ Trace("cegis-unif-enum") << ss.str() << std::endl;
+ }
+ unif_values[index][e].push_back(m_eu);
+ }
+ // inter-enumerator symmetry breaking
+ // given a pool of unification enumerators eu_1, ..., eu_n,
+ // CegisUnifEnumManager insists that size(eu_1) <= ... <= size(eu_n).
+ // We additionally insist that M(eu_i) < M(eu_{i+1}) when
+ // size(eu_i) = size(eu_{i+1}), where < is pointer comparison.
+ // We enforce this below by adding symmetry breaking lemmas of the form
+ // ~( eu_i = M(eu_i) ^ eu_{i+1} = M(eu_{i+1} ) )
+ // when applicable.
+ for (unsigned j = 1, nenum = unif_values[index][e].size(); j < nenum;
+ j++)
+ {
+ Node prev_val = unif_values[index][e][j - 1];
+ Node curr_val = unif_values[index][e][j];
+ // compare the node values
+ if (curr_val < prev_val)
+ {
+ // must have the same size
+ unsigned prev_size = d_tds->getSygusTermSize(prev_val);
+ unsigned curr_size = d_tds->getSygusTermSize(curr_val);
+ Assert(prev_size <= curr_size);
+ if (curr_size == prev_size)
+ {
+ Node slem = nm->mkNode(AND,
+ unif_enums[index][e][j - 1].eqNode(
+ unif_values[index][e][j - 1]),
+ unif_enums[index][e][j].eqNode(
+ unif_values[index][e][j]))
+ .negate();
+ Trace("cegis-unif") << "CegisUnif::lemma, inter-unif-enumerator "
+ "symmetry breaking lemma : "
+ << slem << "\n";
+ d_qe->getOutputChannel().lemma(slem);
+ addedUnifEnumSymBreakLemma = true;
+ break;
+ }
+ }
+ }
+ }
+ }
+ }
+ if (addedUnifEnumSymBreakLemma)
+ {
+ return false;
+ }
+ // set the conditions
+ for (const Node& c : candidates)
{
- d_sygus_unif.setConditions(cs.first, cs.second);
+ for (const Node& e : d_cand_to_strat_pt[c])
+ {
+ d_sygus_unif.setConditions(e, unif_values[1][e]);
+ }
}
- // TODO : check symmetry breaking for enumerators
// build solutions (for unif candidates a divide-and-conquer approach is used)
std::vector<Node> sols;
if (d_sygus_unif.constructSolution(sols))
// Build separation lemma based on current size, and for each heads that
// could not be separated, the condition values currently enumerated for its
// decision tree
- NodeManager* nm = NodeManager::currentNM();
Node neg_cost_lit = d_u_enum_manager.getCurrentLiteral().negate();
std::vector<Node> cenums, cond_eqs;
for (std::pair<const Node, std::vector<Node>>& np : sepPairs)
{
+ Node e = np.first;
// Build equalities between condition enumerators associated with the
// strategy point whose decision tree could not separate the given heads
- d_u_enum_manager.getCondEnumeratorsForStrategyPt(np.first, cenums);
- for (const Node& ce : cenums)
+ std::vector<Node> cond_eqs;
+ std::map<Node, std::vector<Node>>::iterator itue = unif_enums[1].find(e);
+ Assert(itue != unif_enums[1].end());
+ std::map<Node, std::vector<Node>>::iterator ituv = unif_values[1].find(e);
+ Assert(ituv != unif_values[1].end());
+ Assert(itue->second.size() == ituv->second.size());
+ for (unsigned i = 0, size = itue->second.size(); i < size; i++)
{
- Assert(cenum_to_value.find(ce) != cenum_to_value.end());
- cond_eqs.push_back(nm->mkNode(EQUAL, ce, cenum_to_value[ce]));
+ cond_eqs.push_back(itue->second[i].eqNode(ituv->second[i]));
}
Assert(!cond_eqs.empty());
Node neg_conds_lit =
incrementNumEnumerators();
}
-void CegisUnifEnumManager::getCondEnumeratorsForStrategyPt(
- Node e, std::vector<Node>& ces) const
+void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
+ std::vector<Node>& es,
+ unsigned index) const
{
std::map<Node, StrategyPtInfo>::const_iterator itc = d_ce_info.find(e);
Assert(itc != d_ce_info.end());
- ces.insert(
- ces.end(), itc->second.d_enums[1].begin(), itc->second.d_enums[1].end());
+ es.insert(es.end(),
+ itc->second.d_enums[index].begin(),
+ itc->second.d_enums[index].end());
}
void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
projects / cvc5.git / commitdiff