diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/example_eval_cache.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/example_eval_cache.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_enumerator.cpp | 2 |
3 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp index 2a43335d7..ee5394972 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.cpp +++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp @@ -43,7 +43,7 @@ ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds, ExampleEvalCache::~ExampleEvalCache() {} -Node ExampleEvalCache::addSearchVal(Node bv) +Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv) { if (!d_indexSearchVals) { @@ -53,7 +53,7 @@ Node ExampleEvalCache::addSearchVal(Node bv) std::vector<Node> vals; evaluateVec(bv, vals, true); Trace("sygus-pbe-debug") << "Add to trie..." << std::endl; - Node ret = d_trie.addOrGetTerm(bv, vals); + Node ret = d_trie[tn].addOrGetTerm(bv, vals); Trace("sygus-pbe-debug") << "...got " << ret << std::endl; // Only save the cache data if necessary: if the enumerated term // is redundant, its cached data will not be used later and thus should diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h index 6aa78851f..6c5a65e7f 100644 --- a/src/theory/quantifiers/sygus/example_eval_cache.h +++ b/src/theory/quantifiers/sygus/example_eval_cache.h @@ -81,6 +81,10 @@ class ExampleEvalCache * procedure for SyGuS datatypes or the SyGuS fast enumerator when we are * considering a value of enumerator e passed to the constructor of this * class whose analog in the signature of builtin theory is bvr. + * + * The type tn passed to this function is the sygus type of the term whose + * builtin equivalent is bvr. Terms with distinct types must be cached + * independently since two sygus types may not generate the same terms. * * This returns either: * - A term that is equivalent to bvr up to examples that was passed as the @@ -94,7 +98,7 @@ class ExampleEvalCache * result of the evaluation of bvr is cached by this class, and can be * later accessed by evaluateVec below. */ - Node addSearchVal(Node bvr); + Node addSearchVal(TypeNode tn, Node bvr); //----------------------------------- evaluating terms /** Evaluate vector * @@ -149,7 +153,7 @@ class ExampleEvalCache * This is used for symmetry breaking in quantifier-free reasoning * about SyGuS datatypes. */ - NodeTrie d_trie; + std::map< TypeNode, NodeTrie> d_trie; /** cache for evaluate */ std::map<Node, std::vector<Node>> d_exOutCache; }; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 551a9d225..3923361b1 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -346,7 +346,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n) { ++(d_stats->d_enumTermsExampleEval); // Is it equivalent under examples? - Node bne = d_eec->addSearchVal(bnr); + Node bne = d_eec->addSearchVal(d_tn, bnr); if (!bne.isNull()) { if (bnr != bne) |