const std::vector<Node>& candidates,
std::vector<Node>& lemmas)
{
- Trace("cegis-unif-debug") << "Initialize CegisUnif : " << n << std::endl;
- // Init UNIF util
+ Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
+ // list of strategy points for unification candidates
+ std::vector<Node> unif_candidate_pts;
+ // map from strategy points to their conditions
+ std::map<Node, Node> pt_to_cond;
+ // strategy lemmas for each strategy point
std::map<Node, std::vector<Node>> strategy_lemmas;
- d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, strategy_lemmas);
- std::vector<Node> unif_candidates;
- // Initialize enumerators for non-unif functions-to-synhesize
- for (const Node& c : candidates)
+ // Initialize strategies for all functions-to-synhesize
+ for (const Node& f : candidates)
{
- if (!d_sygus_unif.usingUnif(c))
+ // Init UNIF util for this candidate
+ d_sygus_unif.initializeCandidate(
+ d_qe, f, d_cand_to_strat_pt[f], strategy_lemmas);
+ if (!d_sygus_unif.usingUnif(f))
{
- Trace("cegis-unif") << "* non-unification candidate : " << c << std::endl;
- d_tds->registerEnumerator(c, c, d_parent);
+ Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
+ d_tds->registerEnumerator(f, f, d_parent);
}
else
{
- Trace("cegis-unif") << "* unification candidate : " << c << std::endl;
- unif_candidates.push_back(c);
+ Trace("cegis-unif") << "* unification candidate : " << f
+ << " with strategy points:" << std::endl;
+ std::vector<Node>& enums = d_cand_to_strat_pt[f];
+ unif_candidate_pts.insert(
+ unif_candidate_pts.end(), enums.begin(), enums.end());
+ // map strategy point to its condition in pt_to_cond
+ for (const Node& e : enums)
+ {
+ Node cond = d_sygus_unif.getConditionForEvaluationPoint(e);
+ Assert(!cond.isNull());
+ Trace("cegis-unif")
+ << " " << e << " with condition : " << cond << std::endl;
+ pt_to_cond[e] = cond;
+ }
}
}
- for (const Node& e : d_cond_enums)
- {
- Node g = d_tds->getActiveGuardForEnumerator(e);
- Assert(!g.isNull());
- d_enum_to_active_guard[e] = g;
- }
// initialize the enumeration manager
- d_u_enum_manager.initialize(unif_candidates, strategy_lemmas);
+ d_u_enum_manager.initialize(unif_candidate_pts, pt_to_cond, strategy_lemmas);
return true;
}
enums.push_back(c);
continue;
}
- // Collect heads of candidate
+ // 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";
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>())
+ // 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])
{
- enums.push_back(e);
+ 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)
{
- NodeManager* nm = NodeManager::currentNM();
+ // 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";
for (unsigned i = 0, size = enums.size(); i < size; ++i)
{
Trace("cegis-unif-enum") << ss.str() << std::endl;
}
Node e = enums[i], v = enum_values[i];
- std::vector<Node> enum_lems;
- d_sygus_unif.notifyEnumeration(e, v, enum_lems);
- // 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)
+ std::map<Node, Node>::iterator itc = d_cenum_to_strat_pt.find(e);
+ if (itc != d_cenum_to_strat_pt.end())
{
- enum_lems[j] = nm->mkNode(OR, it->second.negate(), enum_lems[j]);
+ 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);
}
- lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
}
// 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)
+ {
+ d_sygus_unif.setConditions(cs.first, cs.second);
+ }
+ // TODO : check symmetry breaking for enumerators
+ // TODO : check separation of evaluation heads wrt condition enumerators and
+ // add lemmas.
// build solutions (for unif candidates a divide-and-conquer approach is used)
std::vector<Node> sols;
if (d_sygus_unif.constructSolution(sols))
}
void CegisUnifEnumManager::initialize(
- const std::vector<Node>& cs,
+ const std::vector<Node>& es,
+ const std::map<Node, Node>& e_to_cond,
const std::map<Node, std::vector<Node>>& strategy_lemmas)
{
Assert(!d_initialized);
d_initialized = true;
- if (cs.empty())
+ if (es.empty())
{
return;
}
- // process strategy lemmas
- std::map<TypeNode, std::pair<Node, std::vector<Node>>> tn_strategy_lemmas;
- for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
- {
- if (Trace.isOn("cegis-unif-enum-debug"))
- {
- Trace("cegis-unif-enum-debug") << "...lemmas of strategy pt " << p.first
- << ":\n";
- for (const Node& lem : p.second)
- {
- Trace("cegis-unif-enum-debug") << "\t" << lem << "\n";
- }
- }
- TypeNode tn = p.first.getType();
- Assert(tn_strategy_lemmas.find(tn) == tn_strategy_lemmas.end());
- tn_strategy_lemmas[tn].first = p.first;
- tn_strategy_lemmas[tn].second = p.second;
- }
// initialize type information for candidates
NodeManager* nm = NodeManager::currentNM();
- for (const Node& c : cs)
+ for (const Node& e : es)
{
- Trace("cegis-unif-enum-debug") << "...adding candidate " << c << "\n";
+ Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n";
// currently, we allocate the same enumerators for candidates of the same
// type
- TypeNode tn = c.getType();
- d_ce_info[tn].d_candidates.push_back(c);
- // retrieve symmetry breaking lemma template for type if not already init
- if (!d_ce_info[tn].d_sbt_lemma.isNull())
- {
- continue;
- }
- std::map<const TypeNode, std::pair<Node, std::vector<Node>>>::iterator it =
- tn_strategy_lemmas.find(tn);
- if (it == tn_strategy_lemmas.end())
+ d_ce_info[e].d_pt = e;
+ 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";
+ d_ce_info[e].d_ce_type = cond.getType();
+ // initialize the symmetry breaking lemma templates
+ for (unsigned index = 0; index < 2; index++)
{
- continue;
+ Assert(d_ce_info[e].d_sbt_lemma_tmpl[index].first.isNull());
+ Node sp = index == 0 ? e : cond;
+ std::map<Node, std::vector<Node>>::const_iterator it =
+ strategy_lemmas.find(sp);
+ if (it == strategy_lemmas.end())
+ {
+ continue;
+ }
+ // collect lemmas for removing redundant ops for this candidate's type
+ Node d_sbt_lemma =
+ it->second.size() == 1 ? it->second[0] : nm->mkNode(AND, it->second);
+ Trace("cegis-unif-enum-debug")
+ << "...adding lemma template to remove redundant operators for " << sp
+ << " --> lambda " << sp << ". " << d_sbt_lemma << "\n";
+ d_ce_info[e].d_sbt_lemma_tmpl[index] =
+ std::pair<Node, Node>(d_sbt_lemma, sp);
}
- // collect lemmas for removing redundant ops for this candidate's type
- d_ce_info[tn].d_sbt_lemma = nm->mkNode(AND, it->second.second);
- Trace("cegis-unif-enum-debug")
- << "...adding lemma template to remove redundant operators for " << c
- << " and its type " << tn << " --> " << d_ce_info[tn].d_sbt_lemma
- << "\n";
- d_ce_info[tn].d_sbt_arg = it->second.first;
}
// initialize the current literal
incrementNumEnumerators();
}
-void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c)
+void CegisUnifEnumManager::getCondEnumeratorsForStrategyPt(
+ Node e, std::vector<Node>& ces) 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());
+}
+
+void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
{
// candidates of the same type are managed
- TypeNode ct = c.getType();
- std::map<TypeNode, TypeInfo>::iterator it = d_ce_info.find(ct);
+ std::map<Node, StrategyPtInfo>::iterator it = d_ce_info.find(e);
Assert(it != d_ce_info.end());
it->second.d_eval_points.insert(
it->second.d_eval_points.end(), eis.begin(), eis.end());
// register at all already allocated sizes
- for (const std::pair<const unsigned, Node>& p : d_guq_lit)
+ for (const Node& ei : eis)
{
- for (const Node& ei : eis)
+ Assert(ei.getType() == e.getType());
+ for (const std::pair<const unsigned, Node>& p : d_guq_lit)
{
- Assert(ei.getType() == ct);
- Trace("cegis-unif-enum") << "...for cand " << c << " adding hd " << ei
+ Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei
<< " at size " << p.first << "\n";
- registerEvalPtAtSize(ct, ei, p.second, p.first);
+ registerEvalPtAtSize(e, ei, p.second, p.first);
}
}
}
d_qe->getOutputChannel().requirePhase(new_lit, true);
d_guq_lit[new_size] = new_lit;
// allocate an enumerator for each candidate
- for (std::pair<const TypeNode, TypeInfo>& ci : d_ce_info)
+ for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
{
- TypeNode ct = ci.first;
+ Node c = ci.first;
+ TypeNode ct = c.getType();
Node eu = nm->mkSkolem("eu", ct);
- // instantiate template for removing redundant operators
- if (!ci.second.d_sbt_lemma.isNull())
+ Node ceu;
+ if (!ci.second.d_enums[0].empty())
{
- Node templ = ci.second.d_sbt_lemma;
- TNode templ_var = ci.second.d_sbt_arg;
- Node sym_break_red_ops = templ.substitute(templ_var, eu);
- Trace("cegis-unif-enum-lemma")
- << "CegisUnifEnum::lemma, remove redundant ops of " << eu << " : "
- << sym_break_red_ops << "\n";
- d_qe->getOutputChannel().lemma(sym_break_red_ops);
+ // make a new conditional enumerator as well, starting the
+ // second type around
+ ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
}
- if (!ci.second.d_enums.empty())
+ // register the new enumerators
+ for (unsigned index = 0; index < 2; index++)
{
- Node eu_prev = ci.second.d_enums.back();
- // symmetry breaking
- Node size_eu = nm->mkNode(DT_SIZE, eu);
- Node size_eu_prev = nm->mkNode(DT_SIZE, eu_prev);
- Node sym_break = nm->mkNode(GEQ, size_eu, size_eu_prev);
+ Node e = index == 0 ? eu : ceu;
+ if (e.isNull())
+ {
+ continue;
+ }
+ // register the enumerator
+ ci.second.d_enums[index].push_back(e);
+ d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
+ // 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
+ 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);
// if the sygus datatype is interpreted as an infinite type
// (this should be the case for almost all examples)
- if (!ct.isInterpretedFinite())
+ TypeNode et = e.getType();
+ if (!et.isInterpretedFinite())
{
// it is disequal from all previous ones
- for (const Node eui : ci.second.d_enums)
+ for (const Node ei : ci.second.d_enums[index])
{
- Node deq = eu.eqNode(eui).negate();
+ Node deq = e.eqNode(ei).negate();
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, enum deq:" << deq << "\n";
d_qe->getOutputChannel().lemma(deq);
}
}
}
- ci.second.d_enums.push_back(eu);
- d_tds->registerEnumerator(eu, d_null, d_parent);
}
// register the evaluation points at the new value
- for (std::pair<const TypeNode, TypeInfo>& ci : d_ce_info)
+ for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
{
- TypeNode ct = ci.first;
+ Node c = 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);
+ registerEvalPtAtSize(c, ei, new_lit, new_size);
}
}
}
return itc->second;
}
-void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct,
+void CegisUnifEnumManager::registerEvalPtAtSize(Node e,
Node ei,
Node guq_lit,
unsigned n)
{
// must be equal to one of the first n enums
- std::map<TypeNode, TypeInfo>::iterator itc = d_ce_info.find(ct);
+ std::map<Node, StrategyPtInfo>::iterator itc = d_ce_info.find(e);
Assert(itc != d_ce_info.end());
- Assert(itc->second.d_enums.size() >= n);
+ Assert(itc->second.d_enums[0].size() >= n);
std::vector<Node> disj;
disj.push_back(guq_lit.negate());
for (unsigned i = 0; i < n; i++)
{
- disj.push_back(ei.eqNode(itc->second.d_enums[i]));
+ 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
/** Cegis Unif Enumeration Manager
*
* This class enforces a decision heuristic that limits the number of
- * unique values given to the set of heads of evaluation points, which are
- * variables of sygus datatype type that are introduced by CegisUnif.
+ * unique values given to the set of heads of evaluation points and conditions
+ * enumerators for these points, which are variables of sygus datatype type that
+ * are introduced by CegisUnif.
*
* It maintains a set of guards, call them G_uq_1 ... G_uq_n, where the
* semantics of G_uq_i is "for each type, the heads of evaluation points of that
* type are interpreted as a value in a set whose cardinality is at most i".
+ * We also enforce that the number of condition enumerators for evaluation
+ * points is equal to (n-1).
*
* To enforce this, we introduce sygus enumerator(s) of the same type as the
- * heads of evaluation points registered to this class and add lemmas that
- * enforce that these terms are equal to at least one enumerator (see
- * registerEvalPtAtValue).
+ * heads of evaluation points and condition enumerators registered to this class
+ * and add lemmas that enforce that these terms are equal to at least one
+ * enumerator (see registerEvalPtAtValue).
*/
class CegisUnifEnumManager
{
/** initialize candidates
*
* Notify this class that it will be managing enumerators for the vector
- * of functions-to-synthesize (candidate variables) in candidates. This
- * function should only be called once.
+ * of strategy points es. This function should only be called once.
*
- * Each candidate c in cs should be such that we are using a
- * synthesis-by-unification approach for c.
+ * Each strategy point in es should be such that we are using a
+ * synthesis-by-unification approach for its candidate.
*/
- void initialize(const std::vector<Node>& cs,
+ void initialize(const std::vector<Node>& es,
+ const std::map<Node, Node>& e_to_cond,
const std::map<Node, std::vector<Node>>& strategy_lemmas);
+ /** get the current set of conditional enumerators for strategy point e */
+ void getCondEnumeratorsForStrategyPt(Node e, std::vector<Node>& ces) const;
/** register evaluation point for candidate
*
* This notifies this class that eis is a set of heads of evaluation points
- * for candidate c, where c should be a candidate that was passed to
- * initialize in the vector cs.
+ * for strategy point e, where e was passed to initialize in the vector es.
*
* This may add new lemmas of the form described above
* registerEvalPtAtValue on the output channel of d_qe.
*/
- void registerEvalPts(const std::vector<Node>& eis, Node c);
+ void registerEvalPts(const std::vector<Node>& eis, Node e);
/** get next decision request
*
* This function has the same contract as Theory::getNextDecisionRequest.
/** null node */
Node d_null;
/** information per initialized type */
- class TypeInfo
+ class StrategyPtInfo
{
public:
- TypeInfo() {}
- /** candidates for this type */
- std::vector<Node> d_candidates;
- /** the set of enumerators we have allocated for this candidate */
- std::vector<Node> d_enums;
- /** the set of evaluation points of this type */
+ StrategyPtInfo() {}
+ /** strategy point for this type */
+ Node d_pt;
+ /** the set of enumerators we have allocated for this strategy point
+ *
+ * Index 0 stores the return value enumerators, and index 1 stores the
+ * conditional enumerators. We have that
+ * d_enums[0].size()==d_enums[1].size()+1.
+ */
+ std::vector<Node> d_enums[2];
+ /** the type of conditional enumerators for this strategy point */
+ TypeNode d_ce_type;
+ /**
+ * The set of evaluation points of this type. In models, we ensure that
+ * each of these are equal to one of d_enums[0].
+ */
std::vector<Node> d_eval_points;
- /** symmetry breaking lemma template for this type */
- Node d_sbt_lemma;
- /** argument (to be instantiated) of symmetry breaking lemma template */
- Node d_sbt_arg;
+ /** symmetry breaking lemma template for this strategy point
+ *
+ * Each pair stores (the symmetry breaking lemma template, argument (to be
+ * instantiated) of symmetry breaking lemma template).
+ *
+ * Index 0 stores the symmetry breaking lemma template for return values,
+ * index 1 stores the template for conditions.
+ */
+ std::pair<Node, Node> d_sbt_lemma_tmpl[2];
};
- /** map types to the above info */
- std::map<TypeNode, TypeInfo> d_ce_info;
+ /** map strategy points to the above info */
+ std::map<Node, StrategyPtInfo> d_ce_info;
/** literals of the form G_uq_n for each n */
std::map<unsigned, Node> d_guq_lit;
/** Have we returned a decision in the current SAT context? */
* This sends a lemma of the form:
* G_uq_n => ei = d1 V ... V ei = dn
* on the output channel of d_qe, where d1...dn are sygus enumerators of the
- * same type (ct) as ei.
+ * same type as e and ei, and ei is an evaluation point of strategy point e.
*/
- void registerEvalPtAtSize(TypeNode ct, Node ei, Node guq_lit, unsigned n);
+ void registerEvalPtAtSize(Node e, Node ei, Node guq_lit, unsigned n);
};
/** Synthesizes functions in a data-driven SyGuS approach
SygusUnifRl d_sygus_unif;
/** enumerator manager utility */
CegisUnifEnumManager d_u_enum_manager;
- /**
- * list of conditonal enumerators to build solutions for candidates being
- * synthesized with unification techniques
- */
- std::vector<Node> d_cond_enums;
- /** map from enumerators to active guards */
- std::map<Node, Node> d_enum_to_active_guard;
/* The null node */
Node d_null;
+ /** list of strategy points per candidate */
+ std::map<Node, std::vector<Node>> d_cand_to_strat_pt;
+ /** map from conditional enumerators to their strategy point */
+ std::map<Node, Node> d_cenum_to_strat_pt;
}; /* class CegisUnif */
} // namespace quantifiers
Assert(d_examples.find(c) != d_examples.end());
Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
<< std::endl;
- std::vector<Node> singleton_c;
- singleton_c.push_back(c);
std::map<Node, std::vector<Node>> strategy_lemmas;
- d_sygus_unif[c].initialize(
- d_qe, singleton_c, d_candidate_to_enum[c], strategy_lemmas);
+ d_sygus_unif[c].initializeCandidate(
+ d_qe, c, d_candidate_to_enum[c], strategy_lemmas);
Assert(!d_candidate_to_enum[c].empty());
Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
<< " enumerators for " << c << "..." << std::endl;
SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
SygusUnif::~SygusUnif() {}
-void SygusUnif::initialize(QuantifiersEngine* qe,
- const std::vector<Node>& funs,
- std::vector<Node>& enums,
- std::map<Node, std::vector<Node>>& strategy_lemmas)
+
+void SygusUnif::initializeCandidate(
+ QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
- Assert(d_candidates.empty());
d_qe = qe;
d_tds = qe->getTermDatabaseSygus();
- for (const Node& f : funs)
- {
- d_candidates.push_back(f);
- // initialize the strategy
- d_strategy[f].initialize(qe, f, enums);
- }
+ d_candidates.push_back(f);
+ // initialize the strategy
+ d_strategy[f].initialize(qe, f, enums);
}
bool SygusUnif::constructSolution(std::vector<Node>& sols)
SygusUnif();
virtual ~SygusUnif();
- /** initialize
+ /** initialize candidate
*
- * This initializes this class with functions-to-synthesize funs. We also call
- * these "candidate variables".
+ * This initializes this class with functions-to-synthesize f. We also call
+ * this a "candidate variable". This function can be called more than once
+ * for different functions-to-synthesize in the same conjecture.
*
* This call constructs a set of enumerators for the relevant subfields of
* the grammar of f and adds them to enums. These enumerators are those that
* strategy is ITE_strat). The lemmas are associated with a strategy point of
* the respective function-to-synthesize.
*/
- virtual void initialize(QuantifiersEngine* qe,
- const std::vector<Node>& funs,
- std::vector<Node>& enums,
- std::map<Node, std::vector<Node>>& strategy_lemmas);
+ virtual void initializeCandidate(
+ QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::vector<Node>>& strategy_lemmas);
/**
* Notify that the value v has been enumerated for enumerator e. This call
}
SygusUnifIo::~SygusUnifIo() {}
-void SygusUnifIo::initialize(QuantifiersEngine* qe,
- const std::vector<Node>& funs,
- std::vector<Node>& enums,
- std::map<Node, std::vector<Node>>& strategy_lemmas)
+void SygusUnifIo::initializeCandidate(
+ QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
- Assert(funs.size() == 1);
d_examples.clear();
d_examples_out.clear();
d_ecache.clear();
- d_candidate = funs[0];
- SygusUnif::initialize(qe, funs, enums, strategy_lemmas);
+ d_candidate = f;
+ SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas);
// learn redundant operators based on the strategy
- d_strategy[d_candidate].staticLearnRedundantOps(strategy_lemmas);
+ d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
}
void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
/** initialize
*
- * The vector funs should be of length one, since I/O specifications across
+ * We only initialize for one function f, since I/O specifications across
* multiple functions can be separated.
*/
- void initialize(QuantifiersEngine* qe,
- const std::vector<Node>& funs,
- std::vector<Node>& enums,
- std::map<Node, std::vector<Node>>& strategy_lemmas) override;
+ void initializeCandidate(
+ QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::vector<Node>>& strategy_lemmas) override;
/** Notify enumeration */
void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
SygusUnifRl::SygusUnifRl(CegConjecture* p) : d_parent(p) {}
SygusUnifRl::~SygusUnifRl() {}
-void SygusUnifRl::initialize(QuantifiersEngine* qe,
- const std::vector<Node>& funs,
- std::vector<Node>& enums,
- std::map<Node, std::vector<Node>>& strategy_lemmas)
+void SygusUnifRl::initializeCandidate(
+ QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
// initialize
std::vector<Node> all_enums;
- SygusUnif::initialize(qe, funs, all_enums, strategy_lemmas);
+ SygusUnif::initializeCandidate(qe, f, all_enums, strategy_lemmas);
// based on the strategy inferred for each function, determine if we are
// using a unification strategy that is compatible our approach.
- for (const Node& f : funs)
- {
- d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
- registerStrategy(f, strategy_lemmas);
- }
- enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end());
+ d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
+ registerStrategy(f, enums);
// Copy candidates and check whether CegisUnif for any of them
- for (const Node& c : d_unif_candidates)
+ if (d_unif_candidates.find(f) != d_unif_candidates.end())
{
- d_hd_to_pt[c].clear();
- d_cand_to_eval_hds[c].clear();
- d_cand_to_hd_count[c] = 0;
+ d_hd_to_pt[f].clear();
+ d_cand_to_eval_hds[f].clear();
+ d_cand_to_hd_count[f] = 0;
}
}
void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
{
- Trace("sygus-unif-rl-notify") << "SyGuSUnifRl: Adding to enum " << e
- << " value " << v << "\n";
- // Exclude v from next enumerations for e
- Node exc_lemma =
- d_tds->getExplain()->getExplanationForEquality(e, v).negate();
- Trace("sygus-unif-rl-notify-debug")
- << "SygusUnifRl : enumeration exclude lemma : " << exc_lemma << std::endl;
- lemmas.push_back(exc_lemma);
- // Update all desicion trees in which this enumerator is a conditional
- // enumerator, if any
- std::map<Node, std::vector<Node>>::iterator it = d_cenum_to_stratpt.find(e);
- if (it == d_cenum_to_stratpt.end())
- {
- return;
- }
- for (const Node& stratpt : it->second)
- {
- Trace("sygus-unif-rl-dt")
- << "...adding value " << v
- << " to decision tree of strategy point : " << stratpt << std::endl;
- Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end());
- // Register new condition value
- d_stratpt_to_dt[stratpt].addCondValue(v);
- Trace("sygus-unif-rl-dt") << "...added\n";
- }
+ // we do not use notify enumeration
+ Assert(false);
}
Node SygusUnifRl::purifyLemma(Node n,
return itd->second.buildSol(etis->d_cons);
}
-bool SygusUnifRl::usingUnif(Node f)
+bool SygusUnifRl::usingUnif(Node f) const
{
return d_unif_candidates.find(f) != d_unif_candidates.end();
}
+Node SygusUnifRl::getConditionForEvaluationPoint(Node e) const
+{
+ std::map<Node, DecisionTreeInfo>::const_iterator it = d_stratpt_to_dt.find(e);
+ Assert(it != d_stratpt_to_dt.end());
+ return it->second.getConditionEnumerator();
+}
+
+void SygusUnifRl::setConditions(Node e, const std::vector<Node>& conds)
+{
+ std::map<Node, DecisionTreeInfo>::iterator it = d_stratpt_to_dt.find(e);
+ Assert(it != d_stratpt_to_dt.end());
+ it->second.clearCondValues();
+ /* TODO
+ for (const Node& c : conds)
+ {
+ it->second.addCondValue(c);
+ }
+ */
+}
+
std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
{
std::map<Node, std::vector<Node>>::iterator it = d_cand_to_eval_hds.find(c);
return it->second;
}
-void SygusUnifRl::registerStrategy(
- Node f, std::map<Node, std::vector<Node>>& strategy_lemmas)
+void SygusUnifRl::registerStrategy(Node f, std::vector<Node>& enums)
{
if (Trace.isOn("sygus-unif-rl-strat"))
{
Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
Node e = d_strategy[f].getRootEnumerator();
std::map<Node, std::map<NodeRole, bool>> visited;
- registerStrategyNode(f, e, role_equal, visited, strategy_lemmas);
+ registerStrategyNode(f, e, role_equal, visited, enums);
}
void SygusUnifRl::registerStrategyNode(
Node e,
NodeRole nrole,
std::map<Node, std::map<NodeRole, bool>>& visited,
- std::map<Node, std::vector<Node>>& strategy_lemmas)
+ std::vector<Node>& enums)
{
Trace("sygus-unif-rl-strat") << " register node " << e << std::endl;
if (visited[e].find(nrole) != visited[e].end())
<< " ...detected recursive ITE strategy, condition enumerator : "
<< cond << std::endl;
// indicate that we will be enumerating values for cond
- registerConditionalEnumerator(f, e, cond, j, strategy_lemmas);
+ registerConditionalEnumerator(f, e, cond, j);
+ // we will be using a strategy for e
+ enums.push_back(e);
}
}
// TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
}
}
-void SygusUnifRl::registerConditionalEnumerator(
- Node f,
- Node e,
- Node cond,
- unsigned strategy_index,
- std::map<Node, std::vector<Node>>& strategy_lemmas)
+void SygusUnifRl::registerConditionalEnumerator(Node f,
+ Node e,
+ Node cond,
+ unsigned strategy_index)
{
+ // only allow one decision tree per strategy point
+ if (d_stratpt_to_dt.find(e) != d_stratpt_to_dt.end())
+ {
+ return;
+ }
// we will do unification for this candidate
d_unif_candidates.insert(f);
// add to the list of all conditional enumerators
{
d_cond_enums.push_back(cond);
d_cand_cenums[f].push_back(cond);
- // register the conditional enumerator
- d_tds->registerEnumerator(cond, f, d_parent, true);
d_cenum_to_stratpt[cond].clear();
- // register lemmas to remove redundant operators from condition enumeration
- std::map<const Node, std::vector<Node>>::iterator it =
- strategy_lemmas.find(cond);
- if (it != strategy_lemmas.end())
- {
- for (const Node& lemma : it->second)
- {
- Trace("cegis-unif-enum-debug")
- << "* Registering lemma to remove redundand operators for " << cond
- << " --> " << lemma << "\n";
- d_qe->getOutputChannel().lemma(lemma);
- }
- strategy_lemmas.erase(cond);
- }
}
// register that this strategy node has a decision tree construction
d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index);
d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size());
}
+void SygusUnifRl::DecisionTreeInfo::clearCondValues()
+{
+ // TODO
+ // d_conds.clear();
+}
+
void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv)
{
d_conds.push_back(condv);
~SygusUnifRl();
/** initialize */
- void initialize(QuantifiersEngine* qe,
- const std::vector<Node>& funs,
- std::vector<Node>& enums,
- std::map<Node, std::vector<Node>>& strategy_lemmas) override;
- /** Notify enumeration */
+ void initializeCandidate(
+ QuantifiersEngine* qe,
+ Node f,
+ std::vector<Node>& enums,
+ std::map<Node, std::vector<Node>>& strategy_lemmas) override;
+
+ /** Notify enumeration (unused) */
void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
/** Construct solution */
bool constructSolution(std::vector<Node>& sols) override;
* checked through wehether f has conditional or point enumerators (we use the
* former)
*/
- bool usingUnif(Node f);
+ bool usingUnif(Node f) const;
+ /** get condition for evaluation point
+ *
+ * Returns the strategy point corresponding to the condition of the strategy
+ * point e.
+ */
+ Node getConditionForEvaluationPoint(Node e) const;
+ /** set conditional enumerators
+ *
+ * This informs this class that the current set of conditions for evaluation
+ * point e is conds.
+ */
+ void setConditions(Node e, const std::vector<Node>& conds);
/** retrieve the head of evaluation points for candidate c, if any */
std::vector<Node> getEvalPointHeads(Node c);
unsigned strategy_index);
/** adds the respective evaluation point of the head f */
void addPoint(Node f);
+ /** clears the condition values */
+ void clearCondValues();
/** adds a condition value to the pool of condition values */
void addCondValue(Node condv);
/** returns index of strategy information of strategy node for this DT */
NodePair d_template;
/** enumerated condition values */
std::vector<Node> d_conds;
+ /** get condition enumerator */
+ Node getConditionEnumerator() const { return d_cond_enum; }
private:
/**
/** register strategy
*
* Initialize the above data for the relevant enumerators in the strategy tree
- * of candidate variable f.
- *
- * Lemmas to remove redundant operators from enumerators of specific strategy
- * points, if any, are retrived from strategy_lemmas.
+ * of candidate variable f. For each strategy point e which there is a
+ * decision tree strategy, we add e to enums.
*/
- void registerStrategy(Node f,
- std::map<Node, std::vector<Node>>& strategy_lemmas);
+ void registerStrategy(Node f, std::vector<Node>& enums);
/** register strategy node
*
* Called while traversing the strategy tree of f. The arguments e and nrole
* indicate the current node in the tree we are traversing, and visited
- * indicates the nodes we have already visited.
- *
- * Lemmas to remove redundant operators from enumerators of specific strategy
- * points, if any, are retrived from strategy_lemmas.
+ * indicates the nodes we have already visited. If e has a decision tree
+ * strategy, it is added to enums.
*/
void registerStrategyNode(Node f,
Node e,
NodeRole nrole,
std::map<Node, std::map<NodeRole, bool>>& visited,
- std::map<Node, std::vector<Node>>& strategy_lemmas);
+ std::vector<Node>& enums);
/** register conditional enumerator
*
* Registers that cond is a conditional enumerator for building a (recursive)
* decision tree at strategy node e within the strategy tree of f.
- *
- * Lemmas to remove redundant operators from enumerators of specific strategy
- * points, if any, are retrived from strategy_lemmas.
*/
void registerConditionalEnumerator(
Node f,
Node e,
Node cond,
- unsigned strategy_index,
- std::map<Node, std::vector<Node>>& strategy_lemmas);
+ unsigned strategy_index);
};
} /* CVC4::theory::quantifiers namespace */
projects / cvc5.git / commitdiff