This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).
In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:
- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.
A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.
There is also small improvements for trace messages.
read_only = true
help = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
-### Rewrite rules options
+### Rewrite rules options
[[option]]
name = "quantRewriteRules"
read_only = true
help = "add one instance of rewrite rule per round"
-### Induction options
+### Induction options
[[option]]
name = "quantInduction"
default = "false"
help = "Unification-based function synthesis"
+[[option]]
+ name = "sygusUnifCondIndependent"
+ category = "regular"
+ long = "sygus-unif-cond-independent"
+ type = "bool"
+ default = "false"
+ help = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
+
+[[option]]
+ name = "sygusUnifCondIndNoRepeatSol"
+ category = "regular"
+ long = "sygus-unif-cond-indpendent-no-repeat-sol"
+ type = "bool"
+ default = "true"
+ help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis"
+
[[option]]
name = "sygusBoolIteReturnConst"
category = "regular"
type = "bool"
default = "true"
help = "Minimize synthesis solutions"
-
+
[[option]]
name = "sygusEvalOpt"
category = "regular"
type = "bool"
default = "false"
help = "static inference techniques for computing whether arguments of functions-to-synthesize are relevant"
-
+
# Internal uses of sygus
[[option]]
Trace("cegis") << " Enumerators :\n";
for (unsigned i = 0, size = enums.size(); i < size; ++i)
{
- Trace("cegis") << " " << enums[i] << " -> ";
+ bool isUnit = false;
+ for (const Node& hd_unit : d_rl_eval_hds)
+ {
+ if (enums[i] == hd_unit[0])
+ {
+ isUnit = true;
+ break;
+ }
+ }
+ Trace("cegis") << " " << enums[i]
+ << (options::sygusUnif() && isUnit ? "*" : "") << " -> ";
std::stringstream ss;
Printer::getPrinter(options::outputLanguage())
->toStreamSygus(ss, enum_values[i]);
{
Node cond = d_sygus_unif.getConditionForEvaluationPoint(e);
Assert(!cond.isNull());
- Trace("cegis-unif") << " " << e << " with condition : " << cond
- << std::endl;
+ Trace("cegis-unif")
+ << " " << e << " with condition : " << cond << std::endl;
pt_to_cond[e] = cond;
}
}
// Collect heads of candidates
for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
{
- Trace("cegis-unif-enum-debug") << "......cand " << c << " with enum hd "
- << hd << "\n";
+ Trace("cegis-unif-enum-debug")
+ << "......cand " << c << " with enum hd " << hd << "\n";
enums.push_back(hd);
}
}
}
if (!satisfiedRl)
{
+ Trace("cegis-unif")
+ << "..added refinement lemmas\n---CegisUnif Engine---\n";
// if we didn't satisfy the specification, there is no way to repair
return false;
}
// 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.getCurrentLiteral();
std::map<Node, std::vector<Node>> unif_enums[2];
// get the current unification enumerators
d_u_enum_manager.getEnumeratorsForStrategyPt(
e, unif_enums[index][e], index);
+ if (index == 1 && options::sygusUnifCondIndependent())
+ {
+ 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>())
+ {
+ Trace("cegis") << " " << eu << " -> N/A\n";
+ unif_enums[index][e].clear();
+ continue;
+ }
+ }
// get the model value of each enumerator
for (const Node& eu : unif_enums[index][e])
{
}
unif_values[index][e].push_back(m_eu);
}
+ // inter-enumerator symmetry breaking for return values
if (index == 0)
{
- // 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
}
if (addedUnifEnumSymBreakLemma)
{
+ Trace("cegis-unif") << "..added unif enum symmetry breaking "
+ "lemma\n---CegisUnif Engine---\n";
return false;
}
// set the conditions
{
d_sygus_unif.setConditions(
e, cost_lit, unif_enums[1][e], unif_values[1][e]);
+ // if condition enumerator had value, exclude this value
+ 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));
+ }
}
}
// build solutions (for unif candidates a divide-and-conquer approach is used)
return true;
}
- Assert(!lemmas.empty());
+ // TODO tie this to the lemma for getting a new condition value
+ Assert(options::sygusUnifCondIndependent() || !lemmas.empty());
for (const Node& lem : lemmas)
{
- Trace("cegis-unif") << "CegisUnif::lemma, separation lemma : " << lem
- << "\n";
+ Trace("cegis-unif-lemma")
+ << "CegisUnif::lemma, separation lemma : " << lem << "\n";
d_qe->getOutputChannel().lemma(lem);
}
+ Trace("cegis-unif") << "..failed to separate heads\n---CegisUnif Engine---\n";
return false;
}
std::map<Node, std::vector<Node>> eval_pts;
Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
addRefinementLemma(plem);
- Trace("cegis-unif-lemma") << "* Refinement lemma:\n" << plem << "\n";
+ Trace("cegis-unif-lemma")
+ << "CegisUnif::lemma, refinement lemma : " << plem << "\n";
// Notify the enumeration manager if there are new evaluation points
for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
{
Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end());
- // Notify each startegy point of the respective candidate
+ // Notify each strategy point of the respective candidate
for (const Node& n : d_cand_to_strat_pt[ep.first])
{
d_u_enum_manager.registerEvalPts(ep.second, n);
std::map<Node, Node>::const_iterator itcc = e_to_cond.find(e);
Assert(itcc != e_to_cond.end());
Node cond = itcc->second;
- Trace("cegis-unif-enum-debug") << "...its condition strategy point is "
- << cond << "\n";
+ Trace("cegis-unif-enum-debug")
+ << "...its condition strategy point is " << cond << "\n";
d_ce_info[e].d_ce_type = cond.getType();
// initialize the symmetry breaking lemma templates
for (unsigned index = 0; index < 2; index++)
}
// initialize the current literal
incrementNumEnumerators();
+ // create single condition enumerator for each decision tree strategy
+ if (options::sygusUnifCondIndependent())
+ {
+ // allocate a condition enumerator for each candidate
+ for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
+ {
+ Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+ setUpEnumerator(ceu, ci.second, 1);
+ d_enum_to_active_guard[ceu] = d_tds->getActiveGuardForEnumerator(ceu);
+ }
+ }
}
void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
Assert(num_enums > 0);
if (index == 1)
{
- // we always use (cost-1) conditions
- num_enums = num_enums - 1;
+ // we always use (cost-1) conditions, or 1 if in the indepedent case
+ num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1;
}
if (num_enums > 0)
{
}
}
+Node CegisUnifEnumManager::getActiveGuardForEnumerator(Node e)
+{
+ Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
+ return d_enum_to_active_guard[e];
+}
+
+void CegisUnifEnumManager::setUpEnumerator(Node e,
+ StrategyPtInfo& si,
+ unsigned index)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ // instantiate template for removing redundant operators
+ if (!si.d_sbt_lemma_tmpl[index].first.isNull())
+ {
+ Node templ = si.d_sbt_lemma_tmpl[index].first;
+ TNode templ_var = si.d_sbt_lemma_tmpl[index].second;
+ Node sym_break_red_ops = templ.substitute(templ_var, e);
+ Trace("cegis-unif-enum-lemma")
+ << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
+ << sym_break_red_ops << "\n";
+ d_qe->getOutputChannel().lemma(sym_break_red_ops);
+ }
+ // symmetry breaking between enumerators
+ if (!si.d_enums[index].empty() && index == 0)
+ {
+ Node e_prev = si.d_enums[index].back();
+ Node size_e = nm->mkNode(DT_SIZE, e);
+ Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
+ Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
+ Trace("cegis-unif-enum-lemma")
+ << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
+ d_qe->getOutputChannel().lemma(sym_break);
+ }
+ // register the enumerator
+ si.d_enums[index].push_back(e);
+ Trace("cegis-unif-enum") << "* Registering new enumerator " << e
+ << " to strategy point " << si.d_pt << "\n";
+ d_tds->registerEnumerator(e, si.d_pt, d_parent);
+}
+
void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
{
// candidates of the same type are managed
TypeNode ct = c.getType();
Node eu = nm->mkSkolem("eu", ct);
Node ceu;
- if (!ci.second.d_enums[0].empty())
+ if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
{
// make a new conditional enumerator as well, starting the
// second type around
{
continue;
}
- // instantiate template for removing redundant operators
- if (!ci.second.d_sbt_lemma_tmpl[index].first.isNull())
- {
- Node templ = ci.second.d_sbt_lemma_tmpl[index].first;
- TNode templ_var = ci.second.d_sbt_lemma_tmpl[index].second;
- Node sym_break_red_ops = templ.substitute(templ_var, e);
- Trace("cegis-unif-enum-lemma")
- << "CegisUnifEnum::lemma, remove redundant ops of " << e << " : "
- << sym_break_red_ops << "\n";
- d_qe->getOutputChannel().lemma(sym_break_red_ops);
- }
- // symmetry breaking between enumerators
- 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);
- Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
- Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
- Trace("cegis-unif-enum-lemma")
- << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
- d_qe->getOutputChannel().lemma(sym_break);
- }
- // register the enumerator
- ci.second.d_enums[index].push_back(e);
- Trace("cegis-unif-enum") << "* Registering new enumerator " << e
- << " to strategy point " << ci.second.d_pt
- << "\n";
- d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
- // TODO symmetry breaking for making
- // e distinct from ei : (ci.second.d_enums[index] \ {e})
- // if its respective type has had at least
- // ci.second.d_enums[index].size() distinct values enumerated
+ setUpEnumerator(e, ci.second, index);
}
}
// register the evaluation points at the new value
disj.push_back(ei.eqNode(itc->second.d_enums[0][i]));
}
Node lem = NodeManager::currentNM()->mkNode(OR, disj);
- Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, domain:" << lem
- << "\n";
+ Trace("cegis-unif-enum-lemma")
+ << "CegisUnifEnum::lemma, domain:" << lem << "\n";
d_qe->getOutputChannel().lemma(lem);
}
* registerEvalPtAtValue on the output channel of d_qe.
*/
void registerEvalPts(const std::vector<Node>& eis, Node e);
+ /** Retrieves active guard for enumerator */
+ Node getActiveGuardForEnumerator(Node e);
/** get next decision request
*
* This function has the same contract as Theory::getNextDecisionRequest.
bool d_initialized;
/** null node */
Node d_null;
+ /** map from condition enumerators to active guards (in case they are
+ * enumerated indepedently of the return values) */
+ std::map<Node, Node> d_enum_to_active_guard;
/** information per initialized type */
class StrategyPtInfo
{
* current SAT context.
*/
context::CDO<unsigned> d_curr_guq_val;
+ /** Registers an enumerator and adds symmetry breaking lemmas
+ *
+ * The symmetry breaking lemmas are generated according to the stored
+ * information from the enumerator's respective strategy point and whether it
+ * is a condition or return value enumerator. For the latter we add symmetry
+ * breaking lemmas that force enumerators to consider values in an increasing
+ * order of size.
+ */
+ void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index);
/** increment the number of enumerators */
void incrementNumEnumerators();
/** get literal G_uq_n */
}
EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
Node sol = itd->second.buildSol(etis->d_cons, lemmas);
- if (sol.isNull())
- {
- Assert(!lemmas.empty());
- }
+ Assert(options::sygusUnifCondIndependent() || !sol.isNull()
+ || !lemmas.empty());
return sol;
}
// set new condition values
d_enums.insert(d_enums.end(), enums.begin(), enums.end());
d_conds.insert(d_conds.end(), conds.begin(), conds.end());
+ // add to condition pool
+ if (options::sygusUnifCondIndependent())
+ {
+ if (Trace.isOn("sygus-unif-cond-pool"))
+ {
+ d_cond_mvs.insert(conds.begin(), conds.end());
+ for (const Node& condv : conds)
+ {
+ if (d_cond_mvs.find(condv) == d_cond_mvs.end())
+ {
+ Trace("sygus-unif-cond-pool")
+ << " ...adding to condition pool : "
+ << d_unif->d_tds->sygusToBuiltin(condv, condv.getType()) << "\n";
+ }
+ }
+ }
+ }
}
unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const
return d_strategy_index;
}
-using UNodePair = std::pair<unsigned, Node>;
-
Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
std::vector<Node>& lemmas)
{
Trace("sygus-unif-sol") << "Decision::buildSol with " << d_hds.size()
<< " evaluation heads and " << d_conds.size()
<< " conditions..." << std::endl;
+
+ return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas)
+ : buildSolMinCond(cons, lemmas);
+}
+
+Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
+ std::vector<Node>& lemmas)
+{
+ // model values for evaluation heads
+ std::map<Node, Node> hd_mv;
+ // add conditions
+ d_conds.clear();
+ d_conds.insert(d_conds.end(), d_cond_mvs.begin(), d_cond_mvs.end());
+ unsigned num_conds = d_conds.size();
+ for (unsigned i = 0; i < num_conds; ++i)
+ {
+ d_pt_sep.d_trie.addClassifier(&d_pt_sep, i);
+ }
+ // add heads
+ for (const Node& e : d_hds)
+ {
+ Node v = d_unif->d_parent->getModelValue(e);
+ hd_mv[e] = v;
+ Node er = d_pt_sep.d_trie.add(e, &d_pt_sep, num_conds);
+ // are we in conflict?
+ if (er == e)
+ {
+ // new separation class, no conflict
+ continue;
+ }
+ Assert(hd_mv.find(er) != hd_mv.end());
+ // merged into separation class with same model value, no conflict
+ if (hd_mv[e] == hd_mv[er])
+ {
+ continue;
+ }
+ // conflict. Explanation?
+ Trace("sygus-unif-sol")
+ << " ...can't separate " << e << " from " << er << std::endl;
+ return Node::null();
+ }
+ Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+ Node sol = d_pt_sep.extractSol(cons, hd_mv);
+ // repeated solution
+ if (options::sygusUnifCondIndNoRepeatSol()
+ && d_sols.find(sol) != d_sols.end())
+ {
+ return Node::null();
+ }
+ d_sols.insert(sol);
+ return sol;
+}
+
+Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons,
+ std::vector<Node>& lemmas)
+{
NodeManager* nm = NodeManager::currentNM();
// model values for evaluation heads
std::map<Node, Node> hd_mv;
}
Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+ return d_pt_sep.extractSol(cons, hd_mv);
+}
+
+Node SygusUnifRl::DecisionTreeInfo::PointSeparator::extractSol(
+ Node cons, std::map<Node, Node>& hd_mv)
+{
// Traverse trie and build ITE with cons
+ NodeManager* nm = NodeManager::currentNM();
std::map<IndTriePair, Node> cache;
std::map<IndTriePair, Node>::iterator it;
std::vector<IndTriePair> visit;
unsigned index = 0;
LazyTrie* trie;
- IndTriePair root = IndTriePair(0, &d_pt_sep.d_trie.d_trie);
+ IndTriePair root = IndTriePair(0, &d_trie.d_trie);
visit.push_back(root);
while (!visit.empty())
{
{
Assert(hd_mv.find(trie->d_lazy_child) != hd_mv.end());
cache[cur] = hd_mv[trie->d_lazy_child];
- Trace("sygus-unif-sol-debug")
- << "......leaf, build "
- << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
- << "\n";
+ Trace("sygus-unif-sol-debug") << "......leaf, build "
+ << d_dt->d_unif->d_tds->sygusToBuiltin(
+ cache[cur], cache[cur].getType())
+ << "\n";
continue;
}
cache[cur] = Node::null();
Assert(trie->d_children.size() == 1 || trie->d_children.size() == 2);
std::vector<Node> children(4);
children[0] = cons;
- children[1] = d_conds[index];
+ children[1] = d_dt->d_conds[index];
unsigned i = 0;
for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
{
{
cache[cur] = children[i];
Trace("sygus-unif-sol-debug")
- << "......no cond, build "
- << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+ << "......no need for cond "
+ << d_dt->d_unif->d_tds->sygusToBuiltin(d_dt->d_conds[index],
+ d_dt->d_conds[index].getType())
+ << ", build "
+ << d_dt->d_unif->d_tds->sygusToBuiltin(cache[cur],
+ cache[cur].getType())
<< "\n";
continue;
}
cache[cur] = nm->mkNode(APPLY_CONSTRUCTOR, children);
Trace("sygus-unif-sol-debug")
<< "......build node "
- << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+ << d_dt->d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
<< "\n";
}
Assert(cache.find(root) != cache.end());
Assert(!cache.find(root)->second.isNull());
- Trace("sygus-unif-sol") << "...solution is "
- << d_unif->d_tds->sygusToBuiltin(
- cache[root], cache[root].getType())
- << "\n";
return cache[root];
}
unsigned strategy_index);
/** returns index of strategy information of strategy node for this DT */
unsigned getStrategyIndex() const;
- /** builds solution stored in DT, if any, using the given constructor
+ /** builds solution, if possible, using the given constructor
*
- * The DT contains a solution when no class contains two heads of evaluation
- * points with different model values, i.e. when all points that must be
- * separated indeed are separated by the current set of conditions.
- *
- * This method either returns a solution (if all points are separated).
- * It it fails, it adds a conflict lemma to lemmas.
+ * A solution is possible when all different valued heads can be separated,
+ * i.e. the current set of conditions separates them in a decision tree
*/
Node buildSol(Node cons, std::vector<Node>& lemmas);
+ /** bulids a solution by considering all condition values ever enumerated */
+ Node buildSolAllCond(Node cons, std::vector<Node>& lemmas);
+ /** builds a solution by incrementally adding points and conditions to DT
+ *
+ * Differently from the above method, here a condition is only added to the
+ * DT when it's necessary for resolving a separation conflict (i.e. heads
+ * with different values in the same leaf of the DT). Only one value per
+ * condition enumerated is considered.
+ *
+ * If a solution cannot be built, then there are more conflicts to be
+ * resolved than condition enumerators. A conflict lemma is added to lemmas
+ * that forces a new assigment in which the conflict is removed (heads are
+ * made equal) or a new condition is enumerated to try to separate them.
+ */
+ Node buildSolMinCond(Node cons, std::vector<Node>& lemmas);
/** reference to parent unif util */
SygusUnifRl* d_unif;
/** enumerator template (if no templates, nodes in pair are Node::null()) */
std::vector<Node> d_conds;
/** gathered evaluation point heads */
std::vector<Node> d_hds;
+ /** all enumerated model values for conditions */
+ std::unordered_set<Node, NodeHashFunction> d_cond_mvs;
/** get condition enumerator */
Node getConditionEnumerator() const { return d_cond_enum; }
/** set conditions */
const std::vector<Node>& conds);
private:
+ /** Accumulates solutions built when considering all enumerated condition
+ * values (which may generate repeated solutions) */
+ std::unordered_set<Node, NodeHashFunction> d_sols;
/**
* Conditional enumerator variables corresponding to the condition values in
* d_conds. These are used for generating separation lemmas during
/** the lazy trie for building the separation classes */
LazyTrieMulti d_trie;
+ /** extracts solution from decision tree built */
+ Node extractSol(Node cons, std::map<Node, Node>& hd_mv);
private:
/** reference to parent unif util */
projects / cvc5.git / commitdiff