From 74ea6e8cb76028f4698f295fb6f6b1746df34f08 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 4 May 2018 16:54:40 -0500 Subject: [PATCH] Cegis unif register evaluation points (#1878) --- src/theory/quantifiers/sygus/cegis_unif.cpp | 14 +++++--- src/theory/quantifiers/sygus/cegis_unif.h | 23 ++++++------- .../quantifiers/sygus/sygus_unif_rl.cpp | 33 ++++++++++++++++--- src/theory/quantifiers/sygus/sygus_unif_rl.h | 25 +++++++++----- 4 files changed, 68 insertions(+), 27 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index cc477fa62..8fa4af99c 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -171,9 +171,15 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, Node lem, std::vector& 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 > 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 >& 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 @@ -197,7 +203,7 @@ CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe, d_tds = d_qe->getTermDatabaseSygus(); } -void CegisUnifEnumManager::initialize(std::vector& cs) +void CegisUnifEnumManager::initialize(const std::vector& cs) { if (cs.empty()) { @@ -214,7 +220,7 @@ void CegisUnifEnumManager::initialize(std::vector& cs) incrementNumEnumerators(); } -void CegisUnifEnumManager::registerEvalPts(std::vector& eis, Node c) +void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node c) { // candidates of the same type are managed TypeNode ct = c.getType(); diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 2b1f1584a..93ab69668 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -29,16 +29,17 @@ namespace quantifiers { /** 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 { @@ -53,17 +54,17 @@ 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& cs); + void initialize(const std::vector& 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& eis, Node c); + void registerEvalPts(const std::vector& eis, Node c); /** get next decision request * * This function has the same contract as Theory::getNextDecisionRequest. diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 2cf751927..2f0460c64 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -31,7 +31,7 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe, std::vector& lemmas) { d_ecache.clear(); - d_cand_to_pt_enum.clear(); + d_cand_to_eval_hds.clear(); // initialize std::vector all_enums; SygusUnif::initialize(qe, funs, all_enums, lemmas); @@ -46,7 +46,7 @@ void SygusUnifRl::initialize(QuantifiersEngine* qe, 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; } } @@ -153,7 +153,7 @@ Node SygusUnifRl::purifyLemma(Node n, /* 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(children.begin() + 2, children.end()); @@ -199,12 +199,20 @@ Node SygusUnifRl::purifyLemma(Node n, return nb; } -Node SygusUnifRl::addRefLemma(Node lemma) +Node SygusUnifRl::addRefLemma(Node lemma, + std::map>& eval_hds) { Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma << "\n"; std::vector model_guards; BoolNodePairMap cache; + // cache previous sizes + std::map prev_n_eval_hds; + for (const std::pair>& 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()) @@ -214,6 +222,23 @@ Node SygusUnifRl::addRefLemma(Node lemma) } 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>& cp : d_cand_to_eval_hds) + { + Node c = cp.first; + unsigned prevn = 0; + std::map::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; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index b8ead4986..29c67aa81 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -55,12 +55,21 @@ class SygusUnifRl : public SygusUnif void notifyEnumeration(Node e, Node v, std::vector& lemmas) override; /** Construct solution */ bool constructSolution(std::vector& 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>& 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 @@ -75,8 +84,7 @@ class SygusUnifRl : public SygusUnif std::unordered_set 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 { @@ -88,7 +96,8 @@ class SygusUnifRl : public SygusUnif }; /** maps enumerators to the information above */ std::map 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 @@ -102,8 +111,8 @@ class SygusUnifRl : public SygusUnif Purification -------------------------------------------------------------- */ - /* Maps unif candidates to their point enumerators */ - std::map> d_cand_to_pt_enum; + /* Maps unif candidates to heads of their evaluation points */ + std::map> d_cand_to_eval_hds; /** * maps applications of the function-to-synthesize to their tuple of arguments * (which constitute a "data point") */ -- 2.30.2