/*! \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.
}
return lt->d_lazy_child;
}
- std::vector<Node> ex;
if (lt->d_children.empty())
{
if (lt->d_lazy_child.isNull())
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 */
/*! \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.
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 */
projects / cvc5.git / commitdiff