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