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