From f0bc0137d00946f79e62e223b849e7372cc0109f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 21 Nov 2018 17:07:17 -0600 Subject: [PATCH] Cache evaluations for PBE (#2699) --- .../quantifiers/sygus/sygus_enumerator.cpp | 6 +- src/theory/quantifiers/sygus/sygus_pbe.cpp | 73 +++++++------------ src/theory/quantifiers/sygus/sygus_pbe.h | 26 +------ .../quantifiers/sygus/sygus_unif_io.cpp | 42 ++++++++--- src/theory/quantifiers/sygus/sygus_unif_io.h | 14 ++++ 5 files changed, 79 insertions(+), 82 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 5c3e44a33..d4b4dd0bf 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -326,9 +326,9 @@ bool SygusEnumerator::TermCache::addTerm(Node n) { 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; } } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 408f076ac..e8aa0a7f0 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -292,53 +292,19 @@ bool SygusPbe::initialize(Node n, 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& 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 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& 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(b, PbeTrie())); + return b; } bool SygusPbe::hasExamples(Node e) @@ -409,8 +375,21 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr) Assert(!e.isNull()); std::map::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 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; } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index a62100692..dc7f1cc51 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -269,35 +269,15 @@ class SygusPbe : public SygusModule 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 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& ex, - SygusPbe* cpbe, - unsigned index, - unsigned ntotal); + Node addTerm(Node b, const std::vector& exOut); }; /** trie of candidate solutions tried * This stores information for each (enumerator, type), diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 4bd6cb7fe..3d26deeaa 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -495,6 +495,32 @@ void SygusUnifIo::addExample(const std::vector& input, Node output) d_examples_out.push_back(output); } +void SygusUnifIo::computeExamples(Node e, Node bv, std::vector& exOut) +{ + std::map>& eoc = d_exOutCache[e]; + std::map>::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& 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>& eoc = d_exOutCache[e]; + Assert(eoc.find(bv) != eoc.end()); + eoc.erase(bv); +} + void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) { Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v @@ -508,17 +534,15 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector& lemmas) // iterations. Node exp_exc; + std::vector base_results; TypeNode xtn = e.getType(); Node bv = d_tds->sygusToBuiltin(v, xtn); - std::vector 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> srmap; Evaluator* ev = d_tds->getEvaluator(); diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 967226e94..2a4ac91c8 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -301,6 +301,17 @@ class SygusUnifIo : public SygusUnif */ void addExample(const std::vector& 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& exOut); + + /** clear example cache */ + void clearExampleCache(Node e, Node bv); + protected: /** the candidate */ Node d_candidate; @@ -343,6 +354,9 @@ class SygusUnifIo : public SygusUnif /** output of I/O examples */ std::vector d_examples_out; + /** cache for computeExamples */ + std::map>> d_exOutCache; + /** * This class stores information regarding an enumerator, including: * a database of values that have been enumerated for this enumerator. -- 2.30.2