\n\
";
+const std::string OptionsHandler::s_sygusActiveGenHelp =
+ "\
+Modes for actively-generated sygus enumerators, supported by --sygus-active-gen:\n\
+\n\
+none \n\
++ Do not use actively-generated sygus enumerators.\n\
+\n\
+basic \n\
++ Use basic type enumerator as sygus enumerator.\n\
+\n\
+var-agnostic \n\
++ Use sygus solver to enumerate terms that are agnostic to variables. \n\
+\n\
+";
+
const std::string OptionsHandler::s_macrosQuantHelp = "\
Modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
\n\
}
}
+theory::quantifiers::SygusActiveGenMode
+OptionsHandler::stringToSygusActiveGenMode(std::string option,
+ std::string optarg)
+{
+ if (optarg == "none")
+ {
+ return theory::quantifiers::SYGUS_ACTIVE_GEN_NONE;
+ }
+ else if (optarg == "basic")
+ {
+ return theory::quantifiers::SYGUS_ACTIVE_GEN_BASIC;
+ }
+ else if (optarg == "var-agnostic")
+ {
+ return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
+ }
+ else if (optarg == "help")
+ {
+ puts(s_sygusActiveGenHelp.c_str());
+ exit(1);
+ }
+ else
+ {
+ throw OptionException(std::string("unknown option for --sygus-inv-templ: `")
+ + optarg + "'. Try --sygus-inv-templ help.");
+ }
+}
+
theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
std::string option, std::string optarg)
{
std::string option, std::string optarg);
theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(
std::string option, std::string optarg);
+ theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode(
+ std::string option, std::string optarg);
theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
std::string option, std::string optarg);
theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(
static const std::string s_cegqiSingleInvRconsHelp;
static const std::string s_cegisSampleHelp;
static const std::string s_sygusInvTemplHelp;
+ static const std::string s_sygusActiveGenHelp;
static const std::string s_termDbModeHelp;
static const std::string s_theoryOfModeHelp;
static const std::string s_triggerSelModeHelp;
SYGUS_INV_TEMPL_MODE_POST,
};
+enum SygusActiveGenMode
+{
+ /** do not use actively-generated enumerators */
+ SYGUS_ACTIVE_GEN_NONE,
+ /** use basic actively-generated enumerators */
+ SYGUS_ACTIVE_GEN_BASIC,
+ /** use variable-agnostic enumerators */
+ SYGUS_ACTIVE_GEN_VAR_AGNOSTIC,
+};
+
enum MacrosQuantMode {
/** infer all definitions */
MACROS_QUANT_MODE_ALL,
help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions"
[[option]]
- name = "sygusEnumVarAgnostic"
+ name = "sygusActiveGenMode"
category = "regular"
- long = "sygus-var-agnostic"
- type = "bool"
- default = "false"
- help = "when possible, use variable-agnostic enumerators"
+ long = "sygus-active-gen=MODE"
+ type = "CVC4::theory::quantifiers::SygusActiveGenMode"
+ default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE"
+ handler = "stringToSygusActiveGenMode"
+ includes = ["options/quantifiers_modes.h"]
+ read_only = true
+ help = "mode for actively-generated sygus enumerators"
[[option]]
name = "sygusMinGrammar"
typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
/**
- * Attribute true for enumerators whose current model values have been excluded
- * by sygus symmetry breaking. This is set by the datatypes sygus solver during
- * LAST_CALL effort checks for each active sygus enumerator.
+ * Attribute true for enumerators whose current model values were registered by
+ * the datatypes sygus solver, and were not excluded by sygus symmetry breaking.
+ * This is set by the datatypes sygus solver during LAST_CALL effort checks for
+ * each active sygus enumerator.
*/
-struct SygusSymBreakExcAttributeId
+struct SygusSymBreakOkAttributeId
{
};
-typedef expr::Attribute<SygusSymBreakExcAttributeId, bool>
- SygusSymBreakExcAttribute;
+typedef expr::Attribute<SygusSymBreakOkAttributeId, bool>
+ SygusSymBreakOkAttribute;
namespace datatypes {
}
}
}
- SygusSymBreakExcAttribute ssbea;
- prog.setAttribute(ssbea, isExc);
+ SygusSymBreakOkAttribute ssbo;
+ prog.setAttribute(ssbo, !isExc);
}
}
//register any measured terms that we haven't encountered yet (should only be invoked on first call to check
}
}
-bool CegSingleInv::needsCheck() { return true; }
-
void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; }
bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){
bool rconsSygus = true );
// is single invocation
bool isSingleInvocation() const { return !d_single_inv.isNull(); }
- //needs check
- bool needsCheck();
/** preregister conjecture */
void preregisterConjecture( Node q );
// 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;
+ bool isActiveGen =
+ options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1;
// initialize an enumerator for each candidate
for (unsigned i = 0; i < csize; i++)
{
d_tds->registerEnumerator(candidates[i],
candidates[i],
d_parent,
- isVarAgnostic,
+ isActiveGen,
do_repair_const,
- isVarAgnostic);
+ isActiveGen);
}
return true;
}
// Non-unif candidate are themselves the enumerators
enums.insert(
enums.end(), d_non_unif_candidates.begin(), d_non_unif_candidates.end());
- Valuation& valuation = d_qe->getValuation();
for (const Node& c : d_unif_candidates)
{
// Collect heads of candidates
std::vector<Node> uenums;
// get the current unification enumerators
d_u_enum_manager.getEnumeratorsForStrategyPt(e, uenums, index);
- if (index == 1 && options::sygusUnifCondIndependent())
- {
- Assert(uenums.size() == 1);
- Node eu = uenums[0];
- Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
- // If active guard for this enumerator is not true, there are no more
- // values for it, and hence we ignore it
- Node gstatus = valuation.getSatValue(g);
- if (gstatus.isNull() || !gstatus.getConst<bool>())
- {
- continue;
- }
- }
// get the model value of each enumerator
enums.insert(enums.end(), uenums.begin(), uenums.end());
}
Assert(!itv->second.empty());
if (d_tds->isPassiveEnumerator(eu))
{
- Node g = d_u_enum_manager.getActiveGuardForEnumerator(eu);
+ Node g = d_tds->getActiveGuardForEnumerator(eu);
Node exp_exc = d_tds->getExplain()
->getExplanationForEquality(eu, itv->second[0])
.negate();
{
Node ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
setUpEnumerator(ceu, ci.second, 1);
- d_enum_to_active_guard[ceu] = d_tds->getActiveGuardForEnumerator(ceu);
}
}
}
}
}
-Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e)
-{
- Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
- return d_enum_to_active_guard[e];
-}
-
void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
StrategyPtInfo& si,
unsigned index)
// register the enumerator
si.d_enums[index].push_back(e);
bool mkActiveGuard = false;
- bool isVarAgnostic = false;
+ bool isActiveGen = 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();
+ isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
}
Trace("cegis-unif-enum") << "* Registering new enumerator " << e
<< " to strategy point " << si.d_pt << "\n";
d_tds->registerEnumerator(
- e, si.d_pt, d_parent, mkActiveGuard, false, isVarAgnostic);
+ e, si.d_pt, d_parent, mkActiveGuard, false, isActiveGen);
}
void CegisUnifEnumDecisionStrategy::registerEvalPts(
/** construct candidate
*
* This function takes as input:
- * terms : the terms returned by a call to getTermList,
+ * terms : (a subset of) the terms returned by a call to getTermList,
* term_values : the current model values of terms,
* candidates : the list of candidates.
*
+ * In particular, notice that terms do not include inactive enumerators,
+ * thus if inactive enumerators were added to getTermList, then the terms
+ * list passed to this call will be a (strict) subset of that list.
+ *
* If this function returns true, it adds to candidate_values a list of terms
* of the same length and type as candidates that are candidate solutions
* to the synthesis conjecture in question. This candidate { v } will then be
return false;
}
}
- bool isVarAgnostic = options::sygusEnumVarAgnostic();
+ bool isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
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, false, isVarAgnostic);
- Node g = d_tds->getActiveGuardForEnumerator(e);
- d_enum_to_active_guard[e] = g;
+ d_tds->registerEnumerator(e, c, d_parent, true, false, isActiveGen);
d_enum_to_candidate[e] = c;
TNode te = e;
// initialize static symmetry breaking lemmas for it
void SygusPbe::getTermList(const std::vector<Node>& candidates,
std::vector<Node>& terms)
{
- Valuation& valuation = d_qe->getValuation();
for( unsigned i=0; i<candidates.size(); i++ ){
Node v = candidates[i];
std::map<Node, std::vector<Node> >::iterator it =
d_candidate_to_enum.find(v);
if (it != d_candidate_to_enum.end())
{
- for (unsigned j = 0; j < it->second.size(); j++)
- {
- Node e = it->second[j];
- Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
- Node g = d_enum_to_active_guard[e];
- // Get whether the active guard for this enumerator is true,
- // if so, then there may exist more values for it, and hence we add it
- // to terms.
- Node gstatus = valuation.getSatValue(g);
- if (!gstatus.isNull() && gstatus.getConst<bool>())
- {
- terms.push_back(e);
- }
- }
+ terms.insert(terms.end(), it->second.begin(), it->second.end());
}
}
}
if (!enum_lems.empty())
{
// the lemmas must be guarded by the active guard of the enumerator
- Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
- Node g = d_enum_to_active_guard[e];
+ Node g = d_tds->getActiveGuardForEnumerator(e);
+ Assert(!g.isNull());
for (unsigned j = 0, size = enum_lems.size(); j < size; j++)
{
enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
std::map<Node, std::vector<Node> > d_candidate_to_enum;
/** reverse map of above */
std::map<Node, Node> d_enum_to_candidate;
- /** map from enumerators to active guards */
- std::map<Node, Node> d_enum_to_active_guard;
/** for each candidate variable (function-to-synthesize), input of I/O
* examples */
std::map<Node, std::vector<std::vector<Node> > > d_examples;
d_master(nullptr),
d_set_ce_sk_vars(false),
d_repair_index(0),
- d_refine_count(0)
+ d_refine_count(0),
+ d_guarded_stream_exc(false)
{
if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
{
bool SynthConjecture::needsCheck()
{
- if (isSingleInvocation() && !d_ceg_si->needsCheck())
- {
- return false;
- }
bool value;
Assert(!d_feasible_guard.isNull());
// non or fully single invocation : look at guard only
Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
return false;
}
+ else
+ {
+ Trace("cegqi-engine-debug") << "Feasible guard " << d_feasible_guard
+ << " assigned true." << std::endl;
+ }
}
else
{
}
bool SynthConjecture::needsRefinement() const { return d_set_ce_sk_vars; }
-void SynthConjecture::doCheck(std::vector<Node>& lems)
+bool SynthConjecture::doCheck(std::vector<Node>& lems)
{
Assert(d_master != nullptr);
// we have a new guard, print and continue the stream
printAndContinueStream();
d_current_stream_guard = currGuard;
- return;
+ return true;
}
}
- 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);
{
// we retain the values in d_ev_active_gen_waiting
Trace("cegqi-engine") << "...partial model, fail." << std::endl;
- return false;
+ return true;
}
// the waiting values are passed to the module below, clear
d_ev_active_gen_waiting.clear();
if (emptyModel)
{
Trace("cegqi-engine") << "...empty model, fail." << std::endl;
- return false;
+ return true;
}
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
{
if (!constructed_cand)
{
- return true;
+ return false;
}
}
if (lem.isNull())
{
// no lemma to check
- return true;
+ return false;
}
lem = Rewriter::rewrite(lem);
Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
Assert(squery.isConst() && squery.getConst<bool>());
#endif
- return true;
+ return false;
}
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 true;
+ return false;
}
lem = getStreamGuardedLemma(lem);
lems.push_back(lem);
bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
std::vector<Node>& v)
{
+ std::vector<Node> ncheck = n;
+ n.clear();
bool ret = true;
- for (unsigned i = 0; i < n.size(); i++)
+ for (unsigned i = 0, size = ncheck.size(); i < size; i++)
{
- Node nv = getEnumeratedValue(n[i]);
+ Node e = ncheck[i];
+ // if it is not active, we return null
+ Node g = d_tds->getActiveGuardForEnumerator(e);
+ if (!g.isNull())
+ {
+ Node gstatus = d_qe->getValuation().getSatValue(g);
+ if (gstatus.isNull() || !gstatus.getConst<bool>())
+ {
+ Trace("cegqi-engine-debug")
+ << "Enumerator " << e << " is inactive." << std::endl;
+ continue;
+ }
+ }
+ Node nv = getEnumeratedValue(e);
+ n.push_back(e);
v.push_back(nv);
ret = ret && !nv.isNull();
}
return ret;
}
+/** A basic sygus value generator
+ *
+ * This class is a "naive" term generator for sygus conjectures, which invokes
+ * the type enumerator to generate a stream of (all) sygus terms of a given
+ * type.
+ */
+class EnumValGeneratorBasic : public EnumValGenerator
+{
+ public:
+ EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn) : d_tds(tds), d_te(tn) {}
+ ~EnumValGeneratorBasic() {}
+ /** initialize (do nothing) */
+ void initialize(Node e) override {}
+ /** initialize (do nothing) */
+ void addValue(Node v) override {}
+ /**
+ * Get next returns the next (T-rewriter-unique) value based on the type
+ * enumerator.
+ */
+ Node getNext() override
+ {
+ if (d_te.isFinished())
+ {
+ return Node::null();
+ }
+ Node next = *d_te;
+ ++d_te;
+ Node nextb = d_tds->sygusToBuiltin(next);
+ if (options::sygusSymBreakDynamic())
+ {
+ nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
+ }
+ if (d_cache.find(nextb) == d_cache.end())
+ {
+ d_cache.insert(nextb);
+ return next;
+ }
+ return getNext();
+ }
+
+ private:
+ /** pointer to term database sygus */
+ TermDbSygus* d_tds;
+ /** the type enumerator */
+ TypeEnumerator d_te;
+ /** cache of (enumerated) builtin values we have enumerated so far */
+ std::unordered_set<Node, NodeHashFunction> d_cache;
+};
+
Node SynthConjecture::getEnumeratedValue(Node e)
{
- if (e.getAttribute(SygusSymBreakExcAttribute()))
+ bool isEnum = d_tds->isEnumerator(e);
+
+ if (isEnum && !e.getAttribute(SygusSymBreakOkAttribute()))
{
- // if the current model value of e was excluded by symmetry breaking, then
- // it does not have a proper model value that we should consider, thus we
- // return null.
+ // if the current model value of e was not registered by the datatypes
+ // sygus solver, or was excluded by symmetry breaking, then it does not
+ // have a proper model value that we should consider, thus we return null.
+ Trace("cegqi-engine-debug")
+ << "Enumerator " << e << " does not have proper model value."
+ << std::endl;
return Node::null();
}
- if (!d_tds->isEnumerator(e) || d_tds->isPassiveEnumerator(e))
+ if (!isEnum || d_tds->isPassiveEnumerator(e))
{
return getModelValue(e);
}
+
// management of actively generated enumerators goes here
// initialize the enumerated value generator for e
d_evg.find(e);
if (iteg == d_evg.end())
{
- d_evg[e].reset(new EnumStreamConcrete(d_tds));
+ if (d_tds->isVariableAgnosticEnumerator(e))
+ {
+ d_evg[e].reset(new EnumStreamConcrete(d_tds));
+ }
+ else
+ {
+ d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+ }
Trace("sygus-active-gen")
<< "Active-gen: initialize for " << e << std::endl;
d_evg[e]->initialize(e);
}
if (!exp.empty())
{
+ if (!d_guarded_stream_exc)
+ {
+ d_guarded_stream_exc = true;
+ exp.push_back(d_feasible_guard);
+ }
Node exc_lem = exp.size() == 1
? exp[0]
: NodeManager::currentNM()->mkNode(kind::AND, exp);
*/
void doSingleInvCheck(std::vector<Node>& lems);
/** do syntax-guided enumerative check
+ *
* This is step 2(a) of Figure 3 of Reynolds et al CAV 2015.
+ *
+ * The method returns true if this conjecture is finished trying solutions
+ * for the given call to SynthEngine::check.
+ *
+ * Notice that we make multiple calls to doCheck on one call to
+ * SynthEngine::check. 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 doCheck
+ * when each of t1, ..., tn fails to satisfy the current refinement lemmas.
*/
- void doCheck(std::vector<Node>& lems);
+ bool doCheck(std::vector<Node>& lems);
/** do refinement
* This is step 2(b) of Figure 3 of Reynolds et al CAV 2015.
*/
/**
* Prints the synthesis solution to output stream out. This invokes solution
* reconstruction if the conjecture is single invocation. Otherwise, it
- * returns the enumer
+ * returns the solution found by sygus enumeration.
*/
void printSynthSolution(std::ostream& out);
/** get synth solutions
/**
* 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.
+ *
+ * It removes terms from n that correspond to "inactive" enumerators, that
+ * is, enumerators whose values have been exhausted.
*/
bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v);
/**
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
/**
* Prints the current synthesis solution to the output stream indicated by
* the Options object, send a lemma blocking the current solution to the
- * output channel.
+ * output channel, which we refer to as a "stream exclusion lemma".
*/
void printAndContinueStream();
+ /**
+ * Whether we have guarded a stream exclusion lemma when using sygusStream.
+ * This is an optimization that allows us to guard only the first stream
+ * exclusion lemma.
+ */
+ bool d_guarded_stream_exc;
//-------------------------------- end sygus stream
/** expression miner managers for each function-to-synthesize
*
<< std::endl;
Trace("cegqi-engine-debug") << std::endl;
Valuation& valuation = d_quantEngine->getValuation();
+ std::vector<SynthConjecture*> activeCheckConj;
for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
{
SynthConjecture* sc = d_conjs[i].get();
<< "Current conjecture status : active : " << active << std::endl;
if (active && sc->needsCheck())
{
- checkConjecture(sc);
+ activeCheckConj.push_back(sc);
}
}
+ std::vector<SynthConjecture*> acnext;
+ do
+ {
+ Trace("cegqi-engine-debug") << "Checking " << activeCheckConj.size()
+ << " active conjectures..." << std::endl;
+ for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
+ {
+ SynthConjecture* sc = activeCheckConj[i];
+ if (!checkConjecture(sc))
+ {
+ if (!sc->needsRefinement())
+ {
+ acnext.push_back(sc);
+ }
+ }
+ }
+ activeCheckConj.clear();
+ activeCheckConj = acnext;
+ acnext.clear();
+ } while (!activeCheckConj.empty()
+ && !d_quantEngine->getTheoryEngine()->needCheck());
Trace("cegqi-engine")
<< "Finished Counterexample Guided Instantiation engine." << std::endl;
}
}
}
-void SynthEngine::checkConjecture(SynthConjecture* conj)
+bool SynthEngine::checkConjecture(SynthConjecture* conj)
{
Node q = conj->getEmbeddedConjecture();
Node aq = conj->getConjecture();
<< " ...FAILED to add cbqi instantiation for single invocation!"
<< std::endl;
}
- return;
+ return true;
}
Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl;
std::vector<Node> cclems;
- conj->doCheck(cclems);
+ bool ret = conj->doCheck(cclems);
bool addedLemma = false;
for (const Node& lem : cclems)
{
if (addedLemma)
{
Trace("cegqi-engine") << " ...check for counterexample." << std::endl;
+ return true;
}
else
{
if (conj->needsRefinement())
{
// immediately go to refine candidate
- checkConjecture(conj);
- return;
+ return checkConjecture(conj);
}
}
+ return ret;
}
else
{
Trace("cegqi-engine") << " ...refine candidate." << std::endl;
}
}
+ return true;
}
void SynthEngine::printSynthSolution(std::ostream& out)
* this is the quantifier elimination step option::sygusQePreproc().
*/
void assignConjecture(Node q);
- /** check conjecture */
- void checkConjecture(SynthConjecture* conj);
+ /** check conjecture
+ *
+ * This method returns true if the conjecture is finished processing solutions
+ * for this call to SynthEngine::check().
+ */
+ bool checkConjecture(SynthConjecture* conj);
public:
SynthEngine(QuantifiersEngine* qe, context::Context* c);
Trace("sygus-db") << ", kind = " << sk;
d_kinds[tn][sk] = i;
d_arg_kind[tn][i] = sk;
- }else if( sop.isConst() ){
+ }
+ else if (sop.isConst() && dt[i].getNumArgs() == 0)
+ {
Trace("sygus-db") << ", constant";
d_consts[tn][n] = i;
d_arg_const[tn][i] = n;
SynthConjecture* conj,
bool mkActiveGuard,
bool useSymbolicCons,
- bool isVarAgnostic)
+ bool isActiveGen)
{
if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
{
}
Trace("sygus-db") << " ...finished" << std::endl;
+ d_enum_active_gen[e] = isActiveGen;
+ bool isVarAgnostic =
+ isActiveGen
+ && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
d_enum_var_agnostic[e] = isVarAgnostic;
if (isVarAgnostic)
{
bool TermDbSygus::isPassiveEnumerator(Node e) const
{
- if (isVariableAgnosticEnumerator(e))
+ std::map<Node, bool>::const_iterator itus = d_enum_active_gen.find(e);
+ if (itus != d_enum_active_gen.end())
{
- return false;
+ return !itus->second;
}
- // other criteria go here
return true;
}
* (see d_enum_to_active_guard),
* useSymbolicCons : whether we want model values for e to include symbolic
* constructors like the "any constant" variable.
- * isVarAgnostic : if this flag is true, the enumerator will only generate
- * values whose variables are in canonical order (for example, only x1-x2
+ * isActiveGen : if this flag is true, the enumerator will be
+ * actively-generated based on the mode specified by --sygus-active-gen.
+ * For example, if --sygus-active-gen=var-agnostic, then the enumerator will
+ * only generate values whose variables are in canonical order (only x1-x2
* and not x2-x1 will be generated, assuming x1 and x2 are in the same
* "subclass", see getSubclassForVar).
*
SynthConjecture* conj,
bool mkActiveGuard = false,
bool useSymbolicCons = false,
- bool isVarAgnostic = false);
+ bool isActiveGen = false);
/** is e an enumerator registered with this class? */
bool isEnumerator(Node e) const;
/** return the conjecture e is associated with */
std::map<Node, TypeNode> d_sb_lemma_to_type;
/** mapping from symmetry breaking lemmas to size */
std::map<Node, unsigned> d_sb_lemma_to_size;
+ /** enumerators to whether they are actively-generated */
+ std::map<Node, bool> d_enum_active_gen;
/** enumerators to whether they are variable agnostic */
std::map<Node, bool> d_enum_var_agnostic;
//------------------------------end enumerators
; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.")
; EXIT: 1
-; COMMAND-LINE: --sygus-stream --sygus-abort-size=0
+; COMMAND-LINE: --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic
(set-logic LIA)
projects / cvc5.git / commitdiff