Node lem,
std::vector<Node>& lems)
{
- /* Notify lemma to unification utility and get its purified form */
- Node plem = d_sygus_unif.addRefLemma(lem);
+ // Notify lemma to unification utility and get its purified form
+ std::map<Node, std::vector<Node> > eval_pts;
+ Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
d_refinement_lemmas.push_back(plem);
+ // Notify the enumeration manager if there are new evaluation points
+ for (const std::pair<const Node, std::vector<Node> >& ep : eval_pts)
+ {
+ d_u_enum_manager.registerEvalPts(ep.second, ep.first);
+ }
/* Make the refinement lemma and add it to lems. This lemma is guarded by the
parent's guard, which has the semantics "this conjecture has a solution",
hence this lemma states: if the parent conjecture has a solution, it
d_tds = d_qe->getTermDatabaseSygus();
}
-void CegisUnifEnumManager::initialize(std::vector<Node>& cs)
+void CegisUnifEnumManager::initialize(const std::vector<Node>& cs)
{
if (cs.empty())
{
incrementNumEnumerators();
}
-void CegisUnifEnumManager::registerEvalPts(std::vector<Node>& eis, Node c)
+void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node c)
{
// candidates of the same type are managed
TypeNode ct = c.getType();
/** Cegis Unif Enumeration Manager
*
* This class enforces a decision heuristic that limits the number of
- * unique values given to the set 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, 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 evaluation points of that type
- * are interpreted as a value in a set whose cardinality is at most i".
+ * 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".
*
* To enforce this, we introduce sygus enumerator(s) of the same type as the
- * evaluation points registered to this class and add lemmas that enforce that
- * points are equal to at least one enumerator (see registerEvalPtAtValue).
+ * 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).
*/
class CegisUnifEnumManager
{
* Each candidate c in cs should be such that we are using a
* synthesis-by-unification approach for c.
*/
- void initialize(std::vector<Node>& cs);
+ void initialize(const std::vector<Node>& cs);
/** register evaluation point for candidate
*
- * This notifies this class that eis is a set of evaluation points for
- * candidate c, where c should be a candidate that was passed to initialize
- * in the vector cs.
+ * 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.
*
* This may add new lemmas of the form described above
* registerEvalPtAtValue on the output channel of d_qe.
*/
- void registerEvalPts(std::vector<Node>& eis, Node c);
+ void registerEvalPts(const std::vector<Node>& eis, Node c);
/** get next decision request
*
* This function has the same contract as Theory::getNextDecisionRequest.
std::vector<Node>& lemmas)
{
d_ecache.clear();
- d_cand_to_pt_enum.clear();
+ d_cand_to_eval_hds.clear();
// initialize
std::vector<Node> all_enums;
SygusUnif::initialize(qe, funs, all_enums, lemmas);
for (const Node& c : d_unif_candidates)
{
d_app_to_pt[c].clear();
- d_cand_to_pt_enum[c].clear();
+ d_cand_to_eval_hds[c].clear();
d_purified_count[c] = 0;
}
}
/* Adds new enumerator to map from candidate */
Trace("sygus-unif-rl-purify") << "...new enum " << new_f
<< " for candidate " << nb[0] << "\n";
- d_cand_to_pt_enum[nb[0]].push_back(new_f);
+ d_cand_to_eval_hds[nb[0]].push_back(new_f);
/* Maps new enumerator to its respective tuple of arguments */
d_app_to_pt[new_f] =
std::vector<Node>(children.begin() + 2, children.end());
return nb;
}
-Node SygusUnifRl::addRefLemma(Node lemma)
+Node SygusUnifRl::addRefLemma(Node lemma,
+ std::map<Node, std::vector<Node>>& eval_hds)
{
Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma
<< "\n";
std::vector<Node> model_guards;
BoolNodePairMap cache;
+ // cache previous sizes
+ std::map<Node, unsigned> prev_n_eval_hds;
+ for (const std::pair<const Node, std::vector<Node>>& cp : d_cand_to_eval_hds)
+ {
+ prev_n_eval_hds[cp.first] = cp.second.size();
+ }
+
/* Make the purified lemma which will guide the unification utility. */
Node plem = purifyLemma(lemma, false, model_guards, cache);
if (!model_guards.empty())
}
plem = Rewriter::rewrite(plem);
Trace("sygus-unif-rl-purify") << "Purified lemma : " << plem << "\n";
+
+ Trace("sygus-unif-rl-purify") << "Collect new evaluation points...\n";
+ for (const std::pair<const Node, std::vector<Node>>& cp : d_cand_to_eval_hds)
+ {
+ Node c = cp.first;
+ unsigned prevn = 0;
+ std::map<Node, unsigned>::iterator itp = prev_n_eval_hds.find(c);
+ if (itp != prev_n_eval_hds.end())
+ {
+ prevn = itp->second;
+ }
+ for (unsigned j = prevn, size = cp.second.size(); j < size; j++)
+ {
+ eval_hds[c].push_back(cp.second[j]);
+ }
+ }
+
return plem;
}
void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
/** Construct solution */
bool constructSolution(std::vector<Node>& sols) override;
- Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
/** add refinement lemma
*
- * This adds a lemma to the specification for f.
+ * This adds a lemma to the specification. It returns the purified form
+ * of the lemma based on the method purifyLemma below. The method adds the
+ * head of "evaluation points" to the map eval_hds, where an evaluation point
+ * is a term of the form:
+ * ev( e1, c1...cn )
+ * where ev is an evaluation function for the sygus deep embedding, e1 is of
+ * sygus datatype type (the "head" of the evaluation point), and c1...cn are
+ * constants. If ev( e1, c1...cn ) is the purified form of ev( e, t1...tn ),
+ * then e1 is added to eval_hds[e]. We add evaluation points to eval_hds only
+ * for those terms that are newly generated by this call (and have not been
+ * returned by a previous call to this method).
*/
- Node addRefLemma(Node lemma);
+ Node addRefLemma(Node lemma, std::map<Node, std::vector<Node>>& eval_hds);
/**
* whether f is being synthesized with unification strategies. This can be
* checked through wehether f has conditional or point enumerators (we use the
std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
/**
* This class stores information regarding an enumerator, including: a
- * database
- * of values that have been enumerated for this enumerator.
+ * database of values that have been enumerated for this enumerator.
*/
class EnumCache
{
};
/** maps enumerators to the information above */
std::map<Node, EnumCache> d_ecache;
-
+ /** construct sol */
+ Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
/** collects data from refinement lemmas to drive solution construction
*
* In particular it rebuilds d_app_to_pt whenever d_prev_rlemmas is different
Purification
--------------------------------------------------------------
*/
- /* Maps unif candidates to their point enumerators */
- std::map<Node, std::vector<Node>> d_cand_to_pt_enum;
+ /* Maps unif candidates to heads of their evaluation points */
+ std::map<Node, std::vector<Node>> d_cand_to_eval_hds;
/**
* maps applications of the function-to-synthesize to their tuple of arguments
* (which constitute a "data point") */
projects / cvc5.git / commitdiff