if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) {
priority = 0;
return feasible_guard;
- }else{
- if( value ){
- // the conjecture is feasible
- if( options::sygusStream() ){
- Assert( !isSingleInvocation() );
- // if we are in sygus streaming mode, then get the "next guard"
- // which denotes "we have not yet generated the next solution to the conjecture"
- Node curr_stream_guard = getCurrentStreamGuard();
- bool needs_new_stream_guard = false;
- if( curr_stream_guard.isNull() ){
- needs_new_stream_guard = true;
- }else{
- // check the polarity of the guard
- if( !d_qe->getValuation().hasSatValue( curr_stream_guard, value ) ) {
- priority = 0;
- return curr_stream_guard;
- }else{
- if( !value ){
- Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl;
- // need to make the next stream guard
- needs_new_stream_guard = true;
- // the guard has propagated false, indicating that a verify
- // lemma was unsatisfiable. Hence, the previous candidate is
- // an actual solution. We print and continue the stream.
- printAndContinueStream();
- }
- }
- }
- if( needs_new_stream_guard ){
- // generate a new stream guard
- curr_stream_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G_Stream", NodeManager::currentNM()->booleanType() ) );
- curr_stream_guard = d_qe->getValuation().ensureLiteral( curr_stream_guard );
- AlwaysAssert( !curr_stream_guard.isNull() );
- d_qe->getOutputChannel().requirePhase( curr_stream_guard, true );
- d_stream_guards.push_back( curr_stream_guard );
- Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : " << curr_stream_guard << std::endl;
- // return it as a decision
- priority = 0;
- return curr_stream_guard;
- }
- }
+ }
+ if (!value)
+ {
+ Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible."
+ << std::endl;
+ return Node::null();
+ }
+ // the conjecture is feasible
+ if (options::sygusStream())
+ {
+ Assert(!isSingleInvocation());
+ // if we are in sygus streaming mode, then get the "next guard"
+ // which denotes "we have not yet generated the next solution to the
+ // conjecture"
+ Node curr_stream_guard = getCurrentStreamGuard();
+ bool needs_new_stream_guard = false;
+ if (curr_stream_guard.isNull())
+ {
+ needs_new_stream_guard = true;
}else{
- Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible." << std::endl;
- }
+ // check the polarity of the guard
+ if (!d_qe->getValuation().hasSatValue(curr_stream_guard, value))
+ {
+ priority = 0;
+ return curr_stream_guard;
+ }
+ if (!value)
+ {
+ Trace("cegqi-debug") << "getNextDecision : we have a new solution "
+ "since stream guard was propagated false: "
+ << curr_stream_guard << std::endl;
+ // need to make the next stream guard
+ needs_new_stream_guard = true;
+ // the guard has propagated false, indicating that a verify
+ // lemma was unsatisfiable. Hence, the previous candidate is
+ // an actual solution. We print and continue the stream.
+ printAndContinueStream();
+ }
+ }
+ if (needs_new_stream_guard)
+ {
+ // generate a new stream guard
+ curr_stream_guard = Rewriter::rewrite(NodeManager::currentNM()->mkSkolem(
+ "G_Stream", NodeManager::currentNM()->booleanType()));
+ curr_stream_guard = d_qe->getValuation().ensureLiteral(curr_stream_guard);
+ AlwaysAssert(!curr_stream_guard.isNull());
+ d_qe->getOutputChannel().requirePhase(curr_stream_guard, true);
+ d_stream_guards.push_back(curr_stream_guard);
+ Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : "
+ << curr_stream_guard << std::endl;
+ // return it as a decision
+ priority = 0;
+ return curr_stream_guard;
+ }
}
+ // see if the master module has a decision
+ if (!isSingleInvocation())
+ {
+ Assert(d_master != nullptr);
+ Node mlit = d_master->getNextDecisionRequest(priority);
+ if (!mlit.isNull())
+ {
+ Trace("cegqi-debug") << "getNextDecision : master module returned : "
+ << mlit << std::endl;
+ return mlit;
+ }
+ }
+
return Node::null();
}
namespace quantifiers {
CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
- : Cegis(qe, p), d_sygus_unif(p)
+ : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
{
d_tds = d_qe->getTermDatabaseSygus();
}
Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
/* Init UNIF util */
d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas);
- /* TODO initialize unif enumerators */
Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
+ std::vector<Node> unif_candidates;
/* Initialize enumerators for non-unif functions-to-synhesize */
for (const Node& c : candidates)
{
if (!d_sygus_unif.usingUnif(c))
{
+ Trace("cegis-unif") << "* non-unification candidate : " << c << std::endl;
d_tds->registerEnumerator(c, c, d_parent);
}
+ else
+ {
+ Trace("cegis-unif") << "* unification candidate : " << c << std::endl;
+ unif_candidates.push_back(c);
+ }
}
+ // initialize the enumeration manager
+ d_u_enum_manager.initialize(unif_candidates);
return true;
}
OR, d_parent->getGuard().negate(), plem));
}
+Node CegisUnif::getNextDecisionRequest(unsigned& priority)
+{
+ return d_u_enum_manager.getNextDecisionRequest(priority);
+}
+
CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
CegConjecture* parent)
- : d_qe(qe), d_parent(parent), d_curr_guq_val(qe->getSatContext(), 0)
+ : d_qe(qe),
+ d_parent(parent),
+ d_ret_dec(qe->getSatContext(), false),
+ d_curr_guq_val(qe->getSatContext(), 0)
{
d_tds = d_qe->getTermDatabaseSygus();
}
void CegisUnifEnumManager::initialize(std::vector<Node>& cs)
{
+ if (cs.empty())
+ {
+ return;
+ }
for (const Node& c : cs)
{
// currently, we allocate the same enumerators for candidates of the same
Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
{
+ // have we returned our decision in the current SAT context?
+ if (d_ret_dec.get())
+ {
+ return Node::null();
+ }
+ // only call this after initialization
+ if (d_ce_info.empty())
+ {
+ // if no enumerators, the decision is null
+ d_ret_dec = true;
+ return Node::null();
+ }
Node lit = getCurrentLiteral();
bool value;
if (!d_qe->getValuation().hasSatValue(lit, value))
{
+ d_ret_dec = true;
priority = 0;
return lit;
}
namespace theory {
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.
+ *
+ * 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;
+ /** Have we returned a decision in the current SAT context? */
+ context::CDO<bool> d_ret_dec;
+ /**
+ * 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);
+};
+
/** Synthesizes functions in a data-driven SyGuS approach
*
* Data is derived from refinement lemmas generated through the regular CEGIS
void registerRefinementLemma(const std::vector<Node>& vars,
Node lem,
std::vector<Node>& lems) override;
+ /** get next decision request */
+ Node getNextDecisionRequest(unsigned& priority) override;
private:
/** sygus term database of d_qe */
* tree learning) that this module relies upon.
*/
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
Node d_null;
}; /* 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