\n\
";
+const std::string OptionsHandler::s_sygusUnifPiHelp =
+ "\
+Modes for piecewise-independent unification supported by --sygus-unif-pi:\n\
+\n\
+none \n\
++ Do not use piecewise-independent unification.\n\
+\n\
+complete \n\
++ Use complete approach for piecewise-independent unification (see Section 3\n\
+of Barbosa et al FMCAD 2019).\n\
+\n\
+cond-enum \n\
++ Use unconstrained condition enumeration for piecewise-independent\n\
+unification (see Section 4 of Barbosa et al FMCAD 2019).\n\
+\n\
+cond-enum-igain \n\
++ Same as cond-enum, but additionally uses an information gain heuristic\n\
+when doing decision tree learning.\n\
+\n\
+";
+
const std::string OptionsHandler::s_sygusGrammarConsHelp =
"\
Modes for default SyGuS grammars, supported by --sygus-grammar-cons:\n\
}
}
+theory::quantifiers::SygusUnifPiMode OptionsHandler::stringToSygusUnifPiMode(
+ std::string option, std::string optarg)
+{
+ if (optarg == "none")
+ {
+ return theory::quantifiers::SYGUS_UNIF_PI_NONE;
+ }
+ else if (optarg == "complete")
+ {
+ return theory::quantifiers::SYGUS_UNIF_PI_COMPLETE;
+ }
+ else if (optarg == "cond-enum")
+ {
+ return theory::quantifiers::SYGUS_UNIF_PI_CENUM;
+ }
+ else if (optarg == "cond-enum-igain")
+ {
+ return theory::quantifiers::SYGUS_UNIF_PI_CENUM_IGAIN;
+ }
+ else if (optarg == "help")
+ {
+ puts(s_sygusUnifPiHelp.c_str());
+ exit(1);
+ }
+ else
+ {
+ throw OptionException(std::string("unknown option for --sygus-unif-pi: `")
+ + optarg + "'. Try --sygus-unif-pi help.");
+ }
+}
+
theory::quantifiers::MacrosQuantMode OptionsHandler::stringToMacrosQuantMode(
std::string option, std::string optarg)
{
std::string option, std::string optarg);
theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode(
std::string option, std::string optarg);
+ theory::quantifiers::SygusUnifPiMode stringToSygusUnifPiMode(
+ std::string option, std::string optarg);
theory::quantifiers::SygusGrammarConsMode stringToSygusGrammarConsMode(
std::string option, std::string optarg);
theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(
static const std::string s_sygusFilterSolHelp;
static const std::string s_sygusInvTemplHelp;
static const std::string s_sygusActiveGenHelp;
+ static const std::string s_sygusUnifPiHelp;
static const std::string s_sygusGrammarConsHelp;
static const std::string s_termDbModeHelp;
static const std::string s_theoryOfModeHelp;
QUANT_REP_MODE_DEPTH,
};
+/**
+ * Modes for piecewise-independent unification for synthesis (see Barbosa et al
+ * FMCAD 2019).
+ */
+enum SygusUnifPiMode
+{
+ /** do not do piecewise-independent unification for synthesis */
+ SYGUS_UNIF_PI_NONE,
+ /** use (finite-model) complete piecewise-independent unification */
+ SYGUS_UNIF_PI_COMPLETE,
+ /** use approach based on condition enumeration for piecewise-independent
+ unification */
+ SYGUS_UNIF_PI_CENUM,
+ /** use approach based on condition enumeration with information gain
+ heuristics for piecewise-independent unification */
+ SYGUS_UNIF_PI_CENUM_IGAIN,
+};
+
}/* CVC4::theory::quantifiers namespace */
}/* CVC4::theory namespace */
help = "abort if constant repair techniques are not applicable"
[[option]]
- name = "sygusUnif"
+ name = "sygusUnifPi"
category = "regular"
- long = "sygus-unif"
- type = "bool"
- default = "false"
- help = "Unification-based function synthesis"
-
-[[option]]
- name = "sygusUnifCondIndependent"
- category = "regular"
- long = "sygus-unif-cond-independent"
- type = "bool"
- default = "false"
- help = "Synthesize conditions indepedently from return values (may generate bigger solutions)"
+ long = "sygus-unif-pi=MODE"
+ type = "CVC4::theory::quantifiers::SygusUnifPiMode"
+ default = "CVC4::theory::quantifiers::SYGUS_UNIF_PI_NONE"
+ handler = "stringToSygusUnifPiMode"
+ includes = ["options/quantifiers_modes.h"]
+ read_only = true
+ help = "mode for synthesis via piecewise-indepedent unification"
[[option]]
name = "sygusUnifShuffleCond"
default = "false"
help = "Shuffle condition pool when building solutions (may change solutions sizes)"
-[[option]]
- name = "sygusUnifBooleanHeuristicDt"
- category = "regular"
- long = "sygus-unif-boolean-heuristic-dt"
- type = "bool"
- default = "false"
- help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)"
-
[[option]]
name = "sygusUnifCondIndNoRepeatSol"
category = "regular"
options::cbqi.set(true);
}
}
- // setting unif requirements
- if (options::sygusUnifBooleanHeuristicDt()
- && !options::sygusUnifCondIndependent())
- {
- options::sygusUnifCondIndependent.set(true);
- }
- if (options::sygusUnifCondIndependent() && !options::sygusUnif())
- {
- options::sygusUnif.set(true);
- }
}
if (options::sygusInference())
{
// set enums for condition enumerators
if (index == 1)
{
- if (options::sygusUnifCondIndependent())
+ if (usingConditionPool())
{
Assert(es.size() == 1);
// whether valueus exhausted
return !addedUnifEnumSymBreakLemma;
}
+bool CegisUnif::usingConditionPool() const
+{
+ return d_sygus_unif.usingConditionPool();
+}
+
void CegisUnif::setConditions(
const std::map<Node, std::vector<Node>>& unif_cenums,
const std::map<Node, std::vector<Node>>& unif_cvalues,
// d_sygus_unif.setConditions(e, cost_lit, unif_cenums[e],
// unif_cvalues[e]); if condition enumerator had value and it is being
// passively generated, exclude this value
- if (options::sygusUnifCondIndependent() && !itc->second.empty())
+ if (usingConditionPool() && !itc->second.empty())
{
Node eu = itc->second[0];
Assert(d_tds->isEnumerator(eu));
// if condition values are being indepedently enumerated, they should be
// communicated to the decision tree strategies indepedently of we
// proceeding to attempt solution building
- if (options::sygusUnifCondIndependent())
+ if (usingConditionPool())
{
setConditions(unif_cenums, unif_cvalues, lems);
}
}
// TODO tie this to the lemma for getting a new condition value
- Assert(options::sygusUnifCondIndependent() || !lemmas.empty());
+ Assert(usingConditionPool() || !lemmas.empty());
for (const Node& lem : lemmas)
{
Trace("cegis-unif-lemma")
{
d_initialized = false;
d_tds = d_qe->getTermDatabaseSygus();
+ SygusUnifPiMode mode = options::sygusUnifPi();
+ d_useCondPool =
+ mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
}
Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
TypeNode ct = c.getType();
Node eu = nm->mkSkolem("eu", ct);
Node ceu;
- if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
+ if (!d_useCondPool && !ci.second.d_enums[0].empty())
{
// make a new conditional enumerator as well, starting the
// second type around
DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
// create single condition enumerator for each decision tree strategy
- if (options::sygusUnifCondIndependent())
+ if (d_useCondPool)
{
// allocate a condition enumerator for each candidate
for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
if (index == 1)
{
// we always use (cost-1) conditions, or 1 if in the indepedent case
- num_enums = !options::sygusUnifCondIndependent() ? num_enums - 1 : 1;
+ num_enums = !d_useCondPool ? num_enums - 1 : 1;
}
if (num_enums > 0)
{
// 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)
+ if (d_useCondPool && index == 1)
{
erole = ROLE_ENUM_POOL;
}
TermDbSygus* d_tds;
/** reference to the parent conjecture */
SynthConjecture* d_parent;
+ /**
+ * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+ * FMCAD 2019). This is determined by option::sygusUnifPi().
+ */
+ bool d_useCondPool;
/** whether this module has been initialized */
bool d_initialized;
/** null node */
std::map<Node, std::vector<Node>>& unif_cenums,
std::map<Node, std::vector<Node>>& unif_cvalues,
std::vector<Node>& lems);
+
+ /**
+ * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+ * FMCAD 2019). This is determined by option::sygusUnifPi().
+ */
+ bool usingConditionPool() const;
/**
* Sygus unif utility. This class implements the core algorithm (e.g. decision
* tree learning) that this module relies upon.
// TODO #1935 ITEs are added to Boolean grammars so that we can infer
// unification strategies. We can do away with this if we can infer
// unification strategies from and/or/not
- if (k == ITE && !options::sygusUnif())
+ if (k == ITE && options::sygusUnifPi() == SYGUS_UNIF_PI_NONE)
{
continue;
}
namespace theory {
namespace quantifiers {
-SygusUnifRl::SygusUnifRl(SynthConjecture* p) : d_parent(p) {}
+SygusUnifRl::SygusUnifRl(SynthConjecture* p)
+ : d_parent(p), d_useCondPool(false), d_useCondPoolIGain(false)
+{
+}
SygusUnifRl::~SygusUnifRl() {}
void SygusUnifRl::initializeCandidate(
QuantifiersEngine* qe,
d_cand_to_eval_hds[f].clear();
d_cand_to_hd_count[f] = 0;
}
+ // check whether we are using condition enumeration
+ SygusUnifPiMode mode = options::sygusUnifPi();
+ d_useCondPool =
+ mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
+ d_useCondPoolIGain = mode == SYGUS_UNIF_PI_CENUM_IGAIN;
}
void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
}
EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
Node sol = itd->second.buildSol(etis->d_cons, lemmas);
- Assert(options::sygusUnifCondIndependent() || !sol.isNull()
- || !lemmas.empty());
+ Assert(d_useCondPool || !sol.isNull() || !lemmas.empty());
return sol;
}
return it->second;
}
+bool SygusUnifRl::usingConditionPool() const { return d_useCondPool; }
+bool SygusUnifRl::usingConditionPoolInfoGain() const
+{
+ return d_useCondPoolIGain;
+}
void SygusUnifRl::registerStrategy(
Node f,
std::vector<Node>& enums,
d_enums.insert(d_enums.end(), enums.begin(), enums.end());
d_conds.insert(d_conds.end(), conds.begin(), conds.end());
// add to condition pool
- if (options::sygusUnifCondIndependent())
+ if (d_unif->usingConditionPool())
{
d_cond_mvs.insert(conds.begin(), conds.end());
if (Trace.isOn("sygus-unif-cond-pool"))
<< " conditions..." << std::endl;
// reset the trie
d_pt_sep.d_trie.clear();
- return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas)
- : buildSolMinCond(cons, lemmas);
+ return d_unif->usingConditionPool() ? buildSolAllCond(cons, lemmas)
+ : buildSolMinCond(cons, lemmas);
}
Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
std::map<Node, Node>& hd_mv)
{
// rebuild decision tree using heuristic learning
- if (options::sygusUnifBooleanHeuristicDt())
+ if (d_unif->usingConditionPoolInfoGain())
{
recomputeSolHeuristically(hd_mv);
}
/** retrieve the head of evaluation points for candidate c, if any */
std::vector<Node> getEvalPointHeads(Node c);
+ /**
+ * Whether we are using condition pool enumeration (Section 4 of Barbosa et al
+ * FMCAD 2019). This is determined by option::sygusUnifPi().
+ */
+ bool usingConditionPool() const;
+ /** Whether we are additionally using information gain. */
+ bool usingConditionPoolInfoGain() const;
+
protected:
/** reference to the parent conjecture */
SynthConjecture* d_parent;
+ /** Whether we are using condition pool enumeration */
+ bool d_useCondPool;
+ /** Whether we are additionally using information gain heuristics */
+ bool d_useCondPoolIGain;
/* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
/** construct sol */
{
d_modules.push_back(d_ceg_pbe.get());
}
- if (options::sygusUnif())
+ if (options::sygusUnifPi() != SYGUS_UNIF_PI_NONE)
{
d_modules.push_back(d_ceg_cegisUnif.get());
}
; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
-; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)
(define-fun g ((x Int)) Int (ite (= x 1) 15 19))
(define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z)))))))
-; COMMAND-LINE: --sygus-unif --sygus-infer
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-infer
; EXPECT: sat
(set-logic UFLIA)
(set-info :status sat)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-unif --sygus-unif-cond-independent --sygus-unif-boolean-heuristic-dt --decision=justification
+; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-bool-ite-return-const --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status
(set-logic LIA)
(define-fun
; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-unif
+; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete
(set-logic SAT)
(synth-fun u ((x Int)) Int)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)
(define-fun get-y ((currPoint Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif --sygus-out=status
+; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
(set-logic BV)
(synth-fun f ((x (BitVec 64)) (y (BitVec 64))) (BitVec 64)
projects / cvc5.git / commitdiff