diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-27 15:39:13 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-27 13:39:13 -0800 |
commit | a2bba0806dab0e0d4728bbba8e4e6b4160335eeb (patch) | |
tree | 76a9508f241908561176d2105a59195137944ec6 /src/expr/node_trie.cpp | |
parent | 711234e01a17289d1fa4af3574ddf5d6de2405a1 (diff) |
Make (T)NodeTrie a general utility (#2489)
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.
Diffstat (limited to 'src/expr/node_trie.cpp')
-rw-r--r-- | src/expr/node_trie.cpp | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp new file mode 100644 index 000000000..4404e78ca --- /dev/null +++ b/src/expr/node_trie.cpp @@ -0,0 +1,95 @@ +/********************* */ +/*! \file node_trie.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of a trie class for Nodes and TNodes. + **/ + +#include "expr/node_trie.h" + +namespace CVC4 { +namespace theory { + +template <bool ref_count> +NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::existsTerm( + const std::vector<NodeTemplate<ref_count>>& reps) const +{ + const NodeTemplateTrie<ref_count>* tnt = this; + typename std::map<NodeTemplate<ref_count>, + NodeTemplateTrie<ref_count>>::const_iterator it; + for (const NodeTemplate<ref_count> r : reps) + { + it = tnt->d_data.find(r); + if (it == tnt->d_data.end()) + { + // didn't find this child, return null + return Node::null(); + } + tnt = &it->second; + } + if (tnt->d_data.empty()) + { + return Node::null(); + } + return tnt->d_data.begin()->first; +} + +template TNode NodeTemplateTrie<false>::existsTerm( + const std::vector<TNode>& reps) const; +template Node NodeTemplateTrie<true>::existsTerm( + const std::vector<Node>& reps) const; + +template <bool ref_count> +NodeTemplate<ref_count> NodeTemplateTrie<ref_count>::addOrGetTerm( + NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps) +{ + NodeTemplateTrie<ref_count>* tnt = this; + for (const NodeTemplate<ref_count> r : reps) + { + tnt = &(tnt->d_data[r]); + } + if (tnt->d_data.empty()) + { + // Store n in d_data. This should be interpretted as the "data" and not as a + // reference to a child. + tnt->d_data[n].clear(); + return n; + } + return tnt->d_data.begin()->first; +} + +template TNode NodeTemplateTrie<false>::addOrGetTerm( + TNode n, const std::vector<TNode>& reps); +template Node NodeTemplateTrie<true>::addOrGetTerm( + Node n, const std::vector<Node>& reps); + +template <bool ref_count> +void NodeTemplateTrie<ref_count>::debugPrint(const char* c, + unsigned depth) const +{ + for (const std::pair<const NodeTemplate<ref_count>, + NodeTemplateTrie<ref_count>>& p : d_data) + { + for (unsigned i = 0; i < depth; i++) + { + Trace(c) << " "; + } + Trace(c) << p.first << std::endl; + p.second.debugPrint(c, depth + 1); + } +} + +template void NodeTemplateTrie<false>::debugPrint(const char* c, + unsigned depth) const; +template void NodeTemplateTrie<true>::debugPrint(const char* c, + unsigned depth) const; + +} // namespace theory +} // namespace CVC4 |