Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Mathias Preiner, Daniel Larraz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : 8061140 : NaryMatchFrame(const std::vector<Node>& syms, const NaryMatchTrie* t)
30 : 8061140 : : d_syms(syms), d_trie(t), d_index(0), d_variant(0), d_boundVar(false)
31 : : {
32 : 8061140 : }
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 : 946998 : bool NaryMatchTrie::getMatches(Node n, NotifyMatch* ntm) const
46 : : {
47 : 946998 : NodeManager* nm = n.getNodeManager();
48 : 1894000 : std::vector<Node> vars;
49 : 1894000 : std::vector<Node> subs;
50 : 1894000 : std::map<Node, Node> smap;
51 : :
52 : 946998 : std::map<Node, NaryMatchTrie>::const_iterator itc;
53 : :
54 : 1894000 : std::vector<NaryMatchFrame> visit;
55 : 1894000 : visit.push_back(NaryMatchFrame({n}, this));
56 : :
57 [ + + ]: 19930800 : while (!visit.empty())
58 : : {
59 : 19234100 : NaryMatchFrame& curr = visit.back();
60 : : // currently, copy the symbols from previous frame TODO: improve?
61 : 19234100 : std::vector<Node> syms = curr.d_syms;
62 : 19234100 : const NaryMatchTrie* mt = curr.d_trie;
63 [ + + ]: 19234100 : if (syms.empty())
64 : : {
65 : : // if we matched, there must be a data member at this node
66 [ - + ][ - + ]: 1082360 : Assert(!mt->d_data.isNull());
[ - - ]
67 : : // notify match?
68 [ - + ][ - + ]: 1082360 : Assert(n == expr::narySubstitute(mt->d_data, vars, subs));
[ - - ]
69 [ + - ]: 1082360 : Trace("match-debug") << "notify : " << mt->d_data << std::endl;
70 [ + + ]: 1082360 : if (!ntm->notify(n, mt->d_data, vars, subs))
71 : : {
72 : 250202 : return false;
73 : : }
74 : 832155 : visit.pop_back();
75 : 832155 : continue;
76 : : }
77 : :
78 : : // clean up if we previously bound a variable
79 [ + + ]: 18151700 : if (curr.d_boundVar)
80 : : {
81 [ - + ][ - + ]: 4638520 : Assert(!vars.empty());
[ - - ]
82 [ - + ][ - + ]: 4638520 : Assert(smap.find(vars.back()) != smap.end());
[ - - ]
83 : 4638520 : smap.erase(vars.back());
84 : 4638520 : vars.pop_back();
85 : 4638520 : subs.pop_back();
86 : 4638520 : curr.d_boundVar = false;
87 : : }
88 : :
89 [ + + ]: 18151700 : if (curr.d_index == 0)
90 : : {
91 : 6978780 : curr.d_index++;
92 : : // finished matching variables, try to match the operator
93 : 13957600 : Node next = syms.back();
94 : : Node op =
95 [ + + ][ + + ]: 13957600 : (!next.isNull() && next.hasOperator()) ? next.getOperator() : next;
96 : 6978780 : itc = mt->d_children.find(op);
97 [ + + ]: 6978780 : if (itc != mt->d_children.end())
98 : : {
99 : 1902090 : syms.pop_back();
100 : : // push the children + null termination marker, in reverse order
101 [ + + ]: 1902090 : if (NodeManager::isNAryKind(next.getKind()))
102 : : {
103 : 244423 : syms.push_back(Node::null());
104 : : }
105 [ + + ]: 1902090 : if (next.hasOperator())
106 : : {
107 : 1581640 : syms.insert(syms.end(), next.rbegin(), next.rend());
108 : : }
109 : : // new frame
110 : 1902090 : visit.push_back(NaryMatchFrame(syms, &itc->second));
111 : : }
112 : : }
113 [ + + ]: 11172900 : else if (curr.d_index <= mt->d_vars.size())
114 : : {
115 : : // try to match the next (variable, length)
116 : 6423380 : Node var;
117 : 6423380 : Node next;
118 : 2351080 : do
119 : : {
120 : 8774460 : var = mt->d_vars[curr.d_index - 1];
121 [ - + ][ - + ]: 8774460 : Assert(mt->d_children.find(var) != mt->d_children.end());
[ - - ]
122 : 17548900 : std::vector<Node> currChildren;
123 [ + + ]: 8774460 : if (isListVar(var))
124 : : {
125 : : // get the length of the list we want to consider
126 : 2739120 : size_t l = curr.d_variant;
127 : 2739120 : curr.d_variant++;
128 : : // match with l, or increment d_index otherwise
129 : 2739120 : 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 [ + + ]: 68668500 : for (size_t i = 0; i < l; i++)
135 : : {
136 [ - + ][ - + ]: 66347500 : Assert(!syms.empty());
[ - - ]
137 : 66347500 : 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 : 66347500 : if (s.isNull() || !s.getType().isComparableTo(var.getType()))
146 : : {
147 : 418161 : foundChildren = false;
148 : 418161 : break;
149 : : }
150 : 65929300 : currChildren.push_back(s);
151 : 65929300 : syms.pop_back();
152 : : }
153 [ + + ]: 2739120 : if (foundChildren)
154 : : {
155 : : // we are matching the next list
156 : 2320960 : next = nm->mkNode(Kind::SEXPR, currChildren);
157 : : }
158 : : else
159 : : {
160 : : // otherwise, we have run out of variants, go to next variable
161 : 418161 : curr.d_index++;
162 : 418161 : curr.d_variant = 0;
163 : : }
164 : : }
165 : : else
166 : : {
167 : 6035330 : next = syms.back();
168 : 6035330 : curr.d_index++;
169 : : // we could be at the end of an n-ary operator, in which case we
170 : : // do not match
171 [ + + ]: 6035330 : if (!next.isNull())
172 : : {
173 : 5885960 : currChildren.push_back(next);
174 : 5885960 : syms.pop_back();
175 [ + - ]: 11771900 : Trace("match-debug")
176 : 0 : << "Compare types " << var << " " << next << " "
177 : 5885960 : << var.getType() << " " << next.getType() << std::endl;
178 : : // check types in the (non-list) case
179 [ + + ]: 5885960 : if (!var.getType().isComparableTo(next.getType()))
180 : : {
181 [ + - ]: 2116920 : Trace("match-debug") << "...fail" << std::endl;
182 : 2116920 : next = Node::null();
183 : : }
184 : : }
185 : : }
186 [ + + ]: 8774460 : if (!next.isNull())
187 : : {
188 : : // check if it is already bound, do the binding if necessary
189 : 6090000 : std::map<Node, Node>::iterator its = smap.find(var);
190 [ + + ]: 6090000 : if (its != smap.end())
191 : : {
192 [ + + ]: 917489 : if (its->second != next)
193 : : {
194 : : // failed to match
195 : 877958 : next = Node::null();
196 : : }
197 : : // otherwise, successfully matched, nothing to do
198 : : }
199 : : else
200 : : {
201 : : // add to binding
202 [ + - ]: 10345000 : Trace("match-debug")
203 : 5172520 : << "Set " << var << " -> " << next << std::endl;
204 : 5172520 : vars.push_back(var);
205 : 5172520 : subs.push_back(next);
206 : 5172520 : smap[var] = next;
207 : 5172520 : curr.d_boundVar = true;
208 : : }
209 : : }
210 [ + + ]: 8774460 : if (next.isNull())
211 : : {
212 : : // if we failed, revert changes to syms
213 : 3562410 : syms.insert(syms.end(), currChildren.rbegin(), currChildren.rend());
214 : : }
215 [ + + ][ + + ]: 8774460 : } while (next.isNull() && curr.d_index <= mt->d_vars.size());
[ + + ]
216 [ + + ]: 6423380 : if (next.isNull())
217 : : {
218 : : // we are out of variables to match, finished with this frame
219 : 1211330 : visit.pop_back();
220 : 1211330 : continue;
221 : : }
222 [ + - ]: 5212050 : Trace("match-debug") << "recurse var : " << var << std::endl;
223 : 5212050 : itc = mt->d_children.find(var);
224 [ - + ][ - + ]: 5212050 : Assert(itc != mt->d_children.end());
[ - - ]
225 : 5212050 : visit.push_back(NaryMatchFrame(syms, &itc->second));
226 : : }
227 : : else
228 : : {
229 : : // no variables to match, we are done
230 : 4749540 : visit.pop_back();
231 : : }
232 : : }
233 : 696796 : return true;
234 : : }
235 : :
236 : 3005660 : void NaryMatchTrie::addTerm(Node n)
237 : : {
238 [ - + ][ - + ]: 3005660 : Assert(!n.isNull());
[ - - ]
239 : 6011310 : std::vector<Node> visit;
240 : 3005660 : visit.push_back(n);
241 : 3005660 : NaryMatchTrie* curr = this;
242 [ + + ]: 19122100 : while (!visit.empty())
243 : : {
244 : 32232800 : Node cn = visit.back();
245 : 16116400 : visit.pop_back();
246 [ + + ]: 16116400 : if (cn.isNull())
247 : : {
248 : 1273920 : curr = &(curr->d_children[cn]);
249 : : }
250 [ + + ]: 14842500 : else if (cn.hasOperator())
251 : : {
252 : 5493780 : curr = &(curr->d_children[cn.getOperator()]);
253 : : // add null terminator if an n-ary kind
254 [ + + ]: 5493780 : if (NodeManager::isNAryKind(cn.getKind()))
255 : : {
256 : 1273920 : visit.push_back(Node::null());
257 : : }
258 : : // note children are processed left to right
259 : 5493780 : visit.insert(visit.end(), cn.rbegin(), cn.rend());
260 : : }
261 : : else
262 : : {
263 : 9348720 : if (cn.isVar()
264 [ + + ][ + + ]: 26958000 : && std::find(curr->d_vars.begin(), curr->d_vars.end(), cn)
265 [ + + ]: 26958000 : == curr->d_vars.end())
266 : : {
267 : 6090930 : curr->d_vars.push_back(cn);
268 : : }
269 : 9348720 : curr = &(curr->d_children[cn]);
270 : : }
271 : : }
272 : 3005660 : curr->d_data = n;
273 : 3005660 : }
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
|
