only lazy trie changes (#1885)

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<Node> 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<unsigned, LazyTrie*>;
+
+void LazyTrieMulti::addClassifier(LazyTrieEvaluator* ev, unsigned ntotal)
+{
+  Trace("lazy-trie-multi") << "LazyTrieM: Adding classifier " << ntotal + 1
+                           << "\n";
+  std::vector<IndTriePair> 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<const Node, LazyTrie>& 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<Node> 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<Node, LazyTrie>::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<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 */