return Node::null();
}
-using IndTriePair = std::pair<unsigned, LazyTrie*>;
-
void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal)
{
Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1
bool forceKeep);
};
+using IndTriePair = std::pair<unsigned, LazyTrie*>;
+
/** Lazy trie with multiple elements per leaf
*
* As the above trie, but allows multiple elements per leaf. This is done by
* containing only itself.
*/
Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
- private:
/** A regular lazy trie */
LazyTrie d_trie;
};
{
for (const Node& c : candidates)
{
+ // Non-unif candidate are themselves the enumerators
if (!d_sygus_unif.usingUnif(c))
{
enums.push_back(c);
continue;
}
- Valuation& valuation = d_qe->getValuation();
- for (const Node& e : d_cond_enums)
+ // Collect heads of candidate
+ for (const Node& hd : d_sygus_unif.getEvalPointHeads(c))
{
- 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.
- Node gstatus = valuation.getSatValue(g);
- if (!gstatus.isNull() && gstatus.getConst<bool>())
- {
- enums.push_back(e);
- }
+ Trace("cegis-unif-enum-debug") << "......cand " << c << " with enum hd "
+ << hd << "\n";
+ enums.push_back(hd);
+ }
+ }
+ // Collect condition enumerators
+ Valuation& valuation = d_qe->getValuation();
+ for (const Node& e : d_cond_enums)
+ {
+ 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.
+ Node gstatus = valuation.getSatValue(g);
+ if (!gstatus.isNull() && gstatus.getConst<bool>())
+ {
+ enums.push_back(e);
}
}
}
std::vector<Node>& candidate_values,
std::vector<Node>& lems)
{
- if (addEvalLemmas(enums, enum_values))
- {
- Trace("cegis-unif-lemma") << "Added eval lemmas\n";
- return false;
- }
- unsigned min_term_size = 0;
- std::vector<unsigned> enum_consider;
NodeManager* nm = NodeManager::currentNM();
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
- if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i])
- == d_cond_enums.end())
+ // Non-unif enums (which are the very candidates) should not be notified
+ if (enums[i] == candidates[i] && !d_sygus_unif.usingUnif(enums[i]))
{
+ Trace("cegis-unif-enum") << " Ignoring non-unif candidate " << enums[i]
+ << std::endl;
continue;
}
if (Trace.isOn("cegis-unif-enum"))
->toStreamSygus(ss, enum_values[i]);
Trace("cegis-unif-enum") << ss.str() << std::endl;
}
- unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
- if (i == 0 || sz < min_term_size)
- {
- enum_consider.clear();
- min_term_size = sz;
- enum_consider.push_back(i);
- }
- else if (sz == min_term_size)
- {
- enum_consider.push_back(i);
- }
- }
- // 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)
- {
- unsigned j = enum_consider[i];
- Node e = enums[j], v = enum_values[j];
+ Node e = enums[i], v = enum_values[i];
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
- Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
- Node g = d_enum_to_active_guard[e];
+ // introduce lemmas to exclude this value of a condition enumerator from
+ // future consideration
+ std::map<Node, Node>::iterator it = d_enum_to_active_guard.find(e);
+ if (it == d_enum_to_active_guard.end())
+ {
+ continue;
+ }
for (unsigned j = 0, size = enum_lems.size(); j < size; ++j)
{
- enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
+ enum_lems[j] = nm->mkNode(OR, it->second.negate(), enum_lems[j]);
}
lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
}
- // divide-and-conquer solution bulding for candidates using unif util
+ // evaluate on refinement lemmas
+ if (addEvalLemmas(enums, enum_values))
+ {
+ Trace("cegis-unif-lemma") << "Added eval lemmas\n";
+ return false;
+ }
+ // build solutions (for unif candidates a divide-and-conquer approach is used)
std::vector<Node> sols;
if (d_sygus_unif.constructSolution(sols))
{
candidate_values.insert(candidate_values.end(), sols.begin(), sols.end());
+ if (Trace.isOn("cegis-unif"))
+ {
+ Trace("cegis-unif") << "* Candidate solutions are:\n";
+ for (const Node& sol : sols)
+ {
+ Trace("cegis-unif")
+ << "... " << d_tds->sygusToBuiltin(sol, sol.getType()) << "\n";
+ }
+ Trace("cegis-unif") << "---CegisUnif Engine---\n";
+ }
return true;
}
return false;
std::map<Node, std::vector<Node> > eval_pts;
Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
d_refinement_lemmas.push_back(plem);
+ Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n";
// Notify the enumeration manager if there are new evaluation points
for (const std::pair<const Node, std::vector<Node> >& ep : eval_pts)
{
d_ret_dec(qe->getSatContext(), false),
d_curr_guq_val(qe->getSatContext(), 0)
{
+ d_initialized = false;
d_tds = d_qe->getTermDatabaseSygus();
}
void CegisUnifEnumManager::initialize(const std::vector<Node>& cs)
{
+ Assert(!d_initialized);
+ d_initialized = true;
if (cs.empty())
{
return;
for (const Node& ei : eis)
{
Assert(ei.getType() == ct);
+ Trace("cegis-unif-enum") << "...for cand " << c << " adding hd " << ei
+ << " at size " << p.first << "\n";
registerEvalPtAtSize(ct, ei, p.second, p.first);
}
}
Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
{
- // have we returned our decision in the current SAT context?
- if (d_ret_dec.get())
+ // are we not initialized or have we returned our decision in the current SAT
+ // context?
+ if (!d_initialized || d_ret_dec.get())
{
return Node::null();
}
- // only call this after initialization
if (d_ce_info.empty())
{
// if no enumerators, the decision is null
bool value;
if (!d_qe->getValuation().hasSatValue(lit, value))
{
- d_ret_dec = true;
priority = 0;
return lit;
}
incrementNumEnumerators();
return getNextDecisionRequest(priority);
}
+ d_ret_dec = true;
return Node::null();
}
TypeNode ct = ci.first;
for (const Node& ei : ci.second.d_eval_points)
{
+ Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
+ << " to new size " << new_size << "\n";
registerEvalPtAtSize(ct, ei, new_lit, new_size);
}
}
disj.push_back(ei.eqNode(itc->second.d_enums[i]));
}
Node lem = NodeManager::currentNM()->mkNode(OR, disj);
+ Trace("cegis-unif-enum") << "Adding lemma " << lem << "\n";
d_qe->getOutputChannel().lemma(lem);
}
TermDbSygus* d_tds;
/** reference to the parent conjecture */
CegConjecture* d_parent;
+ /** whether this module has been initialized */
+ bool d_initialized;
/** null node */
Node d_null;
/** information per initialized type */
// Build purified head with fresh skolem and recreate node
std::stringstream ss;
ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
- Node new_f = nm->mkSkolem(ss.str(), nb[0].getType());
+ Node new_f = nm->mkSkolem(ss.str(),
+ nb[0].getType(),
+ "head of unif evaluation point",
+ NodeManager::SKOLEM_EXACT_NAME);
// Adds new enumerator to map from candidate
Trace("sygus-unif-rl-purify") << "...new enum " << new_f
<< " for candidate " << nb[0] << "\n";
{
indent("sygus-unif-sol", ind);
Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl;
+ // retrieve strategy information
+ TypeNode etn = e.getType();
+ EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+ StrategyNode& snode = tinfo.getStrategyNode(nrole);
+ if (nrole != role_equal)
+ {
+ return Node::null();
+ }
// is there a decision tree strategy?
- if (nrole == role_equal)
+ std::map<Node, DecisionTreeInfo>::iterator itd = d_stratpt_to_dt.find(e);
+ // for now only considering simple case of sole "ITE(cond, e, e)" strategy
+ if (itd == d_stratpt_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.\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);
- }
- }
+ return Node::null();
}
-
- return Node::null();
+ indent("sygus-unif-sol", ind);
+ Trace("sygus-unif-sol") << "...it has a decision tree strategy.\n";
+ // whether empty set of points
+ if (d_cand_to_eval_hds[f].empty())
+ {
+ Trace("sygus-unif-sol") << "...... no points, return root enum value "
+ << d_parent->getModelValue(e) << "\n";
+ return d_parent->getModelValue(e);
+ }
+ EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
+ return itd->second.buildSol(etis->d_cons);
}
bool SygusUnifRl::usingUnif(Node f)
return d_unif_candidates.find(f) != d_unif_candidates.end();
}
+std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
+{
+ std::map<Node, std::vector<Node>>::iterator it = d_cand_to_eval_hds.find(c);
+ if (it == d_cand_to_eval_hds.end())
+ {
+ return std::vector<Node>();
+ }
+ return it->second;
+}
+
void SygusUnifRl::registerStrategy(Node f)
{
if (Trace.isOn("sygus-unif-rl-strat"))
<< " ...detected recursive ITE strategy, condition enumerator : "
<< cond << std::endl;
// indicate that we will be enumerating values for cond
- registerConditionalEnumerator(f, e, cond);
+ registerConditionalEnumerator(f, e, cond, j);
}
}
// TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
}
}
-void SygusUnifRl::registerConditionalEnumerator(Node f, Node e, Node cond)
+void SygusUnifRl::registerConditionalEnumerator(Node f,
+ Node e,
+ Node cond,
+ unsigned strategy_index)
{
// we will do unification for this candidate
d_unif_candidates.insert(f);
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]);
+ d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index);
// 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)
+ SygusUnifStrategy* strategy,
+ unsigned strategy_index)
{
d_cond_enum = cond_enum;
d_unif = unif;
d_strategy = strategy;
+ d_strategy_index = strategy_index;
// Retrieve template
EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum);
d_template = NodePair(eiv.d_template, eiv.d_template_arg);
d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1);
}
+unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const
+{
+ return d_strategy_index;
+}
+
+using UNodePair = std::pair<unsigned, Node>;
+
+Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons)
+{
+ if (!d_template.first.isNull())
+ {
+ Trace("sygus-unif-sol") << "...templated conditions unsupported\n";
+ return Node::null();
+ }
+ if (!isSeparated())
+ {
+ Trace("sygus-unif-sol") << "...separation check failed\n";
+ return Node::null();
+ }
+ Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+ // Traverse trie and build ITE with cons
+ NodeManager* nm = NodeManager::currentNM();
+ std::map<IndTriePair, Node> cache;
+ std::map<IndTriePair, Node>::iterator it;
+ std::vector<IndTriePair> visit;
+ unsigned index = 0;
+ LazyTrie* trie;
+ IndTriePair root = IndTriePair(0, &d_pt_sep.d_trie.d_trie);
+ visit.push_back(root);
+ while (!visit.empty())
+ {
+ index = visit.back().first;
+ trie = visit.back().second;
+ visit.pop_back();
+ IndTriePair cur = IndTriePair(index, trie);
+ it = cache.find(cur);
+ // traverse children so results are saved to build node for parent
+ if (it == cache.end())
+ {
+ // leaf
+ if (trie->d_children.empty())
+ {
+ Assert(d_hd_values.find(trie->d_lazy_child) != d_hd_values.end());
+ cache[cur] = d_hd_values[trie->d_lazy_child];
+ Trace("sygus-unif-sol-debug")
+ << "......leaf, build "
+ << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+ << "\n";
+ continue;
+ }
+ cache[cur] = Node::null();
+ visit.push_back(cur);
+ for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
+ {
+ visit.push_back(IndTriePair(index + 1, &p_nt.second));
+ }
+ continue;
+ }
+ // retrieve terms of children and build result
+ Assert(it->second.isNull());
+ Assert(trie->d_children.size() == 1 || trie->d_children.size() == 2);
+ std::vector<Node> children(4);
+ children[0] = cons;
+ children[1] = d_conds[index];
+ unsigned i = 0;
+ for (std::pair<const Node, LazyTrie>& p_nt : trie->d_children)
+ {
+ i = p_nt.first.getConst<bool>() ? 2 : 3;
+ Assert(cache.find(IndTriePair(index + 1, &p_nt.second)) != cache.end());
+ children[i] = cache[IndTriePair(index + 1, &p_nt.second)];
+ Assert(!children[i].isNull());
+ }
+ // condition is useless or result children are equal, no no need for ITE
+ if (trie->d_children.size() == 1 || children[2] == children[3])
+ {
+ cache[cur] = children[i];
+ Trace("sygus-unif-sol-debug")
+ << "......no cond, build "
+ << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+ << "\n";
+ continue;
+ }
+ Assert(trie->d_children.size() == 2);
+ cache[cur] = nm->mkNode(APPLY_CONSTRUCTOR, children);
+ Trace("sygus-unif-sol-debug")
+ << "......build node "
+ << d_unif->d_tds->sygusToBuiltin(cache[cur], cache[cur].getType())
+ << "\n";
+ }
+ Assert(cache.find(root) != cache.end());
+ Assert(!cache.find(root)->second.isNull());
+ Trace("sygus-unif-sol") << "...solution is "
+ << d_unif->d_tds->sygusToBuiltin(
+ cache[root], cache[root].getType())
+ << "\n";
+ return cache[root];
+}
+
bool SygusUnifRl::DecisionTreeInfo::isSeparated()
{
+ d_hd_values.clear();
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];
+ Node v = d_unif->d_parent->getModelValue(rep_to_class.second[0]);
+ if (Trace.isOn("sygus-unif-rl-dt-debug"))
+ {
+ Trace("sygus-unif-rl-dt-debug") << "...class of ("
+ << rep_to_class.second[0];
+ Assert(d_unif->d_hd_to_pt.find(rep_to_class.second[0])
+ != d_unif->d_hd_to_pt.end());
+ for (const Node& pti : d_unif->d_hd_to_pt[rep_to_class.second[0]])
+ {
+ Trace("sygus-unif-rl-dt-debug") << " " << pti << " ";
+ }
+ Trace("sygus-unif-rl-dt-debug") << ") "
+ << " with hd value " << v << "\n";
+ }
+ d_hd_values[rep_to_class.second[0]] = v;
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]);
+ Assert(d_hd_values.find(rep_to_class.second[i]) == d_hd_values.end());
+ d_hd_values[rep_to_class.second[i]] = vi;
+ if (Trace.isOn("sygus-unif-rl-dt-debug"))
+ {
+ Trace("sygus-unif-rl-dt-debug") << "...class of ("
+ << rep_to_class.second[i];
+ Assert(d_unif->d_hd_to_pt.find(rep_to_class.second[i])
+ != d_unif->d_hd_to_pt.end());
+ for (const Node& pti : d_unif->d_hd_to_pt[rep_to_class.second[i]])
+ {
+ Trace("sygus-unif-rl-dt-debug") << " " << pti << " ";
+ }
+ Trace("sygus-unif-rl-dt-debug") << ") "
+ << " with hd value " << vi << "\n";
+ }
+ // Heads with different model values
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;
+ return false;
}
}
- // Heads with different model values
- if (i != size)
- {
- return false;
- }
}
return true;
}
PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
using BoolNodePairMap =
std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
+using NodePairMap = std::unordered_map<Node, Node, NodeHashFunction>;
using NodePair = std::pair<Node, Node>;
class CegConjecture;
*/
bool usingUnif(Node f);
+ /** retrieve the head of evaluation points for candidate c, if any */
+ std::vector<Node> getEvalPointHeads(Node c);
+
protected:
/** reference to the parent conjecture */
CegConjecture* d_parent;
/** initializes this class */
void initialize(Node cond_enum,
SygusUnifRl* unif,
- SygusUnifStrategy* strategy);
+ SygusUnifStrategy* strategy,
+ unsigned strategy_index);
/** 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);
+ /** returns index of strategy information of strategy node for this DT */
+ unsigned getStrategyIndex() const;
+ /** builds solution stored in DT, if any, using the given constructor
+ *
+ * The DT contains a solution when no class contains two heads of evaluation
+ * points with different model values, i.e. when all points that must be
+ * separated indeed are separated.
+ *
+ * This function tests separation of the points in the above sense and may
+ * create separation lemmas to enforce guide the synthesis of conditons that
+ * will separate points not currently separated.
+ */
+ Node buildSol(Node cons);
/** whether all points that must be separated are separated **/
bool isSeparated();
/** reference to parent unif util */
private:
/**
- * reference to infered strategy for the function-to-synthesize this DT is
+ * reference to inferred strategy for the function-to-synthesize this DT is
* associated with
*/
SygusUnifStrategy* d_strategy;
+ /** index of strategy information of strategy node this DT is based on
+ *
+ * this is the index of the strategy (d_strats[index]) in the strategy node
+ * to which this decision tree corresponds, which can be accessed through
+ * the above strategy reference
+ */
+ unsigned d_strategy_index;
/**
* The enumerator in the strategy tree that stores conditions of the
* decision tree.
*/
Node d_cond_enum;
+ /** chache of model values of heads of evaluation points */
+ NodePairMap d_hd_values;
/** Classifies evaluation points according to enumerated condition values
*
* Maintains the invariant that points evaluated in the same way in the
* Registers that cond is a conditional enumerator for building a (recursive)
* decision tree at strategy node e within the strategy tree of f.
*/
- void registerConditionalEnumerator(Node f, Node e, Node cond);
+ void registerConditionalEnumerator(Node f,
+ Node e,
+ Node cond,
+ unsigned strategy_index);
};
} /* CVC4::theory::quantifiers namespace */
projects / cvc5.git / commitdiff