return res;
}
+void LazyTrieMulti::clear()
+{
+ d_trie.clear();
+ d_rep_to_class.clear();
+}
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
* containing only itself.
*/
Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
+ /** clear the trie */
+ void clear();
+
/** A regular lazy trie */
LazyTrie d_trie;
};
{
Node cond = d_sygus_unif.getConditionForEvaluationPoint(e);
Assert(!cond.isNull());
- Trace("cegis-unif")
- << " " << e << " with condition : " << cond << std::endl;
+ Trace("cegis-unif") << " " << e << " with condition : " << cond
+ << std::endl;
pt_to_cond[e] = cond;
}
}
// build the values of the condition enumerators for each strategy point
std::map<Node, std::vector<Node>> condition_map;
Trace("cegis-unif-enum") << "Register new enumerated values :\n";
+ // keep track of the relation between conditional enums and their values
+ NodePairMap cenum_to_value;
for (unsigned i = 0, size = enums.size(); i < size; ++i)
{
// Non-unif enums (which are the very candidates) should not be notified
std::map<Node, Node>::iterator itc = d_cenum_to_strat_pt.find(e);
if (itc != d_cenum_to_strat_pt.end())
{
+ cenum_to_value[e] = v;
Trace("cegis-unif-enum") << " ...this is a condition for " << e << "\n";
// it is the value of a current condition
condition_map[itc->second].push_back(v);
d_sygus_unif.setConditions(cs.first, cs.second);
}
// TODO : check symmetry breaking for enumerators
- // TODO : check separation of evaluation heads wrt condition enumerators and
- // add lemmas.
// build solutions (for unif candidates a divide-and-conquer approach is used)
std::vector<Node> sols;
if (d_sygus_unif.constructSolution(sols))
}
return true;
}
+ std::map<Node, std::vector<Node>> sepPairs;
+ if (d_sygus_unif.getSeparationPairs(sepPairs))
+ {
+ // Build separation lemma based on current size, and for each heads that
+ // could not be separated, the condition values currently enumerated for its
+ // decision tree
+ NodeManager* nm = NodeManager::currentNM();
+ Node neg_cost_lit = d_u_enum_manager.getCurrentLiteral().negate();
+ std::vector<Node> cenums, cond_eqs;
+ for (std::pair<const Node, std::vector<Node>>& np : sepPairs)
+ {
+ // Build equalities between condition enumerators associated with the
+ // strategy point whose decision tree could not separate the given heads
+ d_u_enum_manager.getCondEnumeratorsForStrategyPt(np.first, cenums);
+ for (const Node& ce : cenums)
+ {
+ Assert(cenum_to_value.find(ce) != cenum_to_value.end());
+ cond_eqs.push_back(nm->mkNode(EQUAL, ce, cenum_to_value[ce]));
+ }
+ Assert(!cond_eqs.empty());
+ Node neg_conds_lit =
+ cond_eqs.size() > 1 ? nm->mkNode(AND, cond_eqs) : cond_eqs[0];
+ neg_conds_lit = neg_conds_lit.negate();
+ for (const Node& eq : np.second)
+ {
+ // A separation lemma is of the shape
+ // (cost_n+1 ^ (c_1 = M(c_1) ^ ... ^ M(c_n))) => e_i = e_j
+ // in which cost_n+1 is the cost function for the size n+1, each c_k is
+ // a conditional enumerator associated with the respective decision
+ // tree, each M(c_k) its current model value, and e_i, e_j are two
+ // distinct heads that could not be separated by these condition values
+ //
+ // Such a lemma will force the ground solver, within the restrictions of
+ // the respective cost function, to make e_i and e_j equal or to come up
+ // with new values for the conditional enumerators such that we can try
+ Node sep_lemma = nm->mkNode(OR, neg_cost_lit, neg_conds_lit, eq);
+ Trace("cegis-unif")
+ << "CegisUnif::lemma, separation lemma : " << sep_lemma << "\n";
+ d_qe->getOutputChannel().lemma(sep_lemma);
+ }
+ }
+ }
return false;
}
// Notify the enumeration manager if there are new evaluation points
for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
{
- d_u_enum_manager.registerEvalPts(ep.second, ep.first);
+ Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end());
+ // Notify each startegy point of the respective candidate
+ for (const Node& n : d_cand_to_strat_pt[ep.first])
+ {
+ d_u_enum_manager.registerEvalPts(ep.second, n);
+ }
}
// 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",
std::map<Node, Node>::const_iterator itcc = e_to_cond.find(e);
Assert(itcc != e_to_cond.end());
Node cond = itcc->second;
- Trace("cegis-unif-enum-debug")
- << "...its condition strategy point is " << cond << "\n";
+ Trace("cegis-unif-enum-debug") << "...its condition strategy point is "
+ << cond << "\n";
d_ce_info[e].d_ce_type = cond.getType();
// initialize the symmetry breaking lemma templates
for (unsigned index = 0; index < 2; index++)
{
continue;
}
- // register the enumerator
- ci.second.d_enums[index].push_back(e);
- d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
// instantiate template for removing redundant operators
if (!ci.second.d_sbt_lemma_tmpl[index].first.isNull())
{
d_qe->getOutputChannel().lemma(sym_break_red_ops);
}
// symmetry breaking between enumerators
- Node e_prev = ci.second.d_enums[index].back();
- Node size_e = nm->mkNode(DT_SIZE, e);
- Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
- Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
- Trace("cegis-unif-enum-lemma")
- << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
- d_qe->getOutputChannel().lemma(sym_break);
+ if (!ci.second.d_enums[index].empty())
+ {
+ Node e_prev = ci.second.d_enums[index].back();
+ Node size_e = nm->mkNode(DT_SIZE, e);
+ Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
+ Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
+ Trace("cegis-unif-enum-lemma")
+ << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
+ d_qe->getOutputChannel().lemma(sym_break);
+ }
+ // register the enumerator
+ ci.second.d_enums[index].push_back(e);
+ Trace("cegis-unif-enum") << "* Registering new enumerator " << e
+ << " to strategy point " << ci.second.d_pt
+ << "\n";
+ d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
// if the sygus datatype is interpreted as an infinite type
// (this should be the case for almost all examples)
TypeNode et = e.getType();
if (!et.isInterpretedFinite())
{
// it is disequal from all previous ones
- for (const Node ei : ci.second.d_enums[index])
+ for (const Node& ei : ci.second.d_enums[index])
{
+ if (ei == e)
+ {
+ continue;
+ }
Node deq = e.eqNode(ei).negate();
Trace("cegis-unif-enum-lemma")
<< "CegisUnifEnum::lemma, enum deq:" << deq << "\n";
* registerEvalPtAtValue on the output channel of d_qe.
*/
Node getNextDecisionRequest(unsigned& priority);
+ /**
+ * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n
+ * is not asserted negatively in the current SAT context.
+ */
+ Node getCurrentLiteral() const;
private:
/** reference to quantifier engine */
context::CDO<unsigned> d_curr_guq_val;
/** increment the number of enumerators */
void incrementNumEnumerators();
- /**
- * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n
- * is not asserted negatively in the current SAT context.
- */
- Node getCurrentLiteral() const;
/** get literal G_uq_n */
Node getLiteral(unsigned n) const;
/** register evaluation point at size
else
{
nv = d_parent->getModelValue(n);
- 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";
}
Assert(n != nv);
}
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";
+ Trace("sygus-unif-rl-dt") << "Register 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]);
+ d_stratpt_to_dt[stratpt].d_hds.push_back(cp.second[j]);
}
}
}
return plem;
}
-void SygusUnifRl::initializeConstructSol() {}
+void SygusUnifRl::initializeConstructSol() { d_sepPairs.clear(); }
void SygusUnifRl::initializeConstructSolFor(Node f) {}
bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
{
initializeConstructSol();
+ bool successful = true;
for (const Node& c : d_candidates)
{
if (!usingUnif(c))
{
Node v = d_parent->getModelValue(c);
- Trace("sygus-unif-rl-sol") << "Adding solution " << v
- << " to non-unif candidate " << c << "\n";
sols.push_back(v);
continue;
}
Node v = constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0);
if (v.isNull())
{
- return false;
+ // we continue trying to build solutions to accumulate potentitial
+ // separation conditions from other decision trees
+ successful = false;
+ continue;
}
- Trace("sygus-unif-rl-sol") << "Adding solution " << v
- << " to unif candidate " << c << "\n";
sols.push_back(v);
d_cand_to_sol[c] = v;
}
- return true;
+ return successful;
}
Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
return d_parent->getModelValue(e);
}
EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
- return itd->second.buildSol(etis->d_cons);
+ std::vector<Node> toSeparate;
+ Node sol = itd->second.buildSol(etis->d_cons, toSeparate);
+ if (sol.isNull())
+ {
+ Assert(!toSeparate.empty());
+ d_sepPairs[e] = toSeparate;
+ }
+ return sol;
+}
+
+bool SygusUnifRl::getSeparationPairs(
+ std::map<Node, std::vector<Node>>& sepPairs)
+{
+ sepPairs = d_sepPairs;
+ return !sepPairs.empty();
}
bool SygusUnifRl::usingUnif(Node f) const
{
std::map<Node, DecisionTreeInfo>::iterator it = d_stratpt_to_dt.find(e);
Assert(it != d_stratpt_to_dt.end());
- it->second.clearCondValues();
- /* TODO
- for (const Node& c : conds)
- {
- it->second.addCondValue(c);
- }
- */
+ // Clear previous trie
+ it->second.resetPointSeparator(conds);
}
std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
d_pt_sep.initialize(this);
}
-void SygusUnifRl::DecisionTreeInfo::addPoint(Node f)
+void SygusUnifRl::DecisionTreeInfo::resetPointSeparator(
+ const std::vector<Node>& conds)
{
- d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size());
+ // clear old condition values and trie
+ d_conds.clear();
+ d_pt_sep.d_trie.clear();
+ // set new condition values
+ d_conds.insert(d_conds.end(), conds.begin(), conds.end());
}
-void SygusUnifRl::DecisionTreeInfo::clearCondValues()
+void SygusUnifRl::DecisionTreeInfo::addPoint(Node f)
{
- // TODO
- // d_conds.clear();
+ d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size());
}
void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv)
using UNodePair = std::pair<unsigned, Node>;
-Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons)
+Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
+ std::vector<Node>& toSeparate)
{
if (!d_template.first.isNull())
{
Trace("sygus-unif-sol") << "...templated conditions unsupported\n";
return Node::null();
}
- if (!isSeparated())
+ if (!isSeparated(toSeparate))
{
Trace("sygus-unif-sol") << "...separation check failed\n";
return Node::null();
return cache[root];
}
-bool SygusUnifRl::DecisionTreeInfo::isSeparated()
+bool SygusUnifRl::DecisionTreeInfo::isSeparated(std::vector<Node>& toSeparate)
{
+ // build point separator
+ for (const Node& f : d_hds)
+ {
+ addPoint(f);
+ }
+ // check separation
d_hd_values.clear();
+ NodeManager* nm = NodeManager::currentNM();
for (const std::pair<const Node, std::vector<Node>>& rep_to_class :
d_pt_sep.d_trie.d_rep_to_class)
{
Trace("sygus-unif-rl-dt") << "...in sep class heads with diff values: "
<< rep_to_class.second[0] << " and "
<< rep_to_class.second[i] << "\n";
- return false;
+ toSeparate.push_back(
+ nm->mkNode(EQUAL, rep_to_class.second[0], rep_to_class.second[i]));
+ // For non-separation suffices to consider one head pair per sep class
+ break;
}
}
}
- return true;
+ return toSeparate.empty();
}
void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize(
/** retrieve the head of evaluation points for candidate c, if any */
std::vector<Node> getEvalPointHeads(Node c);
+ /**
+ * if a separation condition is necessary after a failed solution
+ * construction, then sepCond is assigned a pair (e, fi = fj) in which e is
+ * the strategy point and fi, fj head of evaluation points of a unif
+ * function-to-synthesize, such that fi could not be separated from fj by the
+ * current condition values
+ */
+ bool getSeparationPairs(std::map<Node, std::vector<Node>>& sepPairs);
+
protected:
/** reference to the parent conjecture */
CegConjecture* d_parent;
void initializeConstructSolFor(Node f) override;
/** maps unif functions-to~synhesize to their last built solutions */
std::map<Node, Node> d_cand_to_sol;
+ /** pair of strategy point and equality between evaluation point heads
+ *
+ * this pair is set when a unif solution cannot be built because a two
+ * evaluation point heads cannot be separated
+ */
+ std::map<Node, std::vector<Node>> d_sepPairs;
/*
--------------------------------------------------------------
Purification
SygusUnifRl* unif,
SygusUnifStrategy* strategy,
unsigned strategy_index);
- /** adds the respective evaluation point of the head f */
- void addPoint(Node f);
- /** clears the condition values */
- void clearCondValues();
- /** 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.
+ */
+ Node buildSol(Node cons, std::vector<Node>& toSeparate);
+ /** whether all points that must be separated 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.
+ * This function tests separation of the points in the above sense and in
+ * case two heads cannot be separated, an equality between them is created
+ * and stored in toSeparate, so that a separation lemma can be generated to
+ * guide the synthesis search to yield either conditions that will separate
+ * these heads or equal values to them.
*/
- Node buildSol(Node cons);
- /** whether all points that must be separated are separated **/
- bool isSeparated();
+ bool isSeparated(std::vector<Node>& toSeparate);
/** 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;
+ /** gathered evaluation point heads */
+ std::vector<Node> d_hds;
/** get condition enumerator */
Node getConditionEnumerator() const { return d_cond_enum; }
+ /** clear trie and registered condition values */
+ void resetPointSeparator(const std::vector<Node>& conds);
private:
/**
* enumerated condiotion values
*/
PointSeparator d_pt_sep;
+ /** adds the respective evaluation point of the head f to d_pt_sep */
+ void addPoint(Node f);
+ /** adds a value to the pool of condition values and to d_pt_sep */
+ void addCondValue(Node condv);
};
/** maps strategy points in the strategy tree to the above data */
std::map<Node, DecisionTreeInfo> d_stratpt_to_dt;
* 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,
- unsigned strategy_index);
+ void registerConditionalEnumerator(Node f,
+ Node e,
+ Node cond,
+ unsigned strategy_index);
};
} /* CVC4::theory::quantifiers namespace */
projects / cvc5.git / commitdiff