diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_unif.cpp | 128 |
1 files changed, 50 insertions, 78 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index ac70a97b2..ab9834254 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -127,6 +127,7 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, // values NodeManager* nm = NodeManager::currentNM(); bool addedUnifEnumSymBreakLemma = false; + Node cost_lit = d_u_enum_manager.getCurrentLiteral(); std::map<Node, std::vector<Node>> unif_enums[2]; std::map<Node, std::vector<Node>> unif_values[2]; for (const Node& c : candidates) @@ -157,40 +158,47 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, } 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++) + if (index == 0) { - 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) + // 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. + // we only do this for return value enumerators, since condition + // enumerators cannot be ordered (their order is based on the + // seperation resolution scheme during model construction). + for (unsigned j = 1, nenum = unif_values[index][e].size(); j < nenum; + j++) { - // 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 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) { - 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; + // 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; + } } } } @@ -206,12 +214,14 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, { for (const Node& e : d_cand_to_strat_pt[c]) { - d_sygus_unif.setConditions(e, unif_values[1][e]); + d_sygus_unif.setConditions( + e, cost_lit, unif_enums[1][e], unif_values[1][e]); } } // build solutions (for unif candidates a divide-and-conquer approach is used) std::vector<Node> sols; - if (d_sygus_unif.constructSolution(sols)) + std::vector<Node> lemmas; + if (d_sygus_unif.constructSolution(sols, lemmas)) { candidate_values.insert(candidate_values.end(), sols.begin(), sols.end()); if (Trace.isOn("cegis-unif")) @@ -226,51 +236,13 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums, } return true; } - std::map<Node, std::vector<Node>> sepPairs; - if (d_sygus_unif.getSeparationPairs(sepPairs)) + + Assert(!lemmas.empty()); + for (const Node& lem : lemmas) { - // 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 - 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 - 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++) - { - cond_eqs.push_back(itue->second[i].eqNode(ituv->second[i])); - } - Assert(!cond_eqs.empty()); - Node neg_conds_lit = - cond_eqs.size() > 1 ? nm->mkNode(AND, cond_eqs) : cond_eqs[0]; - neg_conds_lit = neg_conds_lit.negate(); - for (const Node& eq : np.second) - { - // A separation lemma is of the shape - // (cost_n+1 ^ (c_1 = M(c_1) ^ ... ^ M(c_n))) => e_i = e_j - // in which cost_n+1 is the cost function for the size n+1, each c_k is - // a conditional enumerator associated with the respective decision - // tree, each M(c_k) its current model value, and e_i, e_j are two - // distinct heads that could not be separated by these condition values - // - // Such a lemma will force the ground solver, within the restrictions of - // the respective cost function, to make e_i and e_j equal or to come up - // with new values for the conditional enumerators such that we can try - Node sep_lemma = nm->mkNode(OR, neg_cost_lit, neg_conds_lit, eq); - Trace("cegis-unif") - << "CegisUnif::lemma, separation lemma : " << sep_lemma << "\n"; - d_qe->getOutputChannel().lemma(sep_lemma); - } - } + Trace("cegis-unif") << "CegisUnif::lemma, separation lemma : " << lem + << "\n"; + d_qe->getOutputChannel().lemma(lem); } return false; } @@ -478,7 +450,7 @@ void CegisUnifEnumManager::incrementNumEnumerators() d_qe->getOutputChannel().lemma(sym_break_red_ops); } // symmetry breaking between enumerators - if (!ci.second.d_enums[index].empty()) + if (!ci.second.d_enums[index].empty() && index == 0) { Node e_prev = ci.second.d_enums[index].back(); Node size_e = nm->mkNode(DT_SIZE, e); |