From d3f4ac852146c41341e485d9035f3631993e3fa5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 May 2018 17:30:25 -0500 Subject: [PATCH] Cegis unif enumerator manager (#1837) --- src/theory/quantifiers/sygus/cegis_unif.cpp | 132 ++++++++++++++++++++ src/theory/quantifiers/sygus/cegis_unif.h | 100 +++++++++++++++ 2 files changed, 232 insertions(+) diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 256955bbd..cbd9358e0 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -235,6 +235,138 @@ void CegisUnif::registerRefinementLemma(const std::vector& vars, NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem)); } +CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe, + CegConjecture* parent) + : d_qe(qe), d_parent(parent), d_curr_guq_val(qe->getSatContext(), 0) +{ + d_tds = d_qe->getTermDatabaseSygus(); +} + +void CegisUnifEnumManager::initialize(std::vector& cs) +{ + for (const Node& c : cs) + { + // 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); + } + // initialize the current literal + incrementNumEnumerators(); +} + +void CegisUnifEnumManager::registerEvalPts(std::vector& eis, Node c) +{ + // candidates of the same type are managed + TypeNode ct = c.getType(); + std::map::iterator it = d_ce_info.find(ct); + 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& p : d_guq_lit) + { + for (const Node& ei : eis) + { + Assert(ei.getType() == ct); + registerEvalPtAtSize(ct, ei, p.second, p.first); + } + } +} + +Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority) +{ + Node lit = getCurrentLiteral(); + bool value; + if (!d_qe->getValuation().hasSatValue(lit, value)) + { + priority = 0; + return lit; + } + else if (!value) + { + // propagated false, increment + incrementNumEnumerators(); + return getNextDecisionRequest(priority); + } + return Node::null(); +} + +void CegisUnifEnumManager::incrementNumEnumerators() +{ + unsigned new_size = d_curr_guq_val.get() + 1; + d_curr_guq_val.set(new_size); + // ensure that the literal has been allocated + std::map::iterator itc = d_guq_lit.find(new_size); + if (itc == d_guq_lit.end()) + { + // allocate the new literal + NodeManager* nm = NodeManager::currentNM(); + Node new_lit = Rewriter::rewrite(nm->mkSkolem("G_cost", nm->booleanType())); + new_lit = d_qe->getValuation().ensureLiteral(new_lit); + AlwaysAssert(!new_lit.isNull()); + d_qe->getOutputChannel().requirePhase(new_lit, true); + d_guq_lit[new_size] = new_lit; + // allocate an enumerator for each candidate + for (std::pair& ci : d_ce_info) + { + TypeNode ct = ci.first; + Node eu = nm->mkSkolem("eu", ct); + if (!ci.second.d_enums.empty()) + { + 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); + d_qe->getOutputChannel().lemma(sym_break); + } + 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& ci : d_ce_info) + { + TypeNode ct = ci.first; + for (const Node& ei : ci.second.d_eval_points) + { + registerEvalPtAtSize(ct, ei, new_lit, new_size); + } + } + } +} + +Node CegisUnifEnumManager::getCurrentLiteral() const +{ + return getLiteral(d_curr_guq_val.get()); +} + +Node CegisUnifEnumManager::getLiteral(unsigned n) const +{ + std::map::const_iterator itc = d_guq_lit.find(n); + Assert(itc != d_guq_lit.end()); + return itc->second; +} + +void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct, + Node ei, + Node guq_lit, + unsigned n) +{ + // must be equal to one of the first n enums + std::map::iterator itc = d_ce_info.find(ct); + Assert(itc != d_ce_info.end()); + Assert(itc->second.d_enums.size() >= n); + std::vector disj; + disj.push_back(guq_lit.negate()); + for (unsigned i = 0; i < n; i++) + { + disj.push_back(ei.eqNode(itc->second.d_enums[i])); + } + Node lem = NodeManager::currentNM()->mkNode(OR, disj); + d_qe->getOutputChannel().lemma(lem); +} + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 78586cd9c..3100d7d0d 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -152,6 +152,106 @@ class CegisUnif : public SygusModule }; /* class CegisUnif */ +/** 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. + * + * 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". + * + * 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). + */ +class CegisUnifEnumManager +{ + public: + CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent); + /** 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. + * + * Each candidate c in cs should be such that we are using a + * synthesis-by-unification approach for c. + */ + void initialize(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 may add new lemmas of the form described above + * registerEvalPtAtValue on the output channel of d_qe. + */ + void registerEvalPts(std::vector& eis, Node c); + /** get next decision request + * + * This function has the same contract as Theory::getNextDecisionRequest. + * + * If no guard G_uq_* is asserted positively, then this method returns the + * minimal G_uq_i that is not asserted negatively. It allocates this guard + * if necessary. + * + * This call may add new lemmas of the form described above + * registerEvalPtAtValue on the output channel of d_qe. + */ + Node getNextDecisionRequest(unsigned& priority); + + private: + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; + /** sygus term database of d_qe */ + TermDbSygus* d_tds; + /** reference to the parent conjecture */ + CegConjecture* d_parent; + /** null node */ + Node d_null; + /** information per initialized type */ + class TypeInfo + { + public: + TypeInfo() {} + /** candidates for this type */ + std::vector d_candidates; + /** the set of enumerators we have allocated for this candidate */ + std::vector d_enums; + /** the set of evaluation points of this type */ + std::vector d_eval_points; + }; + /** map types to the above info */ + std::map d_ce_info; + /** literals of the form G_uq_n for each n */ + std::map d_guq_lit; + /** + * The minimal n such that G_uq_n is not asserted negatively in the + * current SAT context. + */ + context::CDO d_curr_guq_val; + /** increment the number of enumerators */ + void incrementNumEnumerators(); + /** + * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n + * is not asserted negatively in the current SAT context. + */ + Node getCurrentLiteral() const; + /** get literal G_uq_n */ + Node getLiteral(unsigned n) const; + /** register evaluation point at size + * + * 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. + */ + void registerEvalPtAtSize(TypeNode ct, Node ei, Node guq_lit, unsigned n); +}; + } // namespace quantifiers } // namespace theory } // namespace CVC4 -- 2.30.2