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<Node>& 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<Node>& eis, Node c)
+{
+ // candidates of the same type are managed
+ TypeNode ct = c.getType();
+ std::map<TypeNode, TypeInfo>::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<const unsigned, Node>& 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<unsigned, Node>::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<const TypeNode, TypeInfo>& 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<const TypeNode, TypeInfo>& 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<unsigned, Node>::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<TypeNode, TypeInfo>::iterator itc = d_ce_info.find(ct);
+ Assert(itc != d_ce_info.end());
+ Assert(itc->second.d_enums.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]));
+ }
+ Node lem = NodeManager::currentNM()->mkNode(OR, disj);
+ d_qe->getOutputChannel().lemma(lem);
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
}; /* 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<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 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);
+ /** 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<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 */
+ std::vector<Node> d_eval_points;
+ };
+ /** map types to the above info */
+ std::map<TypeNode, TypeInfo> d_ce_info;
+ /** literals of the form G_uq_n for each n */
+ std::map<unsigned, Node> d_guq_lit;
+ /**
+ * The minimal n such that G_uq_n is not asserted negatively in the
+ * current SAT context.
+ */
+ context::CDO<unsigned> 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
projects / cvc5.git / commitdiff