{
if (bnr != bne)
{
- Trace("sygus-enum-exc") << "Exclude (by examples): " << bn
- << ", since we already have " << bne
- << "!=" << bnr << std::endl;
+ Trace("sygus-enum-exc")
+ << "Exclude (by examples): " << bn << ", since we already have "
+ << bne << std::endl;
return false;
}
}
return true;
}
-Node SygusPbe::PbeTrie::addPbeExample(TypeNode etn,
- Node e,
- Node b,
- SygusPbe* cpbe,
- unsigned index,
- unsigned ntotal)
+Node SygusPbe::PbeTrie::addTerm(Node b, const std::vector<Node>& exOut)
{
- if (index == ntotal) {
- // lazy child holds the leaf data
- if (d_lazy_child.isNull()) {
- d_lazy_child = b;
- }
- return d_lazy_child;
- } else {
- std::vector<Node> ex;
- if (d_children.empty()) {
- if (d_lazy_child.isNull()) {
- d_lazy_child = b;
- return d_lazy_child;
- } else {
- // evaluate the lazy child
- Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
- Assert(index < cpbe->d_examples[e].size());
- ex = cpbe->d_examples[e][index];
- addPbeExampleEval(etn, e, d_lazy_child, ex, cpbe, index, ntotal);
- Assert(!d_children.empty());
- d_lazy_child = Node::null();
- }
- } else {
- Assert(cpbe->d_examples.find(e) != cpbe->d_examples.end());
- Assert(index < cpbe->d_examples[e].size());
- ex = cpbe->d_examples[e][index];
- }
- return addPbeExampleEval(etn, e, b, ex, cpbe, index, ntotal);
+ PbeTrie* curr = this;
+ for (const Node& eo : exOut)
+ {
+ curr = &(curr->d_children[eo]);
}
-}
-
-Node SygusPbe::PbeTrie::addPbeExampleEval(TypeNode etn,
- Node e,
- Node b,
- std::vector<Node>& ex,
- SygusPbe* cpbe,
- unsigned index,
- unsigned ntotal)
-{
- Node eb = cpbe->d_tds->evaluateBuiltin(etn, b, ex);
- return d_children[eb].addPbeExample(etn, e, b, cpbe, index + 1, ntotal);
+ if (!curr->d_children.empty())
+ {
+ return curr->d_children.begin()->first;
+ }
+ curr->d_children.insert(std::pair<Node, PbeTrie>(b, PbeTrie()));
+ return b;
}
bool SygusPbe::hasExamples(Node e)
Assert(!e.isNull());
std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee);
if (itx == d_examples_invalid.end()) {
- unsigned nex = d_examples[ee].size();
- Node ret = d_pbe_trie[e][tn].addPbeExample(tn, ee, bvr, this, 0, nex);
+ // compute example values with the I/O utility
+ std::vector<Node> vals;
+ Trace("sygus-pbe-debug")
+ << "Compute examples " << bvr << "..." << std::endl;
+ d_sygus_unif[ee].computeExamples(e, bvr, vals);
+ Assert(vals.size() == d_examples[ee].size());
+ Trace("sygus-pbe-debug") << "...got " << vals << std::endl;
+ Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
+ Node ret = d_pbe_trie[e][tn].addTerm(bvr, vals);
+ Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
+ if (ret != bvr)
+ {
+ Trace("sygus-pbe-debug") << "...clear example cache" << std::endl;
+ d_sygus_unif[ee].clearExampleCache(e, bvr);
+ }
Assert(ret.getType() == bvr.getType());
return ret;
}
public:
PbeTrie() {}
~PbeTrie() {}
- /** the data for this node in the trie */
- Node d_lazy_child;
/** the children for this node in the trie */
std::map<Node, PbeTrie> d_children;
/** clear this trie */
void clear() { d_children.clear(); }
/**
- * Add term b as a value enumerated for enumerator e to the trie.
- *
- * cpbe : reference to the parent pbe utility which stores the examples,
- * index : the index of the example we are processing,
- * ntotal : the total of the examples for enumerator e.
+ * Add term b whose value on examples is exOut to the trie. Return
+ * the first term registered to this trie whose evaluation was exOut.
*/
- Node addPbeExample(TypeNode etn,
- Node e,
- Node b,
- SygusPbe* cpbe,
- unsigned index,
- unsigned ntotal);
-
- private:
- /** Helper function for above, called when we get the current example ex. */
- Node addPbeExampleEval(TypeNode etn,
- Node e,
- Node b,
- std::vector<Node>& ex,
- SygusPbe* cpbe,
- unsigned index,
- unsigned ntotal);
+ Node addTerm(Node b, const std::vector<Node>& exOut);
};
/** trie of candidate solutions tried
* This stores information for each (enumerator, type),
d_examples_out.push_back(output);
}
+void SygusUnifIo::computeExamples(Node e, Node bv, std::vector<Node>& exOut)
+{
+ std::map<Node, std::vector<Node>>& eoc = d_exOutCache[e];
+ std::map<Node, std::vector<Node>>::iterator it = eoc.find(bv);
+ if (it != eoc.end())
+ {
+ exOut.insert(exOut.end(), it->second.begin(), it->second.end());
+ return;
+ }
+ TypeNode xtn = e.getType();
+ std::vector<Node>& eocv = eoc[bv];
+ for (size_t j = 0, size = d_examples.size(); j < size; j++)
+ {
+ Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]);
+ exOut.push_back(res);
+ eocv.push_back(res);
+ }
+}
+
+void SygusUnifIo::clearExampleCache(Node e, Node bv)
+{
+ std::map<Node, std::vector<Node>>& eoc = d_exOutCache[e];
+ Assert(eoc.find(bv) != eoc.end());
+ eoc.erase(bv);
+}
+
void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
{
Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v
// iterations.
Node exp_exc;
+ std::vector<Node> base_results;
TypeNode xtn = e.getType();
Node bv = d_tds->sygusToBuiltin(v, xtn);
- std::vector<Node> base_results;
- // compte the results
- for (unsigned j = 0, size = d_examples.size(); j < size; j++)
- {
- Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]);
- Trace("sygus-sui-enum-debug")
- << "...got res = " << res << " from " << bv << std::endl;
- base_results.push_back(res);
- }
+ bv = d_tds->getExtRewriter()->extendedRewrite(bv);
+ Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl;
+ // compte the results (should be cached)
+ computeExamples(e, bv, base_results);
+ // don't need it after this
+ clearExampleCache(e, bv);
// get the results for each slave enumerator
std::map<Node, std::vector<Node>> srmap;
Evaluator* ev = d_tds->getEvaluator();
*/
void addExample(const std::vector<Node>& input, Node output);
+ /** compute examples
+ *
+ * This adds the result of evaluating bv on the set of input examples managed
+ * by this class. Term bv is the builtin version of a term generated for
+ * enumerator e. It stores the resulting output for each example in exOut.
+ */
+ void computeExamples(Node e, Node bv, std::vector<Node>& exOut);
+
+ /** clear example cache */
+ void clearExampleCache(Node e, Node bv);
+
protected:
/** the candidate */
Node d_candidate;
/** output of I/O examples */
std::vector<Node> d_examples_out;
+ /** cache for computeExamples */
+ std::map<Node, std::map<Node, std::vector<Node>>> d_exOutCache;
+
/**
* This class stores information regarding an enumerator, including:
* a database of values that have been enumerated for this enumerator.
projects / cvc5.git / commitdiff