Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Lazy trie.
14 : : */
15 : :
16 : : #ifndef CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H
17 : : #define CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H
18 : :
19 : : #include "expr/node.h"
20 : :
21 : : namespace cvc5::internal {
22 : : namespace theory {
23 : : namespace quantifiers {
24 : :
25 : : /** abstract evaluator class
26 : : *
27 : : * This class is used for the LazyTrie data structure below.
28 : : */
29 : : class LazyTrieEvaluator
30 : : {
31 : : public:
32 : 21670 : virtual ~LazyTrieEvaluator() {}
33 : : virtual Node evaluate(Node n, unsigned index) = 0;
34 : : };
35 : :
36 : : /** LazyTrie
37 : : *
38 : : * This is a trie where terms are added in a lazy fashion. This data structure
39 : : * is useful, for instance, when we are only interested in when two terms
40 : : * map to the same node in the trie but we need not care about computing
41 : : * exactly where they are.
42 : : *
43 : : * In other words, when a term n is added to this trie, we do not insist
44 : : * that n is placed at the maximal depth of the trie. Instead, we place n at a
45 : : * minimal depth node that has no children. In this case we say n is partially
46 : : * evaluated in this trie.
47 : : *
48 : : * This class relies on an abstract evaluator interface above, which evaluates
49 : : * nodes for indices.
50 : : *
51 : : * For example, say we have terms a, b, c and an evaluator ev where:
52 : : * ev->evaluate( a, 0,1,2 ) = 0, 5, 6
53 : : * ev->evaluate( b, 0,1,2 ) = 1, 3, 0
54 : : * ev->evaluate( c, 0,1,2 ) = 1, 3, 2
55 : : * After adding a to the trie, we get:
56 : : * root: a
57 : : * After adding b to the resulting trie, we get:
58 : : * root: null
59 : : * d_children[0]: a
60 : : * d_children[1]: b
61 : : * After adding c to the resulting trie, we get:
62 : : * root: null
63 : : * d_children[0]: a
64 : : * d_children[1]: null
65 : : * d_children[3]: null
66 : : * d_children[0] : b
67 : : * d_children[2] : c
68 : : * Notice that we need not call ev->evalute( a, 1 ) and ev->evalute( a, 2 ).
69 : : */
70 : : class LazyTrie
71 : : {
72 : : public:
73 : 12708 : LazyTrie() {}
74 : 12708 : ~LazyTrie() {}
75 : : /** the data at this node, which may be partially evaluated */
76 : : Node d_lazy_child;
77 : : /** the children of this node */
78 : : std::map<Node, LazyTrie> d_children;
79 : : /** clear the trie */
80 : 1814 : void clear() { d_children.clear(); }
81 : : /** add n to the trie
82 : : *
83 : : * This function returns a node that is mapped to the same node in the trie
84 : : * if one exists, or n otherwise.
85 : : *
86 : : * ev is an evaluator which determines where n is placed in the trie
87 : : * index is the depth of this node
88 : : * ntotal is the maximal depth of the trie
89 : : * forceKeep is whether we wish to force that n is chosen as a representative
90 : : */
91 : : Node add(Node n,
92 : : LazyTrieEvaluator* ev,
93 : : unsigned index,
94 : : unsigned ntotal,
95 : : bool forceKeep);
96 : : };
97 : :
98 : : using IndTriePair = std::pair<unsigned, LazyTrie*>;
99 : :
100 : : /** Lazy trie with multiple elements per leaf
101 : : *
102 : : * As the above trie, but allows multiple elements per leaf. This is done by
103 : : * keeping classes of elements associated with each element kept in a leaf,
104 : : * which is denoted the representative of the class associated with that leaf.
105 : : *
106 : : * Another feature of this data structure is to allow the insertion of new
107 : : * classifiers besides that of data.
108 : : */
109 : : class LazyTrieMulti
110 : : {
111 : : public:
112 : : /** maps representatives to their classes
113 : : *
114 : : * the equivalence relation is defined in terms of the tuple of evaluations
115 : : * under the current classifiers. For example if we currently have three
116 : : * classifiers and four elements -- a,b,c,d -- have been inserted into the
117 : : * trie such that their evaluation on the classifiers are:
118 : : *
119 : : * a -> (0, 0, 0)
120 : : * b -> (1, 3, 0)
121 : : * c -> (1, 3, 0)
122 : : * d -> (1, 3, 0)
123 : : *
124 : : * then a is the representative of the class {a}, while b of the class {b,c,d}
125 : : */
126 : : std::map<Node, std::vector<Node>> d_rep_to_class;
127 : : /** adds a new classifier to the trie
128 : : *
129 : : * When a new classifier is added a new level is added to each leaf that has
130 : : * data and the class associated with the element is the leaf is separated
131 : : * according to the new classifier.
132 : : *
133 : : * For example in the following trie with three classifiers:
134 : : *
135 : : * root: null
136 : : * d_children[0]: a -> {a}
137 : : * d_children[1]: null
138 : : * d_children[3]: null
139 : : * d_children[0] : b -> {b, c, d}
140 : : *
141 : : * to which we add a fourth classifier C such that C(b) = 0, C(c) = 1, C(d) =
142 : : * 1 we have the resulting trie:
143 : : *
144 : : * root: null
145 : : * d_children[0]: a -> {a}
146 : : * d_children[1]: null
147 : : * d_children[3]: null
148 : : * d_children[0] : null
149 : : * d_children[0] : b -> {b}
150 : : * d_children[1] : c -> {c, d}
151 : : *
152 : : * ntotal is the number of classifiers before the addition of the new one. In
153 : : * the above example it would be 3.
154 : : */
155 : : void addClassifier(LazyTrieEvaluator* ev, unsigned ntotal);
156 : : /** adds an element to the trie
157 : : *
158 : : * If f ends it in a leaf that already contains an element, it is added to the
159 : : * class of that element. Otherwise it becomes the representative of the class
160 : : * containing only itself.
161 : : */
162 : : Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
163 : : /** clear the trie */
164 : : void clear();
165 : :
166 : : /** A regular lazy trie */
167 : : LazyTrie d_trie;
168 : : };
169 : :
170 : : } // namespace quantifiers
171 : : } // namespace theory
172 : : } // namespace cvc5::internal
173 : :
174 : : #endif /* CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H */
|
