type = "unsigned long"
help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
+[[option]]
+ name = "sygusEnumVarAgnostic"
+ category = "regular"
+ long = "sygus-var-agnostic"
+ type = "bool"
+ default = "false"
+ help = "when possible, use variable-agnostic enumerators"
+
[[option]]
name = "sygusMinGrammar"
category = "regular"
<< "Simple symmetry breaking for " << dt.getName() << ", constructor "
<< dt[tindex].getName() << ", at depth " << depth << std::endl;
- // if we are the "any constant" constructor, we do no symmetry breaking
- // only do simple symmetry breaking up to depth 2
+ // get the sygus operator
Node sop = Node::fromExpr(dt[tindex].getSygusOp());
- if (sop.getAttribute(SygusAnyConstAttribute()) || depth > 2)
- {
- d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = Node::null();
- return Node::null();
- }
+ // get the kind of the constructor operator
+ Kind nk = d_tds->getConsNumKind(tn, tindex);
+ // is this the any-constant constructor?
+ bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute());
+
// conjunctive conclusion of lemma
std::vector<Node> sbp_conj;
+ // the number of (sygus) arguments
+ // Notice if this is an any-constant constructor, its child is not a
+ // sygus child, hence we set to 0 here.
+ unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs();
+
+ // builtin type
+ TypeNode tnb = TypeNode::fromType(dt.getSygusType());
+ // get children
+ std::vector<Node> children;
+ for (unsigned j = 0; j < dt_index_nargs; j++)
+ {
+ Node sel = nm->mkNode(
+ APPLY_SELECTOR_TOTAL,
+ Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)),
+ n);
+ Assert(sel.getType().isDatatype());
+ children.push_back(sel);
+ }
+
if (depth == 0)
{
Trace("sygus-sb-simple-debug") << " Size..." << std::endl;
// fairness
- if (options::sygusFair() == SYGUS_FAIR_DT_SIZE)
+ if (options::sygusFair() == SYGUS_FAIR_DT_SIZE && !isAnyConstant)
{
Node szl = nm->mkNode(DT_SIZE, n);
Node szr =
szr = Rewriter::rewrite(szr);
sbp_conj.push_back(szl.eqNode(szr));
}
- }
-
- // symmetry breaking
- Kind nk = d_tds->getConsNumKind(tn, tindex);
- if (options::sygusSymBreak())
- {
- // the number of (sygus) arguments
- unsigned dt_index_nargs = dt[tindex].getNumArgs();
-
- // builtin type
- TypeNode tnb = TypeNode::fromType(dt.getSygusType());
- // get children
- std::vector<Node> children;
- for (unsigned j = 0; j < dt_index_nargs; j++)
- {
- Node sel = nm->mkNode(
- APPLY_SELECTOR_TOTAL,
- Node::fromExpr(dt[tindex].getSelectorInternal(tn.toType(), j)),
- n);
- Assert(sel.getType().isDatatype());
- children.push_back(sel);
- }
-
- // direct solving for children
- // for instance, we may want to insist that the LHS of MINUS is 0
- Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl;
- std::map<unsigned, unsigned> children_solved;
- for (unsigned j = 0; j < dt_index_nargs; j++)
- {
- int i = d_ssb.solveForArgument(tn, tindex, j);
- if (i >= 0)
- {
- children_solved[j] = i;
- TypeNode ctn = children[j].getType();
- const Datatype& cdt =
- static_cast<DatatypeType>(ctn.toType()).getDatatype();
- Assert(i < static_cast<int>(cdt.getNumConstructors()));
- sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt));
- }
- }
-
- if (isVarAgnostic && depth == 0)
+ if (isVarAgnostic)
{
// Enforce symmetry breaking lemma template for each x_i:
// template z.
sbp_conj.push_back(finish.eqNode(prev));
}
}
+ }
+
+ // if we are the "any constant" constructor, we do no symmetry breaking
+ // only do simple symmetry breaking up to depth 2
+ bool doSymBreak = options::sygusSymBreak();
+ if (isAnyConstant || depth > 2)
+ {
+ doSymBreak = false;
+ }
+ // symmetry breaking
+ if (doSymBreak)
+ {
+ // direct solving for children
+ // for instance, we may want to insist that the LHS of MINUS is 0
+ Trace("sygus-sb-simple-debug") << " Solve children..." << std::endl;
+ std::map<unsigned, unsigned> children_solved;
+ for (unsigned j = 0; j < dt_index_nargs; j++)
+ {
+ int i = d_ssb.solveForArgument(tn, tindex, j);
+ if (i >= 0)
+ {
+ children_solved[j] = i;
+ TypeNode ctn = children[j].getType();
+ const Datatype& cdt =
+ static_cast<DatatypeType>(ctn.toType()).getDatatype();
+ Assert(i < static_cast<int>(cdt.getNumConstructors()));
+ sbp_conj.push_back(DatatypesRewriter::mkTester(children[j], i, cdt));
+ }
+ }
+
// depth 1 symmetry breaking : talks about direct children
if (depth == 1)
{
}
}
-Node SygusSymBreakNew::registerSearchValue(
- Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas)
+Node SygusSymBreakNew::registerSearchValue(Node a,
+ Node n,
+ Node nv,
+ unsigned d,
+ std::vector<Node>& lemmas,
+ bool isVarAgnostic,
+ bool doSym)
{
Assert(n.getType().isComparableTo(nv.getType()));
TypeNode tn = n.getType();
APPLY_SELECTOR_TOTAL,
Node::fromExpr(dt[cindex].getSelectorInternal(tn.toType(), i)),
n);
- Node nvc = registerSearchValue(a, sel, nv[i], d + 1, lemmas);
+ Node nvc = registerSearchValue(a,
+ sel,
+ nv[i],
+ d + 1,
+ lemmas,
+ isVarAgnostic,
+ doSym && (!isVarAgnostic || i == 0));
if (nvc.isNull())
{
return Node::null();
nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children);
}
}
+ if (!doSym)
+ {
+ return nv;
+ }
Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl;
std::map<TypeNode, int> var_count;
Node cnv = d_tds->canonizeBuiltin(nv, var_count);
Node bad_val_o = d_cache[a].d_search_val[tn][bad_val_bvr];
Assert( d_cache[a].d_search_val_sz[tn].find( bad_val_bvr )!=d_cache[a].d_search_val_sz[tn].end() );
unsigned prev_sz = d_cache[a].d_search_val_sz[tn][bad_val_bvr];
- if( prev_sz>sz ){
+ bool doFlip = (prev_sz > sz);
+ if (doFlip)
+ {
//swap : the excluded value is the previous
d_cache[a].d_search_val_sz[tn][bad_val_bvr] = sz;
bad_val = d_cache[a].d_search_val[tn][bad_val_bvr];
bad_val_o = nv;
+ if (Trace.isOn("sygus-sb-exc"))
+ {
+ Trace("sygus-sb-exc") << "Flip : exclude ";
+ quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val);
+ Trace("sygus-sb-exc") << " instead of ";
+ quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val_o);
+ Trace("sygus-sb-exc") << ", since its size is " << sz << " < "
+ << prev_sz << std::endl;
+ }
sz = prev_sz;
}
if( Trace.isOn("sygus-sb-exc") ){
a, bad_val, eset, bad_val_o, var_count, lemmas);
// other generalization criteria go here
- return Node::null();
+
+ // If the exclusion was flipped, we are excluding a previous value
+ // instead of the current one. Hence, the current value is a legal
+ // value that we will consider.
+ if (!doFlip)
+ {
+ return Node::null();
+ }
}
}
}
Trace("dt-sygus") << ss.str() << std::endl;
}
// first check that the value progv for prog is what we expected
+ bool isExc = true;
if (checkValue(prog, progv, 0, lemmas))
{
+ isExc = false;
//debugging : ensure fairness was properly handled
if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog );
Node szlem = NodeManager::currentNM()->mkNode( kind::OR, prog.eqNode( progv ).negate(),
prog_sz.eqNode( progv_sz ) );
Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem << std::endl;
- lemmas.push_back( szlem );
- return;
+ lemmas.push_back(szlem);
+ isExc = true;
}
}
-
- // register the search value ( prog -> progv ), this may invoke symmetry breaking
- if( options::sygusSymBreakDynamic() ){
+
+ // register the search value ( prog -> progv ), this may invoke symmetry
+ // breaking
+ if (!isExc && options::sygusSymBreakDynamic())
+ {
+ bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog);
// check that it is unique up to theory-specific rewriting and
// conjecture-specific symmetry breaking.
- Node rsv = registerSearchValue(prog, prog, progv, 0, lemmas);
- SygusSymBreakExcAttribute ssbea;
- prog.setAttribute(ssbea, rsv.isNull());
+ Node rsv = registerSearchValue(
+ prog, prog, progv, 0, lemmas, isVarAgnostic, true);
if (rsv.isNull())
{
+ isExc = true;
Trace("sygus-sb") << " SygusSymBreakNew::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
}
else
}
}
}
+ SygusSymBreakExcAttribute ssbea;
+ prog.setAttribute(ssbea, isExc);
}
}
//register any measured terms that we haven't encountered yet (should only be invoked on first call to check
registerSizeTerm( mts[i], lemmas );
}
Trace("sygus-sb") << " SygusSymBreakNew::check: finished." << std::endl;
-
- if( Trace.isOn("cegqi-engine") ){
- if (lemmas.empty() && !d_szinfo.empty())
+
+ if (Trace.isOn("cegqi-engine") && !d_szinfo.empty())
+ {
+ if (lemmas.empty())
{
Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
for (std::pair<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>&
}
Trace("cegqi-engine") << std::endl;
}
+ else
+ {
+ Trace("cegqi-engine")
+ << "*** Sygus : produced symmetry breaking lemmas" << std::endl;
+ for (const Node& lem : lemmas)
+ {
+ Trace("cegqi-engine-debug") << " " << lem << std::endl;
+ }
+ }
}
}
* not "some constant". Thus, we should consider the subterm
* C_{any_constant}( 5 ) above to be an unconstrained variable (as represented
* by a selector chain), instead of the concrete value 5.
- */
- Node registerSearchValue(
- Node a, Node n, Node nv, unsigned d, std::vector<Node>& lemmas);
+ *
+ * The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If
+ * this is the case, we restrict symmetry breaking to subterms of n on its
+ * leftmost subchain. For example, consider the grammar:
+ * A -> B=B
+ * B -> B+B | x | y | 0
+ * Say we are registering the search value x = y+x. Notice that this value is
+ * ordered. If a were a variable-agnostic enumerator of type A in this
+ * case, we would only register x = y+x and x, and not y+x or y, since the
+ * latter two terms are not leftmost subterms in this value. If we did on the
+ * other hand register y+x, we would be prevented from solutions like x+y = 0
+ * later, since x+y is equivalent to (the already registered value) y+x.
+ *
+ * If doSym is false, we are not performing symmetry breaking on n. This flag
+ * is set to false on branches of n that are not leftmost.
+ */
+ Node registerSearchValue(Node a,
+ Node n,
+ Node nv,
+ unsigned d,
+ std::vector<Node>& lemmas,
+ bool isVarAgnostic,
+ bool doSym);
/** Register symmetry breaking lemma
*
* This function adds the symmetry breaking lemma template lem for terms of
d_addedLemma = true;
return true;
}else{
+ Trace("dt-lemma-send") << "TheoryDatatypes::doSendLemma : duplicate : "
+ << lem << std::endl;
return false;
}
}
std::vector<Node>& lemmas)
{
Trace("cegis") << "Initialize cegis..." << std::endl;
+ unsigned csize = candidates.size();
+ // We only can use actively-generated enumerators if there is only one
+ // function-to-synthesize. Otherwise, we would have to generate a "product" of
+ // two actively-generated enumerators. That is, given a conjecture with two
+ // functions-to-synthesize with enumerators e_f and e_g, if:
+ // e_f -> t1, ..., tn
+ // e_g -> s1, ..., sm
+ // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj)
+ // for each i,j. We do not do this and revert to the default behavior of
+ // this module instead.
+ bool isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1;
// initialize an enumerator for each candidate
- for (unsigned i = 0; i < candidates.size(); i++)
+ for (unsigned i = 0; i < csize; i++)
{
Trace("cegis") << "...register enumerator " << candidates[i];
bool do_repair_const = false;
}
}
Trace("cegis") << std::endl;
- d_tds->registerEnumerator(
- candidates[i], candidates[i], d_parent, false, do_repair_const);
+ // variable agnostic enumerators require an active guard
+ d_tds->registerEnumerator(candidates[i],
+ candidates[i],
+ d_parent,
+ isVarAgnostic,
+ do_repair_const,
+ isVarAgnostic);
}
return true;
}
}
bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
- const std::vector<Node>& candidate_values)
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& lems)
{
// First, decide if this call will apply "conjecture-specific refinement".
// In other words, in some settings, the following method will identify and
}
if (!cre_lems.empty())
{
- for (const Node& lem : cre_lems)
+ lems.insert(lems.end(), cre_lems.begin(), cre_lems.end());
+ addedEvalLemmas = true;
+ if (Trace.isOn("cegqi-lemma"))
{
- if (d_qe->addLemma(lem))
+ for (const Node& lem : cre_lems)
{
Trace("cegqi-lemma")
<< "Cegqi::Lemma : ref evaluation : " << lem << std::endl;
- addedEvalLemmas = true;
}
}
/* we could, but do not return here. experimentally, it is better to
{
Node lem = nm->mkNode(
OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
- if (d_qe->addLemma(lem))
- {
- Trace("cegqi-lemma")
- << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl;
- addedEvalLemmas = true;
- }
+ lems.push_back(lem);
+ Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem
+ << std::endl;
}
}
return addedEvalLemmas;
}
// evaluate on refinement lemmas
- bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
+ bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems);
// try to construct candidates
if (!processConstructCandidates(enums,
/** evaluates candidate values on current refinement lemmas
*
- * Returns true if refinement lemmas are added after evaluation, false
- * otherwise.
+ * This method performs techniques that ensure that
+ * { candidates -> candidate_values } is a candidate solution that should
+ * be checked by the solution verifier of the CEGIS loop. This method
+ * invokes two sub-methods which may reject the current solution.
+ * The first is "refinement evaluation", described above the method
+ * getRefinementEvalLemmas below. The second is "evaluation unfolding",
+ * which eagerly unfolds applications of evaluation functions (see
+ * sygus_eval_unfold.h for details).
*
- * Also eagerly unfolds evaluation functions in a heuristic manner, which is
- * useful e.g. for boolean connectives
+ * If this method returns true, then { candidates -> candidate_values }
+ * is not ready to be tried as a candidate solution. In this case, it may add
+ * lemmas to lems.
+ *
+ * Notice that this method may return true without adding any lemmas to
+ * lems, in the case that terms from candidates are "actively-generated
+ * enumerators", since the model values of such terms are managed
+ * explicitly within getEnumeratedValue. In this case, the owner of the
+ * actively-generated enumerators (e.g. SynthConjecture) is responsible for
+ * blocking the current value of candidates.
*/
bool addEvalLemmas(const std::vector<Node>& candidates,
- const std::vector<Node>& candidate_values);
+ const std::vector<Node>& candidate_values,
+ std::vector<Node>& lems);
//-----------------------------------end refinement lemmas
/** Get refinement evaluation lemmas
+ *
+ * This method performs "refinement evaluation", that is, it tests
+ * whether the current solution, given by { candidates -> candidate_values },
+ * satisfies all current refinement lemmas. If it does not, it may add
+ * blocking lemmas L to lems which exclude (a generalization of) the current
+ * solution.
*
* Given a candidate solution ms for candidates vs, this function adds lemmas
* to lems based on evaluating the conjecture, instantiated for ms, on lemmas
}
// register the enumerator
si.d_enums[index].push_back(e);
+ bool mkActiveGuard = false;
+ bool isVarAgnostic = false;
+ // if we are using a single independent enumerator for conditions, then we
+ // allocate an active guard, and are eligible to use variable-agnostic
+ // enumeration.
+ if (options::sygusUnifCondIndependent() && index == 1)
+ {
+ mkActiveGuard = true;
+ isVarAgnostic = options::sygusEnumVarAgnostic();
+ }
Trace("cegis-unif-enum") << "* Registering new enumerator " << e
<< " to strategy point " << si.d_pt << "\n";
d_tds->registerEnumerator(
- e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1);
+ e, si.d_pt, d_parent, mkActiveGuard, false, isVarAgnostic);
}
void CegisUnifEnumDecisionStrategy::registerEvalPts(
return new_comb;
}
+void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
+void EnumStreamConcrete::addValue(Node v) { d_ess.resetValue(v); }
+Node EnumStreamConcrete::getNext() { return d_ess.getNext(); }
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
unsigned d_curr_ind;
};
+/**
+ * An enumerated value generator based on the above class. This is
+ * SynthConjecture's interface to using the above utility.
+ */
+class EnumStreamConcrete : public EnumValGenerator
+{
+ public:
+ EnumStreamConcrete(quantifiers::TermDbSygus* tds) : d_ess(tds) {}
+ /** initialize this class with enumerator e */
+ void initialize(Node e) override;
+ /** get that value v was enumerated */
+ void addValue(Node v) override;
+ /** get the next value enumerated by this class */
+ Node getNext() override;
+
+ private:
+ /** stream substitution utility */
+ EnumStreamSubstitution d_ess;
+};
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
return false;
}
}
+ bool isVarAgnostic = options::sygusEnumVarAgnostic();
for (const Node& c : candidates)
{
Assert(d_examples.find(c) != d_examples.end());
for (const Node& e : d_candidate_to_enum[c])
{
TypeNode etn = e.getType();
- d_tds->registerEnumerator(e, c, d_parent, true);
+ d_tds->registerEnumerator(e, c, d_parent, true, false, isVarAgnostic);
Node g = d_tds->getActiveGuardForEnumerator(e);
d_enum_to_active_guard[e] = g;
d_enum_to_candidate[e] = c;
{
Assert(isPbe());
Assert(!e.isNull());
+ if (!d_tds->isPassiveEnumerator(e))
+ {
+ // we cannot apply conjecture-specific symmetry breaking on enumerators that
+ // are not passive
+ return Node::null();
+ }
e = d_tds->getSynthFunForEnumerator(e);
Assert(!e.isNull());
std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/enum_stream_substitution.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
return;
}
}
+ bool checkSuccess = false;
+ do
+ {
+ Trace("cegqi-check-debug") << "doCheckNext..." << std::endl;
+ checkSuccess = doCheckNext(lems);
+ Trace("cegqi-check-debug")
+ << "...finished " << lems.empty() << " " << !needsRefinement() << " "
+ << !d_qe->getTheoryEngine()->needCheck() << " " << checkSuccess
+ << std::endl;
+ } while (lems.empty() && !needsRefinement()
+ && !d_qe->getTheoryEngine()->needCheck() && checkSuccess);
+}
+bool SynthConjecture::doCheckNext(std::vector<Node>& lems)
+{
// get the list of terms that the master strategy is interested in
std::vector<Node> terms;
d_master->getTermList(d_candidates, terms);
Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
}
- if (Trace.isOn("cegqi-check"))
+ if (Trace.isOn("cegqi-engine"))
{
- Trace("cegqi-check") << "CegConjuncture : repair previous solution ";
+ Trace("cegqi-engine") << "CegConjuncture : repair previous solution ";
for (const Node& fc : fail_cvs)
{
std::stringstream ss;
Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc);
- Trace("cegqi-check") << ss.str() << " ";
+ Trace("cegqi-engine") << ss.str() << " ";
}
- Trace("cegqi-check") << std::endl;
+ Trace("cegqi-engine") << std::endl;
}
d_repair_index++;
if (d_sygus_rconst->repairSolution(
}
}
- // get the model value of the relevant terms from the master module
- std::vector<Node> enum_values;
- bool fullModel = getEnumeratedValues(terms, enum_values);
-
- // if the master requires a full model and the model is partial, we fail
- if (!d_master->allowPartialModel() && !fullModel)
- {
- Trace("cegqi-check") << "...partial model, fail." << std::endl;
- return;
- }
-
if (!constructed_cand)
{
+ // get the model value of the relevant terms from the master module
+ std::vector<Node> enum_values;
+ bool fullModel = getEnumeratedValues(terms, enum_values);
+
+ // if the master requires a full model and the model is partial, we fail
+ if (!d_master->allowPartialModel() && !fullModel)
+ {
+ // we retain the values in d_ev_active_gen_waiting
+ Trace("cegqi-engine") << "...partial model, fail." << std::endl;
+ return false;
+ }
+ // the waiting values are passed to the module below, clear
+ d_ev_active_gen_waiting.clear();
+
+ // debug print
+ Assert(terms.size() == enum_values.size());
+ bool emptyModel = true;
+ Trace("cegqi-engine") << " * Value is : ";
+ for (unsigned i = 0, size = terms.size(); i < size; i++)
+ {
+ Node nv = enum_values[i];
+ if (!nv.isNull())
+ {
+ emptyModel = false;
+ }
+ if (Trace.isOn("cegqi-engine"))
+ {
+ Node onv = nv.isNull() ? d_qe->getModel()->getValue(terms[i]) : nv;
+ TypeNode tn = onv.getType();
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
+ Trace("cegqi-engine") << terms[i] << " -> ";
+ if (nv.isNull())
+ {
+ Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
+ }
+ else
+ {
+ Trace("cegqi-engine") << ss.str() << " ";
+ if (Trace.isOn("cegqi-engine-rr"))
+ {
+ Node bv = d_tds->sygusToBuiltin(nv, tn);
+ bv = Rewriter::rewrite(bv);
+ Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+ }
+ }
+ }
+ }
+ Trace("cegqi-engine") << std::endl;
+ if (emptyModel)
+ {
+ Trace("cegqi-engine") << "...empty model, fail." << std::endl;
+ return false;
+ }
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
terms, enum_values, d_candidates, candidate_values, lems);
lem = getStreamGuardedLemma(lem);
lems.push_back(lem);
recordInstantiation(candidate_values);
- return;
+ return true;
}
Assert(!d_set_ce_sk_vars);
}
{
if (!constructed_cand)
{
- return;
+ return true;
}
}
if (lem.isNull())
{
// no lemma to check
- return;
+ return true;
}
lem = Rewriter::rewrite(lem);
Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
Assert(squery.isConst() && squery.getConst<bool>());
#endif
- return;
+ return true;
}
else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
{
// if we were successful, we immediately print the current solution.
// this saves us from introducing a verification lemma and a new guard.
printAndContinueStream();
- return;
+ return true;
}
lem = getStreamGuardedLemma(lem);
lems.push_back(lem);
+ return true;
}
void SynthConjecture::doRefine(std::vector<Node>& lems)
std::vector<Node>& v)
{
bool ret = true;
- Trace("cegqi-engine") << " * Value is : ";
for (unsigned i = 0; i < n.size(); i++)
{
Node nv = getEnumeratedValue(n[i]);
v.push_back(nv);
ret = ret && !nv.isNull();
- if (Trace.isOn("cegqi-engine"))
- {
- Node onv = nv.isNull() ? d_qe->getModel()->getValue(n[i]) : nv;
- TypeNode tn = onv.getType();
- std::stringstream ss;
- Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
- Trace("cegqi-engine") << n[i] << " -> ";
- if (nv.isNull())
- {
- Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
- }
- else
- {
- Trace("cegqi-engine") << ss.str() << " ";
- if (Trace.isOn("cegqi-engine-rr"))
- {
- Node bv = d_tds->sygusToBuiltin(nv, tn);
- bv = Rewriter::rewrite(bv);
- Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
- }
- }
- }
}
- Trace("cegqi-engine") << std::endl;
return ret;
}
// return null.
return Node::null();
}
- if (d_tds->isPassiveEnumerator(e))
+
+ if (!d_tds->isEnumerator(e) || d_tds->isPassiveEnumerator(e))
{
return getModelValue(e);
}
- Assert(false);
// management of actively generated enumerators goes here
- return getModelValue(e);
+
+ // initialize the enumerated value generator for e
+ std::map<Node, std::unique_ptr<EnumValGenerator> >::iterator iteg =
+ d_evg.find(e);
+ if (iteg == d_evg.end())
+ {
+ d_evg[e].reset(new EnumStreamConcrete(d_tds));
+ Trace("sygus-active-gen")
+ << "Active-gen: initialize for " << e << std::endl;
+ d_evg[e]->initialize(e);
+ d_ev_curr_active_gen[e] = Node::null();
+ iteg = d_evg.find(e);
+ Trace("sygus-active-gen-debug") << "...finish" << std::endl;
+ }
+ // if we have a waiting value, return it
+ std::map<Node, Node>::iterator itw = d_ev_active_gen_waiting.find(e);
+ if (itw != d_ev_active_gen_waiting.end())
+ {
+ Trace("sygus-active-gen-debug")
+ << "Active-gen: return waiting " << itw->second << std::endl;
+ return itw->second;
+ }
+ // Check if there is an (abstract) value absE we were actively generating
+ // values based on.
+ Node absE = d_ev_curr_active_gen[e];
+ if (absE.isNull())
+ {
+ // None currently exist. The next abstract value is the model value for e.
+ absE = getModelValue(e);
+ if (Trace.isOn("sygus-active-gen"))
+ {
+ Trace("sygus-active-gen") << "Active-gen: new abstract value : ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", e);
+ Trace("sygus-active-gen") << " -> ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", absE);
+ Trace("sygus-active-gen") << std::endl;
+ }
+ d_ev_curr_active_gen[e] = absE;
+ iteg->second->addValue(absE);
+ }
+ Node v = iteg->second->getNext();
+ if (v.isNull())
+ {
+ // No more concrete values generated from absE.
+ NodeManager* nm = NodeManager::currentNM();
+ d_ev_curr_active_gen[e] = Node::null();
+ // We must block e = absE.
+ std::vector<Node> exp;
+ d_tds->getExplain()->getExplanationForEquality(e, absE, exp);
+ for (unsigned i = 0, size = exp.size(); i < size; i++)
+ {
+ exp[i] = exp[i].negate();
+ }
+ Node g = d_tds->getActiveGuardForEnumerator(e);
+ if (!g.isNull())
+ {
+ if (d_ev_active_gen_first_val.find(e) == d_ev_active_gen_first_val.end())
+ {
+ exp.push_back(g.negate());
+ d_ev_active_gen_first_val[e] = absE;
+ }
+ }
+ else
+ {
+ Assert(false);
+ }
+ Node lem = exp.size() == 1 ? exp[0] : nm->mkNode(OR, exp);
+ Trace("cegqi-lemma") << "Cegqi::Lemma : actively-generated enumerator "
+ "exclude current solution : "
+ << lem << std::endl;
+ if (Trace.isOn("sygus-active-gen-debug"))
+ {
+ Trace("sygus-active-gen-debug") << "Active-gen: block ";
+ TermDbSygus::toStreamSygus("sygus-active-gen-debug", absE);
+ Trace("sygus-active-gen-debug") << std::endl;
+ }
+ d_qe->getOutputChannel().lemma(lem);
+ }
+ else
+ {
+ // We are waiting to send e -> v to the module that requested it.
+ d_ev_active_gen_waiting[e] = v;
+ if (Trace.isOn("sygus-active-gen"))
+ {
+ Trace("sygus-active-gen") << "Active-gen : " << e << " : ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", absE);
+ Trace("sygus-active-gen") << " -> ";
+ TermDbSygus::toStreamSygus("sygus-active-gen", v);
+ Trace("sygus-active-gen") << std::endl;
+ }
+ }
+
+ return v;
}
Node SynthConjecture::getModelValue(Node n)
d_ce_sk_vars.clear();
d_ce_sk_var_mvs.clear();
// However, we need to exclude the current solution using an explicit
- // blocking clause, so that we proceed to the next solution.
+ // blocking clause, so that we proceed to the next solution. We do this only
+ // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator).
std::vector<Node> terms;
d_master->getTermList(d_candidates, terms);
std::vector<Node> exp;
for (const Node& cprog : terms)
{
- Node sol = cprog;
- if (!d_cinfo[cprog].d_inst.empty())
+ Assert(d_tds->isEnumerator(cprog));
+ if (d_tds->isPassiveEnumerator(cprog))
{
- sol = d_cinfo[cprog].d_inst.back();
- // add to explanation of exclusion
- d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp);
+ Node sol = cprog;
+ if (!d_cinfo[cprog].d_inst.empty())
+ {
+ sol = d_cinfo[cprog].d_inst.back();
+ // add to explanation of exclusion
+ d_tds->getExplain()->getExplanationForEquality(cprog, sol, exp);
+ }
}
}
- Assert(!exp.empty());
- Node exc_lem = exp.size() == 1
- ? exp[0]
- : NodeManager::currentNM()->mkNode(kind::AND, exp);
- exc_lem = exc_lem.negate();
- Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
- << exc_lem << std::endl;
- d_qe->getOutputChannel().lemma(exc_lem);
+ if (!exp.empty())
+ {
+ Node exc_lem = exp.size() == 1
+ ? exp[0]
+ : NodeManager::currentNM()->mkNode(kind::AND, exp);
+ exc_lem = exc_lem.negate();
+ Trace("cegqi-lemma") << "Cegqi::Lemma : stream exclude current solution : "
+ << exc_lem << std::endl;
+ d_qe->getOutputChannel().lemma(exc_lem);
+ }
}
void SynthConjecture::printSynthSolution(std::ostream& out,
namespace theory {
namespace quantifiers {
+/**
+ * A base class for generating values for actively-generated enumerators.
+ * At a high level, the job of this class is to accept a stream of "abstract
+ * values" a1, ..., an, ..., and generate a (possibly larger) stream of
+ * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
+ */
+class EnumValGenerator
+{
+ public:
+ virtual ~EnumValGenerator() {}
+ /** initialize this class with enumerator e */
+ virtual void initialize(Node e) = 0;
+ /** Inform this generator that abstract value v was enumerated. */
+ virtual void addValue(Node v) = 0;
+ /** Get the next concrete value generated by this class. */
+ virtual Node getNext() = 0;
+};
+
/** a synthesis conjecture
* This class implements approaches for a synthesis conecjture, given by data
* member d_quant.
void assign(Node q);
/** has a conjecture been assigned to this class */
bool isAssigned() { return !d_embed_quant.isNull(); }
- /**
- * Get model values for terms n, store in vector v. This method returns true
- * if and only if all values added to v are non-null.
- */
- bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v);
- /**
- * Get model value for term n. If n has a value that was excluded by
- * datatypes sygus symmetry breaking, this method returns null.
- */
- Node getEnumeratedValue(Node n);
/**
* Get model value for term n.
*/
SygusModule* d_master;
//------------------------end modules
+ //------------------------enumerators
+ /**
+ * Get model values for terms n, store in vector v. This method returns true
+ * if and only if all values added to v are non-null.
+ */
+ bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v);
+ /**
+ * Get model value for term n. If n has a value that was excluded by
+ * datatypes sygus symmetry breaking, this method returns null.
+ */
+ Node getEnumeratedValue(Node n);
+ /** enumerator generators for each actively-generated enumerator */
+ std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg;
+ /**
+ * Map from enumerators to whether they are currently being
+ * "actively-generated". That is, we are in a state where we have called
+ * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet
+ * returned null. The range of this map stores the abstract value that
+ * we are currently generating values from.
+ */
+ std::map<Node, Node> d_ev_curr_active_gen;
+ /** the current waiting value of each actively-generated enumerator, if any
+ *
+ * This caches values that are actively generated and that we have not yet
+ * passed to a call to SygusModule::constructCandidates. An example of when
+ * this may occur is when there are two actively-generated enumerators e1 and
+ * e2. Say on some iteration we actively-generate v1 for e1, the value
+ * of e2 was excluded by symmetry breaking, and say the current master sygus
+ * module does not handle partial models. Hence, we abort the current check.
+ * We remember that the value of e1 was v1 by storing it here, so that on
+ * a future check when v2 has a proper value, it is returned.
+ */
+ std::map<Node, Node> d_ev_active_gen_waiting;
+ /** the first value enumerated for each actively-generated enumerator
+ *
+ * This is to implement an optimization that only guards the blocking lemma
+ * for the first value of an actively-generated enumerator.
+ */
+ std::map<Node, Node> d_ev_active_gen_first_val;
+ //------------------------end enumerators
+
/** list of constants for quantified formula
* The outer Skolems for the negation of d_embed_quant.
*/
d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]);
}
}
+ /**
+ * This performs the next check of the syntax-guided enumerative check
+ * (see doCheck above). The method returns true if a new solution was
+ * considered.
+ *
+ * Notice that one call to doCheck may correspond to multiple calls to
+ * doCheckNext. For example, if we are using an actively-generated enumerator,
+ * one enumerated (abstract) term may correspond to multiple concrete
+ * terms t1, ..., tn to check, where we make up to n calls to doCheckNext when
+ * each of t1, ..., tn fail to satisfy the current refinement lemmas.
+ */
+ bool doCheckNext(std::vector<Node>& lems);
/** get synth solutions internal
*
* This function constructs the body of solutions for all
d_var_subclass_list[et][sc].push_back(v);
}
}
+ // If no subclass has more than one variable, do not use variable agnostic
+ // enumeration
+ bool useVarAgnostic = false;
+ for (std::pair<const unsigned, std::vector<Node> >& p :
+ d_var_subclass_list[et])
+ {
+ if (p.second.size() > 1)
+ {
+ useVarAgnostic = true;
+ }
+ }
+ if (!useVarAgnostic)
+ {
+ Trace("sygus-db")
+ << "...disabling variable agnostic for " << e
+ << " since it has no subclass with more than one variable."
+ << std::endl;
+ d_enum_var_agnostic[e] = false;
+ }
}
}
projects / cvc5.git / commitdiff