1 /********************* */
2 /*! \file node_trie.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief A trie class for Nodes and TNodes.
13 **/
14
15 #include "cvc4_private.h"
16
17 #ifndef __CVC4__EXPR__NODE_TRIE_H
18 #define __CVC4__EXPR__NODE_TRIE_H
19
20 #include <map>
21 #include "expr/node.h"
22
23 namespace CVC4 {
24 namespace theory {
25
26 /** NodeTemplate trie class
27 *
28 * This is a trie data structure whose distinguishing feature is that it has
29 * no "data" members and only references to children. The motivation for having
30 * no data members is efficiency.
31 *
32 * One use of this class is to represent "term indices" or a "signature tables"
33 * for symbols with fixed arities. In this use case, we "index" terms by the
34 * list of representatives of their arguments.
35 *
36 * For example, consider the equivalence classes :
37 *
38 * { a, d, f( d, c ), f( a, c ) }
39 * { b, f( b, d ) }
40 * { c, f( b, b ) }
41 *
42 * where the first elements ( a, b, c ) are the representatives of these
43 * classes. The NodeTemplateTrie t we may build for f is :
44 *
45 * t :
46 * t.d_data[a] :
47 * t.d_data[a].d_data[c] :
48 * t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf)
49 * t.d_data[b] :
50 * t.d_data[b].d_data[b] :
51 * t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf)
52 * t.d_data[b].d_data[d] :
53 * t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf)
54 *
55 * Leaf nodes store the terms that are indexed by the arguments, for example
56 * term f(d,c) is indexed by the representative arguments (a,c), and is stored
57 * as a the (single) key in the data of t.d_data[a].d_data[c].
58 */
59 template <bool ref_count>
60 class NodeTemplateTrie
61 {
62 public:
63 /** The children of this node. */
64 std::map<NodeTemplate<ref_count>, NodeTemplateTrie<ref_count>> d_data;
65 /** For leaf nodes : does this node have data? */
hasData()66 bool hasData() const { return !d_data.empty(); }
67 /** For leaf nodes : get the node corresponding to this leaf. */
getData()68 NodeTemplate<ref_count> getData() const { return d_data.begin()->first; }
69 /**
70 * Returns the term that is indexed by reps, if one exists, or
71 * or returns null otherwise.
72 */
73 NodeTemplate<ref_count> existsTerm(
74 const std::vector<NodeTemplate<ref_count>>& reps) const;
75 /**
76 * Returns the term that is previously indexed by reps, if one exists, or
77 * adds n to the trie, indexed by reps, and returns n.
78 */
79 NodeTemplate<ref_count> addOrGetTerm(
80 NodeTemplate<ref_count> n,
81 const std::vector<NodeTemplate<ref_count>>& reps);
82 /**
83 * Returns false if a term is previously indexed by reps.
84 * Returns true if no term is previously indexed by reps,
85 * and adds n to the trie, indexed by reps.
86 */
87 inline bool addTerm(NodeTemplate<ref_count> n,
88 const std::vector<NodeTemplate<ref_count>>& reps);
89 /** Debug print this trie on Trace c with indentation depth. */
90 void debugPrint(const char* c, unsigned depth = 0) const;
91 /** Clear all data from this trie. */
clear()92 void clear() { d_data.clear(); }
93 /** Is this trie empty? */
empty()94 bool empty() const { return d_data.empty(); }
95 }; /* class NodeTemplateTrie */
96
97 template <bool ref_count>
addTerm(NodeTemplate<ref_count> n,const std::vector<NodeTemplate<ref_count>> & reps)98 bool NodeTemplateTrie<ref_count>::addTerm(
99 NodeTemplate<ref_count> n, const std::vector<NodeTemplate<ref_count>>& reps)
100 {
101 return addOrGetTerm(n, reps) == n;
102 }
103
104 /** Reference-counted version of the above data structure */
105 typedef NodeTemplateTrie<true> NodeTrie;
106 /** Non-reference-counted version of the above data structure */
107 typedef NodeTemplateTrie<false> TNodeTrie;
108
109 } // namespace theory
110 } // namespace CVC4
111
112 #endif /* __CVC4__EXPR__NODE_TRIE_H */
113