only lazy trie changes (#1885)

1 files changed, 69 insertions, 1 deletions

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<Node, std::vector<Node>> 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 */