/*! \file cegis_unif.cpp
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa
+ ** Haniel Barbosa, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
std::vector<Node>& lemmas)
{
Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
- /* Init UNIF util */
+ // Init UNIF util
d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas);
Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
std::vector<Node> unif_candidates;
- /* Initialize enumerators for non-unif functions-to-synhesize */
+ // Initialize enumerators for non-unif functions-to-synhesize
for (const Node& c : candidates)
{
if (!d_sygus_unif.usingUnif(c))
Valuation& valuation = d_qe->getValuation();
for (const Node& e : d_cond_enums)
{
- Trace("cegis-unif-debug")
- << "Check conditional enumerator : " << e << std::endl;
+ Trace("cegis-unif-debug") << "Check conditional enumerator : " << e
+ << std::endl;
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 set. If so, then
- there may exist more values for it, and hence we add it to enums. */
+ // Get whether the active guard for this enumerator is set. If so, then
+ // there may exist more values for it, and hence we add it to enums.
Node gstatus = valuation.getSatValue(g);
if (!gstatus.isNull() && gstatus.getConst<bool>())
{
Trace("cegis-unif-enum") << "Register new enumerated values :\n";
for (unsigned i = 0, size = enums.size(); i < size; ++i)
{
- /* Only conditional enumerators will be notified to unif utility */
+ // Only conditional enumerators will be notified to unif utility
if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i])
== d_cond_enums.end())
{
enum_consider.push_back(i);
}
}
- /* only consider the enumerators that are at minimum size (for fairness) */
+ // only consider the enumerators that are at minimum size (for fairness)
Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / "
<< enums.size() << std::endl;
for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i)
Node e = enums[j], v = enum_values[j];
std::vector<Node> enum_lems;
d_sygus_unif.notifyEnumeration(e, v, enum_lems);
- /* the lemmas must be guarded by the active guard of the enumerator */
+ // 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];
for (unsigned j = 0, size = enum_lems.size(); j < size; ++j)
}
lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
}
- /* divide-and-conquer solution bulding for candidates using unif util */
+ // divide-and-conquer solution bulding for candidates using unif util
std::vector<Node> sols;
if (d_sygus_unif.constructSolution(sols))
{
{
d_u_enum_manager.registerEvalPts(ep.second, ep.first);
}
- /* Make the refinement lemma and add it to lems. This lemma is guarded by the
- parent's guard, which has the semantics "this conjecture has a solution",
- hence this lemma states: if the parent conjecture has a solution, it
- satisfies the specification for the given concrete point. */
+ // Make the refinement lemma and add it to lems. This lemma is guarded by the
+ // parent's guard, which has the semantics "this conjecture has a solution",
+ // hence this lemma states: if the parent conjecture has a solution, it
+ // satisfies the specification for the given concrete point.
lems.push_back(NodeManager::currentNM()->mkNode(
OR, d_parent->getGuard().negate(), plem));
}
/*! \file sygus_unif_rl.cpp
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa
+ ** Haniel Barbosa, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
std::vector<Node>& enums,
std::vector<Node>& lemmas)
{
- d_ecache.clear();
- d_cand_to_eval_hds.clear();
// initialize
std::vector<Node> all_enums;
SygusUnif::initialize(qe, funs, all_enums, lemmas);
registerStrategy(f);
}
enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end());
- /* Copy candidates and check whether CegisUnif for any of them */
+ // Copy candidates and check whether CegisUnif for any of them
for (const Node& c : d_unif_candidates)
{
- d_app_to_pt[c].clear();
+ d_hd_to_pt[c].clear();
d_cand_to_eval_hds[c].clear();
- d_purified_count[c] = 0;
+ d_cand_to_hd_count[c] = 0;
}
}
{
Trace("sygus-unif-rl-notify") << "SyGuSUnifRl: Adding to enum " << e
<< " value " << v << "\n";
- d_ecache[e].d_enum_vals.push_back(v);
- /* Exclude v from next enumerations for e */
+ // Exclude v from next enumerations for e
Node exc_lemma =
d_tds->getExplain()->getExplanationForEquality(e, v).negate();
- Trace("sygus-unif-rl-notify")
+ Trace("sygus-unif-rl-notify-debug")
<< "SygusUnifRl : enumeration exclude lemma : " << exc_lemma << std::endl;
lemmas.push_back(exc_lemma);
+ // Update all desicion trees in which this enumerator is a conditional
+ // enumerator, if any
+ std::map<Node, std::vector<Node>>::iterator it = d_cenum_to_stratpt.find(e);
+ if (it == d_cenum_to_stratpt.end())
+ {
+ return;
+ }
+ for (const Node& stratpt : it->second)
+ {
+ Trace("sygus-unif-rl-dt")
+ << "...adding value " << v
+ << " to decision tree of strategy point : " << stratpt << std::endl;
+ Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end());
+ // Register new condition value
+ d_stratpt_to_dt[stratpt].addCondValue(v);
+ Trace("sygus-unif-rl-dt") << "...added\n";
+ }
}
Node SygusUnifRl::purifyLemma(Node n,
Trace("sygus-unif-rl-purify-debug") << "... already visited " << n << "\n";
return it->second;
}
- /* Recurse */
+ // Recurse
unsigned size = n.getNumChildren();
Kind k = n.getKind();
- /* We retrive model value now because purified node may not have a value */
+ // We retrive model value now because purified node may not have a value
Node nv = n;
- /* Whether application of a function-to-synthesize */
+ // Whether application of a function-to-synthesize
bool fapp = k == APPLY_UF && size > 0;
bool u_fapp = false;
bool nu_fapp = false;
{
Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0])
!= d_candidates.end());
- /* Whether application of a (non-)unification function-to-synthesize */
+ // Whether application of a (non-)unification function-to-synthesize
u_fapp = usingUnif(n[0]);
nu_fapp = !usingUnif(n[0]);
- /* get model value of non-top level applications of functions-to-synthesize
- occurring under a unification function-to-synthesize */
+ // get model value of non-top level applications of functions-to-synthesize
+ // occurring under a unification function-to-synthesize
if (ensureConst)
{
nv = d_parent->getModelValue(n);
Assert(n != nv);
- Trace("sygus-unif-rl-purify")
- << "PurifyLemma : model value for " << n << " is " << nv << "\n";
+ Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
+ << " is " << nv << "\n";
}
}
- /* Travese to purify */
+ // Travese to purify
bool childChanged = false;
std::vector<Node> children;
NodeManager* nm = NodeManager::currentNM();
children.push_back(n[i]);
continue;
}
- /* Arguments of non-unif functions do not need to be constant */
+ // Arguments of non-unif functions do not need to be constant
Node child = purifyLemma(
n[i], !nu_fapp && (ensureConst || u_fapp), model_guards, cache);
children.push_back(child);
Node nb;
if (childChanged)
{
- if (n.hasOperator())
+ if (fapp && n.hasOperator())
{
+ Trace("sygus-unif-rl-purify-debug") << "Node " << n
+ << " has operator and fapp is true\n";
children.insert(children.begin(), n.getOperator());
}
+ if (Trace.isOn("sygus-unif-rl-purify-debug"))
+ {
+ Trace("sygus-unif-rl-purify-debug")
+ << "...rebuilding " << n << " with kind " << k << " and children:\n";
+ for (const Node& child : children)
+ {
+ Trace("sygus-unif-rl-purify-debug") << "...... " << child << "\n";
+ }
+ }
nb = NodeManager::currentNM()->mkNode(k, children);
Trace("sygus-unif-rl-purify") << "PurifyLemma : transformed " << n
<< " into " << nb << "\n";
{
nb = n;
}
- /* Map to point enumerator every unification function-to-synthesize */
+ // Map to point enumerator every unification function-to-synthesize
if (u_fapp)
{
Node np;
Assert(nb.hasOperator());
children.insert(children.begin(), n.getOperator());
}
- /* Build purified head with fresh skolem and recreate node */
+ // Build purified head with fresh skolem and recreate node
std::stringstream ss;
- ss << nb[0] << "_" << d_purified_count[nb[0]]++;
+ ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
Node new_f = nm->mkSkolem(ss.str(), nb[0].getType());
- /* Adds new enumerator to map from candidate */
+ // Adds new enumerator to map from candidate
Trace("sygus-unif-rl-purify") << "...new enum " << new_f
- << " for candidate " << nb[0] << "\n";
+ << " for candidate " << nb[0] << "\n";
d_cand_to_eval_hds[nb[0]].push_back(new_f);
- /* Maps new enumerator to its respective tuple of arguments */
- d_app_to_pt[new_f] =
+ // Maps new enumerator to its respective tuple of arguments
+ d_hd_to_pt[new_f] =
std::vector<Node>(children.begin() + 2, children.end());
- if (Trace.isOn("sygus-unif-rl-purify"))
+ if (Trace.isOn("sygus-unif-rl-purify-debug"))
{
- Trace("sygus-unif-rl-purify") << "...[" << new_f << "] --> (";
- for (const Node& pt_i : d_app_to_pt[new_f])
+ Trace("sygus-unif-rl-purify-debug") << "...[" << new_f << "] --> (";
+ for (const Node& pt_i : d_hd_to_pt[new_f])
{
- Trace("sygus-unif-rl-purify") << pt_i << " ";
+ Trace("sygus-unif-rl-purify-debug") << pt_i << " ";
}
- Trace("sygus-unif-rl-purify") << ")\n";
+ Trace("sygus-unif-rl-purify-debug") << ")\n";
}
- /* replace first child and rebulid node */
+ // replace first child and rebulid node
children[1] = new_f;
+ Assert(children.size() > 1);
np = NodeManager::currentNM()->mkNode(k, children);
d_app_to_purified[nb] = np;
}
<< np << "\n";
nb = np;
}
- /* Add equality between purified fapp and model value */
+ // Add equality between purified fapp and model value
if (ensureConst && fapp)
{
model_guards.push_back(
<< model_guards.back() << "\n";
}
nb = Rewriter::rewrite(nb);
- /* every non-top level application of function-to-synthesize must be reduced
- to a concrete constant */
+ // every non-top level application of function-to-synthesize must be reduced
+ // to a concrete constant
Assert(!ensureConst || nb.isConst());
Trace("sygus-unif-rl-purify-debug") << "... caching [" << n << "] = " << nb
<< "\n";
std::map<Node, std::vector<Node>>& eval_hds)
{
Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma
- << "\n";
+ << "\n";
std::vector<Node> model_guards;
BoolNodePairMap cache;
// cache previous sizes
prev_n_eval_hds[cp.first] = cp.second.size();
}
- /* Make the purified lemma which will guide the unification utility. */
+ // Make the purified lemma which will guide the unification utility.
Node plem = purifyLemma(lemma, false, model_guards, cache);
if (!model_guards.empty())
{
for (unsigned j = prevn, size = cp.second.size(); j < size; j++)
{
eval_hds[c].push_back(cp.second[j]);
+ // Add new point to respective decision trees
+ Assert(d_cand_cenums.find(c) != d_cand_cenums.end());
+ for (const Node& cenum : d_cand_cenums[c])
+ {
+ Assert(d_cenum_to_stratpt.find(cenum) != d_cenum_to_stratpt.end());
+ for (const Node& stratpt : d_cenum_to_stratpt[cenum])
+ {
+ Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end());
+ Trace("sygus-unif-rl-dt") << "Add point with head " << cp.second[j]
+ << " to strategy point " << stratpt << "\n";
+ // Register new point from new head
+ d_stratpt_to_dt[stratpt].addPoint(cp.second[j]);
+ }
+ }
}
}
{
return false;
}
- Trace("sygus-unif-rl-sol")
- << "Adding solution " << v << " to unif candidate " << c << "\n";
+ Trace("sygus-unif-rl-sol") << "Adding solution " << v
+ << " to unif candidate " << c << "\n";
sols.push_back(v);
}
}
// is there a decision tree strategy?
if (nrole == role_equal)
{
- std::map<Node, DecisionTreeInfo>::iterator itd = d_enum_to_dt.find(e);
- if (itd != d_enum_to_dt.end())
+ std::map<Node, DecisionTreeInfo>::iterator itd = d_stratpt_to_dt.find(e);
+ if (itd != d_stratpt_to_dt.end())
{
indent("sygus-unif-sol", ind);
- Trace("sygus-unif-sol")
- << "...it has a decision tree strategy." << std::endl;
+ Trace("sygus-unif-sol") << "...it has a decision tree strategy.\n";
+ if (itd->second.isSeparated())
+ {
+ Trace("sygus-unif-sol")
+ << "...... points are separated and I have for root enum the value "
+ << d_parent->getModelValue(e) << "\n";
+ return d_parent->getModelValue(e);
+ }
}
}
{
if (Trace.isOn("sygus-unif-rl-strat"))
{
- Trace("sygus-unif-rl-strat")
- << "Strategy for " << f << " is : " << std::endl;
+ Trace("sygus-unif-rl-strat") << "Strategy for " << f
+ << " is : " << std::endl;
d_strategy[f].debugPrint("sygus-unif-rl-strat");
}
Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
Node e = d_strategy[f].getRootEnumerator();
- std::map<Node, std::map<NodeRole, bool> > visited;
+ std::map<Node, std::map<NodeRole, bool>> visited;
registerStrategyNode(f, e, role_equal, visited);
}
Node f,
Node e,
NodeRole nrole,
- std::map<Node, std::map<NodeRole, bool> >& visited)
+ std::map<Node, std::map<NodeRole, bool>>& visited)
{
Trace("sygus-unif-rl-strat") << " register node " << e << std::endl;
if (visited[e].find(nrole) != visited[e].end())
== d_cond_enums.end())
{
d_cond_enums.push_back(cond);
+ d_cand_cenums[f].push_back(cond);
// register the conditional enumerator
d_tds->registerEnumerator(cond, f, d_parent, true);
+ d_cenum_to_stratpt[cond].clear();
+ }
+ // register that this strategy node has a decision tree construction
+ d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f]);
+ // associate conditional enumerator with strategy node
+ d_cenum_to_stratpt[cond].push_back(e);
+}
+
+void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum,
+ SygusUnifRl* unif,
+ SygusUnifStrategy* strategy)
+{
+ d_cond_enum = cond_enum;
+ d_unif = unif;
+ d_strategy = strategy;
+ // Retrieve template
+ EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum);
+ d_template = NodePair(eiv.d_template, eiv.d_template_arg);
+ // Initialize classifier
+ d_pt_sep.initialize(this);
+}
+
+void SygusUnifRl::DecisionTreeInfo::addPoint(Node f)
+{
+ d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size());
+}
+
+void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv)
+{
+ d_conds.push_back(condv);
+ d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1);
+}
+
+bool SygusUnifRl::DecisionTreeInfo::isSeparated()
+{
+ for (const std::pair<const Node, std::vector<Node>>& rep_to_class :
+ d_pt_sep.d_trie.d_rep_to_class)
+ {
+ Assert(!rep_to_class.second.empty());
+ Node v = rep_to_class.second[0];
+ unsigned i, size = rep_to_class.second.size();
+ for (i = 1; i < size; ++i)
+ {
+ Node vi = d_unif->d_parent->getModelValue(rep_to_class.second[i]);
+ if (v != vi)
+ {
+ Trace("sygus-unif-rl-dt") << "...in sep class heads with diff values: "
+ << rep_to_class.second[0] << " and "
+ << rep_to_class.second[i] << "\n";
+ break;
+ }
+ }
+ // Heads with different model values
+ if (i != size)
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize(
+ DecisionTreeInfo* dt)
+{
+ d_dt = dt;
+}
+
+Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n,
+ unsigned index)
+{
+ Assert(index < d_dt->d_conds.size());
+ // Retrieve respective built_in condition
+ Node cond = d_dt->d_conds[index];
+ TypeNode tn = cond.getType();
+ Node builtin_cond = d_dt->d_unif->d_tds->sygusToBuiltin(cond, tn);
+ // Retrieve evaluation point
+ Assert(d_dt->d_unif->d_hd_to_pt.find(n) != d_dt->d_unif->d_hd_to_pt.end());
+ std::vector<Node> pt = d_dt->d_unif->d_hd_to_pt[n];
+ // compute the result
+ Node res = d_dt->d_unif->d_tds->evaluateBuiltin(tn, builtin_cond, pt);
+ if (Trace.isOn("sygus-unif-rl-sep"))
+ {
+ Trace("sygus-unif-rl-sep") << "...got res = " << res << " from cond "
+ << builtin_cond << " on pt " << n << " ( ";
+ for (const Node& pti : pt)
+ {
+ Trace("sygus-unif-rl-sep") << pti << " ";
+ }
+ Trace("sygus-unif-rl-sep") << ")\n";
+ }
+ // If condition is templated, recompute result accordingly
+ Node templ = d_dt->d_template.first;
+ TNode templ_var = d_dt->d_template.second;
+ if (!templ.isNull())
+ {
+ res = templ.substitute(templ_var, res);
+ res = Rewriter::rewrite(res);
+ Trace("sygus-unif-rl-sep") << "...after template res = " << res
+ << std::endl;
}
- // register that this enumerator has a decision tree construction
- d_enum_to_dt[e].d_cond_enum = cond;
+ Assert(res.isConst());
+ return res;
}
} /* CVC4::theory::quantifiers namespace */
/*! \file sygus_unif_rl.h
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa
+ ** Haniel Barbosa, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
#include <map>
#include "theory/quantifiers/sygus/sygus_unif.h"
+#include "theory/quantifiers/lazy_trie.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
using BoolNodePairMap =
std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
+using NodePair = std::pair<Node, Node>;
class CegConjecture;
CegConjecture* d_parent;
/* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
- /**
- * This class stores information regarding an enumerator, including: a
- * database of values that have been enumerated for this enumerator.
- */
- class EnumCache
- {
- public:
- EnumCache() {}
- ~EnumCache() {}
- /** Values that have been enumerated for this enumerator */
- std::vector<Node> d_enum_vals;
- };
- /** maps enumerators to the information above */
- std::map<Node, EnumCache> d_ecache;
/** construct sol */
Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
/** collects data from refinement lemmas to drive solution construction
Purification
--------------------------------------------------------------
*/
- /* Maps unif candidates to heads of their evaluation points */
+ /**
+ * maps heads of applications of a unif function-to-synthesize to their tuple
+ * of arguments (which constitute a "data point" aka an "evaluation point")
+ */
+ std::map<Node, std::vector<Node>> d_hd_to_pt;
+ /** maps unif candidates to heads of their evaluation points */
std::map<Node, std::vector<Node>> d_cand_to_eval_hds;
/**
- * maps applications of the function-to-synthesize to their tuple of arguments
- * (which constitute a "data point") */
- std::map<Node, std::vector<Node>> d_app_to_pt;
- /** Maps applications of unif functions-to-synthesize to purified symbols*/
+ * maps applications of unif functions-to-synthesize to the result of their
+ * purification */
std::map<Node, Node> d_app_to_purified;
- /** Maps unif functions-to-synthesize to counters of purified symbols */
- std::map<Node, unsigned> d_purified_count;
+ /** maps unif functions-to-synthesize to counters of heads of evaluation
+ * points */
+ std::map<Node, unsigned> d_cand_to_hd_count;
/**
* This is called on the refinement lemma and will rewrite applications of
* functions-to-synthesize to their respective purified form, i.e. such that
*
* When the traversal encounters an application of a unification
* function-to-synthesize it will proceed to ensure that the arguments of that
- * function application are constants (the ensureConst becomes "true"). If an
+ * function application are constants (ensureConst becomes "true"). If an
* applicatin of a non-unif function-to-synthesize is reached, the requirement
- * is lifted (the ensureConst becomes "false"). This avoides introducing
- * spurious equalities in model_guards.
+ * is lifted (ensureConst becomes "false"). This avoides introducing spurious
+ * equalities in model_guards.
*
* For example if "f" is being synthesized with a unification strategy and "g"
* is not then the application
* would be purified into
* g(0) = c1 ^ f1(c1) = c2 => f2(+(0,c2))
*
- * This function also populates the maps for point enumerators
+ * This function also populates the maps between candidates, heads and
+ * evaluation points
*/
Node purifyLemma(Node n,
bool ensureConst,
class DecisionTreeInfo
{
public:
+ DecisionTreeInfo() {}
+ ~DecisionTreeInfo() {}
+ /** initializes this class */
+ void initialize(Node cond_enum,
+ SygusUnifRl* unif,
+ SygusUnifStrategy* strategy);
+ /** adds the respective evaluation point of the head f */
+ void addPoint(Node f);
+ /** adds a condition value to the pool of condition values */
+ void addCondValue(Node condv);
+ /** whether all points that must be separated are separated **/
+ bool isSeparated();
+ /** reference to parent unif util */
+ SygusUnifRl* d_unif;
+ /** enumerator template (if no templates, nodes in pair are Node::null()) */
+ NodePair d_template;
+ /** enumerated condition values */
+ std::vector<Node> d_conds;
+
+ private:
+ /**
+ * reference to infered strategy for the function-to-synthesize this DT is
+ * associated with
+ */
+ SygusUnifStrategy* d_strategy;
/**
* The enumerator in the strategy tree that stores conditions of the
* decision tree.
*/
Node d_cond_enum;
+ /** Classifies evaluation points according to enumerated condition values
+ *
+ * Maintains the invariant that points evaluated in the same way in the
+ * current condition values are kept in the same "separation class."
+ */
+ class PointSeparator : public LazyTrieEvaluator
+ {
+ public:
+ /** initializes this class */
+ void initialize(DecisionTreeInfo* dt);
+ /**
+ * evaluates the respective evaluation point of the head n on the index-th
+ * condition
+ */
+ Node evaluate(Node n, unsigned index) override;
+
+ /** the lazy trie for building the separation classes */
+ LazyTrieMulti d_trie;
+
+ private:
+ /** reference to parent unif util */
+ DecisionTreeInfo* d_dt;
+ };
+ /**
+ * Utility for determining how evaluation points are separated by currently
+ * enumerated condiotion values
+ */
+ PointSeparator d_pt_sep;
};
- /** map from enumerators in the strategy trees to the above data */
- std::map<Node, DecisionTreeInfo> d_enum_to_dt;
+ /** maps strategy points in the strategy tree to the above data */
+ std::map<Node, DecisionTreeInfo> d_stratpt_to_dt;
+ /** maps conditional enumerators to strategy points in which they occur */
+ std::map<Node, std::vector<Node>> d_cenum_to_stratpt;
+ /** maps unif candidates to their conditional enumerators */
+ std::map<Node, std::vector<Node>> d_cand_cenums;
/** all conditional enumerators */
std::vector<Node> d_cond_enums;
/** register strategy
projects / cvc5.git / commitdiff