Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, 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 : : * Implements a n-ary match trie
14 : : */
15 : :
16 : : #include "expr/nary_match_trie.h"
17 : :
18 : : #include <sstream>
19 : : #include "expr/nary_term_util.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace expr {
25 : :
26 : : class NaryMatchFrame
27 : : {
28 : : public:
29 : 14401300 : NaryMatchFrame(const std::vector<Node>& syms, const NaryMatchTrie* t)
30 : 14401300 : : d_syms(syms), d_trie(t), d_index(0), d_variant(0), d_boundVar(false)
31 : : {
32 : 14401300 : }
33 : : /** Symbols to match */
34 : : std::vector<Node> d_syms;
35 : : /** The match trie */
36 : : const NaryMatchTrie* d_trie;
37 : : /** The index we are considering, 0 = operator, n>0 = variable # (n-1) */
38 : : size_t d_index;
39 : : /** List length considering */
40 : : size_t d_variant;
41 : : /** Whether we just bound a variable */
42 : : bool d_boundVar;
43 : : };
44 : :
45 : 1749880 : bool NaryMatchTrie::getMatches(Node n, NotifyMatch* ntm) const
46 : : {
47 : 1749880 : NodeManager* nm = NodeManager::currentNM();
48 : 3499750 : std::vector<Node> vars;
49 : 3499750 : std::vector<Node> subs;
50 : 3499750 : std::map<Node, Node> smap;
51 : :
52 : 1749880 : std::map<Node, NaryMatchTrie>::const_iterator itc;
53 : :
54 : 3499750 : std::vector<NaryMatchFrame> visit;
55 : 3499750 : visit.push_back(NaryMatchFrame({n}, this));
56 : :
57 [ + + ]: 36383600 : while (!visit.empty())
58 : : {
59 : 34955300 : NaryMatchFrame& curr = visit.back();
60 : : // currently, copy the symbols from previous frame TODO: improve?
61 : 34955300 : std::vector<Node> syms = curr.d_syms;
62 : 34955300 : const NaryMatchTrie* mt = curr.d_trie;
63 [ + + ]: 34955300 : if (syms.empty())
64 : : {
65 : : // if we matched, there must be a data member at this node
66 [ - + ][ - + ]: 1792220 : Assert(!mt->d_data.isNull());
[ - - ]
67 : : // notify match?
68 [ - + ][ - + ]: 1792220 : Assert(n == expr::narySubstitute(mt->d_data, vars, subs));
[ - - ]
69 [ + - ]: 1792220 : Trace("match-debug") << "notify : " << mt->d_data << std::endl;
70 [ + + ]: 1792220 : if (!ntm->notify(n, mt->d_data, vars, subs))
71 : : {
72 : 321581 : return false;
73 : : }
74 : 1470640 : visit.pop_back();
75 : 1470640 : continue;
76 : : }
77 : :
78 : : // clean up if we previously bound a variable
79 [ + + ]: 33163100 : if (curr.d_boundVar)
80 : : {
81 [ - + ][ - + ]: 8647630 : Assert(!vars.empty());
[ - - ]
82 [ - + ][ - + ]: 8647630 : Assert(smap.find(vars.back()) != smap.end());
[ - - ]
83 : 8647630 : smap.erase(vars.back());
84 : 8647630 : vars.pop_back();
85 : 8647630 : subs.pop_back();
86 : 8647630 : curr.d_boundVar = false;
87 : : }
88 : :
89 [ + + ]: 33163100 : if (curr.d_index == 0)
90 : : {
91 : 12609100 : curr.d_index++;
92 : : // finished matching variables, try to match the operator
93 : 25218100 : Node next = syms.back();
94 : : Node op =
95 [ + + ][ + + ]: 25218100 : (!next.isNull() && next.hasOperator()) ? next.getOperator() : next;
96 : 12609100 : itc = mt->d_children.find(op);
97 [ + + ]: 12609100 : if (itc != mt->d_children.end())
98 : : {
99 : 3189710 : syms.pop_back();
100 : : // push the children + null termination marker, in reverse order
101 [ + + ]: 3189710 : if (NodeManager::isNAryKind(next.getKind()))
102 : : {
103 : 490074 : syms.push_back(Node::null());
104 : : }
105 [ + + ]: 3189710 : if (next.hasOperator())
106 : : {
107 : 2704030 : syms.insert(syms.end(), next.rbegin(), next.rend());
108 : : }
109 : : // new frame
110 : 3189710 : visit.push_back(NaryMatchFrame(syms, &itc->second));
111 : : }
112 : : }
113 [ + + ]: 20554000 : else if (curr.d_index <= mt->d_vars.size())
114 : : {
115 : : // try to match the next (variable, length)
116 : 13717100 : Node var;
117 : 13717100 : Node next;
118 : 5593420 : do
119 : : {
120 : 19310500 : var = mt->d_vars[curr.d_index - 1];
121 [ - + ][ - + ]: 19310500 : Assert(mt->d_children.find(var) != mt->d_children.end());
[ - - ]
122 : 38620900 : std::vector<Node> currChildren;
123 [ + + ]: 19310500 : if (isListVar(var))
124 : : {
125 : : // get the length of the list we want to consider
126 : 5424680 : size_t l = curr.d_variant;
127 : 5424680 : curr.d_variant++;
128 : : // match with l, or increment d_index otherwise
129 : 5424680 : bool foundChildren = true;
130 : : // We are in a state where the children of an n-ary child
131 : : // have been pused to syms. We try to extract l children here. If
132 : : // we encounter the null symbol, then we do not have sufficient
133 : : // children to match for this variant and fail.
134 [ + + ]: 42159600 : for (size_t i = 0; i < l; i++)
135 : : {
136 [ - + ][ - + ]: 37666600 : Assert(!syms.empty());
[ - - ]
137 : 37666600 : Node s = syms.back();
138 : : // we currently reject the term if it does not have the same
139 : : // type as the list variable. This rejects certain corner cases of
140 : : // arithmetic operators which are permissive for subtyping.
141 : : // For example, if x is a list variable of type Real, y is a list
142 : : // variable of type Real, then (+ x y) does *not* match
143 : : // (+ 1.0 2 1.5), despite { x -> (+ 1.0 2), y -> 1.5 } being
144 : : // a well-typed match.
145 : 37666600 : if (s.isNull() || !s.getType().isComparableTo(var.getType()))
146 : : {
147 : 931673 : foundChildren = false;
148 : 931673 : break;
149 : : }
150 : 36734900 : currChildren.push_back(s);
151 : 36734900 : syms.pop_back();
152 : : }
153 [ + + ]: 5424680 : if (foundChildren)
154 : : {
155 : : // we are matching the next list
156 : 4493000 : next = nm->mkNode(Kind::SEXPR, currChildren);
157 : : }
158 : : else
159 : : {
160 : : // otherwise, we have run out of variants, go to next variable
161 : 931673 : curr.d_index++;
162 : 931673 : curr.d_variant = 0;
163 : : }
164 : : }
165 : : else
166 : : {
167 : 13885800 : next = syms.back();
168 : 13885800 : curr.d_index++;
169 : : // we could be at the end of an n-ary operator, in which case we
170 : : // do not match
171 [ + + ]: 13885800 : if (!next.isNull())
172 : : {
173 : 13120200 : currChildren.push_back(next);
174 : 13120200 : syms.pop_back();
175 [ + - ]: 26240500 : Trace("match-debug")
176 : 0 : << "Compare types " << var << " " << next << " "
177 : 13120200 : << var.getType() << " " << next.getType() << std::endl;
178 : : // check types in the (non-list) case
179 [ + + ]: 13120200 : if (!var.getType().isComparableTo(next.getType()))
180 : : {
181 [ + - ]: 4836460 : Trace("match-debug") << "...fail" << std::endl;
182 : 4836460 : next = Node::null();
183 : : }
184 : : }
185 : : }
186 [ + + ]: 19310500 : if (!next.isNull())
187 : : {
188 : : // check if it is already bound, do the binding if necessary
189 : 12776800 : std::map<Node, Node>::iterator its = smap.find(var);
190 [ + + ]: 12776800 : if (its != smap.end())
191 : : {
192 [ + + ]: 3363890 : if (its->second != next)
193 : : {
194 : : // failed to match
195 : 3315080 : next = Node::null();
196 : : }
197 : : // otherwise, successfully matched, nothing to do
198 : : }
199 : : else
200 : : {
201 : : // add to binding
202 [ + - ]: 18825800 : Trace("match-debug")
203 : 9412890 : << "Set " << var << " -> " << next << std::endl;
204 : 9412890 : vars.push_back(var);
205 : 9412890 : subs.push_back(next);
206 : 9412890 : smap[var] = next;
207 : 9412890 : curr.d_boundVar = true;
208 : : }
209 : : }
210 [ + + ]: 19310500 : if (next.isNull())
211 : : {
212 : : // if we failed, revert changes to syms
213 : 9848770 : syms.insert(syms.end(), currChildren.rbegin(), currChildren.rend());
214 : : }
215 [ + + ][ + + ]: 19310500 : } while (next.isNull() && curr.d_index <= mt->d_vars.size());
[ + + ]
216 [ + + ]: 13717100 : if (next.isNull())
217 : : {
218 : : // we are out of variables to match, finished with this frame
219 : 4255350 : visit.pop_back();
220 : 4255350 : continue;
221 : : }
222 [ + - ]: 9461700 : Trace("match-debug") << "recurse var : " << var << std::endl;
223 : 9461700 : itc = mt->d_children.find(var);
224 [ - + ][ - + ]: 9461700 : Assert(itc != mt->d_children.end());
[ - - ]
225 : 9461700 : visit.push_back(NaryMatchFrame(syms, &itc->second));
226 : : }
227 : : else
228 : : {
229 : : // no variables to match, we are done
230 : 6836960 : visit.pop_back();
231 : : }
232 : : }
233 : 1428300 : return true;
234 : : }
235 : :
236 : 1526730 : void NaryMatchTrie::addTerm(Node n)
237 : : {
238 [ - + ][ - + ]: 1526730 : Assert(!n.isNull());
[ - - ]
239 : 3053460 : std::vector<Node> visit;
240 : 1526730 : visit.push_back(n);
241 : 1526730 : NaryMatchTrie* curr = this;
242 [ + + ]: 10434800 : while (!visit.empty())
243 : : {
244 : 17816100 : Node cn = visit.back();
245 : 8908070 : visit.pop_back();
246 [ + + ]: 8908070 : if (cn.isNull())
247 : : {
248 : 1121090 : curr = &(curr->d_children[cn]);
249 : : }
250 [ + + ]: 7786970 : else if (cn.hasOperator())
251 : : {
252 : 2928900 : curr = &(curr->d_children[cn.getOperator()]);
253 : : // add null terminator if an n-ary kind
254 [ + + ]: 2928900 : if (NodeManager::isNAryKind(cn.getKind()))
255 : : {
256 : 1121090 : visit.push_back(Node::null());
257 : : }
258 : : // note children are processed left to right
259 : 2928900 : visit.insert(visit.end(), cn.rbegin(), cn.rend());
260 : : }
261 : : else
262 : : {
263 : 4858070 : if (cn.isVar()
264 [ + + ][ + + ]: 14095100 : && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
265 [ + + ]: 14095100 : == curr->d_vars.end())
266 : : {
267 : 3267460 : curr->d_vars.push_back(cn);
268 : : }
269 : 4858070 : curr = &(curr->d_children[cn]);
270 : : }
271 : : }
272 : 1526730 : curr->d_data = n;
273 : 1526730 : }
274 : :
275 : 0 : void NaryMatchTrie::clear()
276 : : {
277 : 0 : d_children.clear();
278 : 0 : d_vars.clear();
279 : 0 : d_data = Node::null();
280 : 0 : }
281 : :
282 : 0 : std::string NaryMatchTrie::debugPrint() const
283 : : {
284 : 0 : std::stringstream ss;
285 : 0 : std::vector<std::tuple<const NaryMatchTrie*, size_t, Node>> visit;
286 : 0 : visit.emplace_back(this, 0, Node::null());
287 : 0 : do
288 : : {
289 : 0 : std::tuple<const NaryMatchTrie*, size_t, Node> curr = visit.back();
290 : 0 : visit.pop_back();
291 : 0 : size_t indent = std::get<1>(curr);
292 [ - - ]: 0 : for (size_t i = 0; i < indent; i++)
293 : : {
294 : 0 : ss << " ";
295 : : }
296 : 0 : Node n = std::get<2>(curr);
297 [ - - ]: 0 : if (indent == 0)
298 : : {
299 : 0 : ss << ".";
300 : : }
301 : : else
302 : : {
303 : 0 : ss << n;
304 : : }
305 : 0 : ss << ((!n.isNull() && isListVar(n)) ? " [*]" : "");
306 : 0 : ss << std::endl;
307 : 0 : const NaryMatchTrie* mt = std::get<0>(curr);
308 [ - - ]: 0 : for (const std::pair<const Node, NaryMatchTrie>& c : mt->d_children)
309 : : {
310 : 0 : visit.emplace_back(&c.second, indent + 1, c.first);
311 : : }
312 [ - - ]: 0 : } while (!visit.empty());
313 : 0 : return ss.str();
314 : : }
315 : :
316 : : } // namespace expr
317 : : } // namespace cvc5::internal
|
