var-agnostic \n\
+ Use sygus solver to enumerate terms that are agnostic to variables. \n\
\n\
+auto (default) \n\
++ Internally decide the best policy for each enumerator. \n\
+\n\
";
const std::string OptionsHandler::s_macrosQuantHelp = "\
{
return theory::quantifiers::SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
}
+ else if (optarg == "auto")
+ {
+ return theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO;
+ }
else if (optarg == "help")
{
puts(s_sygusActiveGenHelp.c_str());
SYGUS_ACTIVE_GEN_ENUM,
/** use variable-agnostic enumerators */
SYGUS_ACTIVE_GEN_VAR_AGNOSTIC,
+ /** internally decide the best policy for each enumerator */
+ SYGUS_ACTIVE_GEN_AUTO,
};
enum MacrosQuantMode {
category = "regular"
long = "sygus-active-gen=MODE"
type = "CVC4::theory::quantifiers::SygusActiveGenMode"
- default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_NONE"
+ default = "CVC4::theory::quantifiers::SYGUS_ACTIVE_GEN_AUTO"
handler = "stringToSygusActiveGenMode"
includes = ["options/quantifiers_modes.h"]
read_only = true
category = "regular"
long = "sygus-pbe-multi-fair"
type = "bool"
- default = "true"
+ default = "false"
help = "when using multiple enumerators, ensure that we only register value of minimial term size"
[[option]]
{
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 isActiveGen =
- options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE && csize == 1;
+ // The role of enumerators is to be either the single solution or part of
+ // a solution involving multiple enumerators.
+ EnumeratorRole erole =
+ csize == 1 ? ROLE_ENUM_SINGLE_SOLUTION : ROLE_ENUM_MULTI_SOLUTION;
// initialize an enumerator for each candidate
for (unsigned i = 0; i < csize; i++)
{
}
}
Trace("cegis") << std::endl;
- // variable agnostic enumerators require an active guard
- d_tds->registerEnumerator(candidates[i],
- candidates[i],
- d_parent,
- isActiveGen,
- do_repair_const,
- isActiveGen);
+ d_tds->registerEnumerator(
+ candidates[i], candidates[i], d_parent, erole, do_repair_const);
}
return true;
}
std::map<Node, Node> pt_to_cond;
// strategy lemmas for each strategy point
std::map<Node, std::vector<Node>> strategy_lemmas;
- // Initialize strategies for all functions-to-synhesize
+ // Initialize strategies for all functions-to-synthesize
+ // The role of non-unification enumerators is to be either the single solution
+ // or part of a solution involving multiple enumerators.
+ EnumeratorRole eroleNonUnif = candidates.size() == 1
+ ? ROLE_ENUM_SINGLE_SOLUTION
+ : ROLE_ENUM_MULTI_SOLUTION;
for (const Node& f : candidates)
{
// Init UNIF util for this candidate
if (!d_sygus_unif.usingUnif(f))
{
Trace("cegis-unif") << "* non-unification candidate : " << f << std::endl;
- d_tds->registerEnumerator(f, f, d_parent);
+ d_tds->registerEnumerator(f, f, d_parent, eroleNonUnif);
d_non_unif_candidates.push_back(f);
}
else
exclude_cons,
term_irrelevant);
d_virtual_enum = nm->mkSkolem("_ve", vtn);
- d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
+ d_tds->registerEnumerator(
+ d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED);
}
// if new_size is a power of two, then isPow2 returns log2(new_size)+1
// otherwise, this returns 0. In the case it returns 0, we don't care
}
// register the enumerator
si.d_enums[index].push_back(e);
- bool mkActiveGuard = false;
- bool isActiveGen = false;
+ EnumeratorRole erole = ROLE_ENUM_CONSTRAINED;
// 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;
- isActiveGen = options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE;
+ erole = ROLE_ENUM_POOL;
}
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, isActiveGen);
+ d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, false);
}
void CegisUnifEnumDecisionStrategy::registerEvalPts(
return false;
}
}
- 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, isActiveGen);
+ d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false);
d_enum_to_candidate[e] = c;
TNode te = e;
// initialize static symmetry breaking lemmas for it
*/
bool increment() override
{
+ ++d_te;
if (d_te.isFinished())
{
d_currTerm = Node::null();
return false;
}
d_currTerm = *d_te;
- ++d_te;
if (options::sygusSymBreakDynamic())
{
Node nextb = d_tds->sygusToBuiltin(d_currTerm);
else
{
// Actively-generated enumerators are currently either variable agnostic
- // or basic.
+ // or basic. The auto mode always prefers the optimized enumerator over
+ // the basic one.
Assert(d_tds->isBasicEnumerator(e));
- if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM)
+ if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC)
{
- d_evg[e].reset(new SygusEnumerator(d_tds, this));
+ d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
}
else
{
- d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+ Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM
+ || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO);
+ d_evg[e].reset(new SygusEnumerator(d_tds, this));
}
}
Trace("sygus-active-gen")
}
}
+std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
+{
+ switch (r)
+ {
+ case ROLE_ENUM_POOL: os << "POOL"; break;
+ case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break;
+ case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break;
+ case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break;
+ default: os << "enum_" << static_cast<unsigned>(r); break;
+ }
+ return os;
+}
+
TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
: d_quantEngine(qe),
d_syexp(new SygusExplain(this)),
void TermDbSygus::registerEnumerator(Node e,
Node f,
SynthConjecture* conj,
- bool mkActiveGuard,
- bool useSymbolicCons,
- bool isActiveGen)
+ EnumeratorRole erole,
+ bool useSymbolicCons)
{
if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
{
d_enum_to_conjecture[e] = conj;
d_enum_to_synth_fun[e] = f;
NodeManager* nm = NodeManager::currentNM();
- if( mkActiveGuard ){
- // make the guard
- Node ag = nm->mkSkolem("eG", nm->booleanType());
- // must ensure it is a literal immediately here
- ag = d_quantEngine->getValuation().ensureLiteral(ag);
- d_enum_to_active_guard[e] = ag;
- }
Trace("sygus-db") << " registering symmetry breaking clauses..."
<< std::endl;
}
Trace("sygus-db") << " ...finished" << std::endl;
+ // determine if we are actively-generated
+ bool isActiveGen = false;
+ if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE)
+ {
+ if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
+ {
+ // If the enumerator is a solution for a conjecture with multiple
+ // functions, we do not use active generation. If we did, 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, and if these enumerators generated:
+ // e_f -> t1, ..., tn
+ // e_g -> s1, ..., sm
+ // The sygus module in charge of this conjecture would expect
+ // constructCandidates calls of the form
+ // (e_f,e_g) -> (ti, sj)
+ // for each i,j. We instead use passive enumeration in this case.
+ //
+ // If the enumerator is constrained, it cannot be actively generated.
+ }
+ else if (erole == ROLE_ENUM_POOL)
+ {
+ // If the enumerator is used for generating a pool of values, we always
+ // use active generation.
+ isActiveGen = true;
+ }
+ else if (erole == ROLE_ENUM_SINGLE_SOLUTION)
+ {
+ // If the enumerator is the single function-to-synthesize, if auto is
+ // enabled, we infer whether it is better to enable active generation.
+ if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO)
+ {
+ // We use active generation if the grammar of the enumerator does not
+ // have ITE and is not Boolean. Experimentally, it is better to
+ // use passive generation for these cases since it enables useful
+ // search space pruning techniques, e.g. evaluation unfolding,
+ // conjecture-specific symmetry breaking. Also, if sygus-stream is
+ // enabled, we always use active generation, since the use cases of
+ // sygus stream are to find many solutions to an easy problem, where
+ // the bottleneck often becomes the large number of "exclude the current
+ // solution" clauses.
+ const Datatype& dt = et.getDatatype();
+ if (options::sygusStream()
+ || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean()))
+ {
+ isActiveGen = true;
+ }
+ }
+ else
+ {
+ isActiveGen = true;
+ }
+ }
+ else
+ {
+ Unreachable("Unknown enumerator mode in registerEnumerator");
+ }
+ }
+ Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole
+ << " returned " << isActiveGen << std::endl;
// Currently, actively-generated enumerators are either basic or variable
// agnostic.
bool isVarAgnostic =
}
d_enum_active_gen[e] = isActiveGen;
d_enum_basic[e] = isActiveGen && !isVarAgnostic;
+
+ // We make an active guard if we will be explicitly blocking solutions for
+ // the enumerator. This is the case if the role of the enumerator is to
+ // populate a pool of terms, or (some cases) of when it is actively generated.
+ if (isActiveGen || erole == ROLE_ENUM_POOL)
+ {
+ // make the guard
+ Node ag = nm->mkSkolem("eG", nm->booleanType());
+ // must ensure it is a literal immediately here
+ ag = d_quantEngine->getValuation().ensureLiteral(ag);
+ d_enum_to_active_guard[e] = ag;
+ }
}
bool TermDbSygus::isEnumerator(Node e) const
void assignIds(std::map<Node, unsigned>& assign, unsigned& idCount);
};
+/** role for registering an enumerator */
+enum EnumeratorRole
+{
+ /** The enumerator populates a pool of terms (e.g. for PBE). */
+ ROLE_ENUM_POOL,
+ /** The enumerator is the single solution of the problem. */
+ ROLE_ENUM_SINGLE_SOLUTION,
+ /**
+ * The enumerator is part of the solution of the problem (e.g. multiple
+ * functions to synthesize).
+ */
+ ROLE_ENUM_MULTI_SOLUTION,
+ /** The enumerator must satisfy some set of constraints */
+ ROLE_ENUM_CONSTRAINED,
+};
+std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
+
// TODO :issue #1235 split and document this class
class TermDbSygus {
public:
//------------------------------enumerators
/**
* Register a variable e that we will do enumerative search on.
+ *
* conj : the conjecture that the enumeration of e is for.
- * f : the synth-fun that the enumeration of e is for.
- * mkActiveGuard : whether we want to make an active guard for e
- * (see d_enum_to_active_guard),
- * useSymbolicCons : whether we want model values for e to include symbolic
- * constructors like the "any constant" variable.
- * isActiveGen : if this flag is true, the enumerator will be
- * actively-generated based on the mode specified by --sygus-active-gen.
+ *
+ * f : the synth-fun that the enumeration of e is for.Notice that enumerator
+ * e may not be one-to-one with f in synthesis-through-unification approaches
+ * (e.g. decision tree construction for PBE synthesis).
+ *
+ * erole : the role of this enumerator (see definition of EnumeratorRole).
+ * Depending on this and the policy for actively-generated enumerators
+ * (--sygus-active-gen), the enumerator may be "actively-generated".
* 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).
*
- * Notice that enumerator e may not be one-to-one with f in
- * synthesis-through-unification approaches (e.g. decision tree construction
- * for PBE synthesis).
+ * useSymbolicCons : whether we want model values for e to include symbolic
+ * constructors like the "any constant" variable.
+ *
+ * An "active guard" may be allocated by this method for e based on erole
+ * and the policies for active generation.
*/
void registerEnumerator(Node e,
Node f,
SynthConjecture* conj,
- bool mkActiveGuard = false,
- bool useSymbolicCons = false,
- bool isActiveGen = false);
+ EnumeratorRole erole,
+ bool useSymbolicCons = false);
/** is e an enumerator registered with this class? */
bool isEnumerator(Node e) const;
/** return the conjecture e is associated with */
projects / cvc5.git / commitdiff