From f73aef2d69428c0eba57b78a542f2d219ef14a3e Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 8 May 2018 07:32:10 -0500 Subject: [PATCH] only lazy trie changes (#1885) --- src/theory/quantifiers/lazy_trie.cpp | 94 +++++++++++++++++++++++++++- src/theory/quantifiers/lazy_trie.h | 70 ++++++++++++++++++++- 2 files changed, 161 insertions(+), 3 deletions(-) diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp index 5a63024b8..9e910b43a 100644 --- a/src/theory/quantifiers/lazy_trie.cpp +++ b/src/theory/quantifiers/lazy_trie.cpp @@ -2,7 +2,7 @@ /*! \file lazy_trie.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -36,7 +36,6 @@ Node LazyTrie::add(Node n, } return lt->d_lazy_child; } - std::vector ex; if (lt->d_children.empty()) { if (lt->d_lazy_child.isNull()) @@ -60,6 +59,97 @@ Node LazyTrie::add(Node n, return Node::null(); } +using IndTriePair = std::pair; + +void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal) +{ + Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1 + << "\n"; + std::vector visit; + unsigned index = 0; + LazyTrie* trie; + visit.push_back(IndTriePair(0, &d_trie)); + while (!visit.empty()) + { + index = visit.back().first; + trie = visit.back().second; + visit.pop_back(); + // not at (previous) last level, traverse children + if (index < ntotal) + { + for (std::pair& p_nt : trie->d_children) + { + visit.push_back(IndTriePair(index + 1, &p_nt.second)); + } + continue; + } + Assert(trie->d_children.empty()); + // if last level and no element at leaf, ignore + if (trie->d_lazy_child.isNull()) + { + continue; + } + // apply new classifier + Assert(d_rep_to_class.find(trie->d_lazy_child) != d_rep_to_class.end()); + std::vector prev_sep_class = d_rep_to_class[trie->d_lazy_child]; + if (Trace.isOn("lazy-trie-multi")) + { + Trace("lazy-trie-multi") << "...last level. Prev sep class: \n"; + for (const Node& n : prev_sep_class) + { + Trace("lazy-trie-multi") << "...... " << n << "\n"; + } + } + // make new sepclass of lc a singleton with itself + d_rep_to_class.erase(trie->d_lazy_child); + // replace + trie->d_lazy_child = Node::null(); + for (const Node& n : prev_sep_class) + { + Node eval = ev->evaluate(n, index); + std::map::iterator it = trie->d_children.find(eval); + if (it != trie->d_children.end()) + { + // add n to to map of item in next level + Trace("lazy-trie-multi") << "...add " << n << " to the class of " + << it->second.d_lazy_child << "\n"; + d_rep_to_class[it->second.d_lazy_child].push_back(n); + continue; + } + // store at next level + trie->d_children[eval].d_lazy_child = n; + // create new map + Trace("lazy-trie-multi") << "...create new class for : " << n << "\n"; + Assert(d_rep_to_class.find(n) == d_rep_to_class.end()); + d_rep_to_class[n].clear(); + d_rep_to_class[n].push_back(n); + } + } +} + +Node LazyTrieMulti::add(Node f, LazyTrieEvaluator* ev, unsigned ntotal) +{ + Trace("lazy-trie-multi") << "LazyTrieM: Adding " << f << "\n"; + Node res = d_trie.add(f, ev, 0, ntotal, false); + // f was added to the separation class with representative res + if (res != f) + { + Trace("lazy-trie-multi") << "... added " << f << " to the sepclass of " + << res << "\n"; + Assert(d_rep_to_class.find(res) != d_rep_to_class.end()); + Assert(!d_rep_to_class[res].empty()); + d_rep_to_class[res].push_back(f); + return res; + } + // f is the representatitve of a singleton seperation class + Trace("lazy-trie-multi") << "... added " << f + << " as the rep of the sepclass with itself\n"; + Assert(d_rep_to_class.find(res) == d_rep_to_class.end()); + d_rep_to_class[res].clear(); + d_rep_to_class[res].push_back(f); + return res; +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index b114f55df..2da76d6ef 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -2,7 +2,7 @@ /*! \file lazy_trie.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -94,6 +94,74 @@ class LazyTrie bool forceKeep); }; +/** Lazy trie with multiple elements per leaf + * + * As the above trie, but allows multiple elements per leaf. This is done by + * keeping classes of elements associated with each element kept in a leaf, + * which is denoted the representative of the class associated with that leaf. + * + * Another feature of this data structure is to allow the insertion of new + * classifiers besides that of data. + */ +class LazyTrieMulti +{ + public: + /** maps representatives to their classes + * + * the equivalence relation is defined in terms of the tuple of evaluations + * under the current classifiers. For example if we currently have three + * classifiers and four elements -- a,b,c,d -- have been inserted into the + * trie such that their evaluation on the classifiers are: + * + * a -> (0, 0, 0) + * b -> (1, 3, 0) + * c -> (1, 3, 0) + * d -> (1, 3, 0) + * + * then a is the representative of the class {a}, while b of the class {b,c,d} + */ + std::map> d_rep_to_class; + /** adds a new classifier to the trie + * + * When a new classifier is added a new level is added to each leaf that has + * data and the class associated with the element is the leaf is separated + * according to the new classifier. + * + * For example in the following trie with three classifiers: + * + * root: null + * d_children[0]: a -> {a} + * d_children[1]: null + * d_children[3]: null + * d_children[0] : b -> {b, c, d} + * + * to which we add a fourth classifier C such that C(b) = 0, C(c) = 1, C(d) = + * 1 we have the resulting trie: + * + * root: null + * d_children[0]: a -> {a} + * d_children[1]: null + * d_children[3]: null + * d_children[0] : null + * d_children[0] : b -> {b} + * d_children[1] : c -> {c, d} + * + * ntotal is the number of classifiers before the addition of the new one. In + * the above example it would be 3. + */ + void addClassifier(LazyTrieEvaluator* ev, unsigned ntotal); + /** adds an element to the trie + * + * If f ends it in a leaf that already contains an element, it is added to the + * class of that element. Otherwise it becomes the representative of the class + * containing only itself. + */ + Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal); + private: + /** A regular lazy trie */ + LazyTrie d_trie; +}; + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ -- 2.30.2