1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Implements a n-ary match trie
16 #include "expr/nary_match_trie.h"
19 #include "expr/nary_term_util.h"
21 using namespace cvc5::kind
;
29 NaryMatchFrame(const std::vector
<Node
>& syms
, const NaryMatchTrie
* t
)
30 : d_syms(syms
), d_trie(t
), d_index(0), d_variant(0), d_boundVar(false)
33 /** Symbols to match */
34 std::vector
<Node
> d_syms
;
36 const NaryMatchTrie
* d_trie
;
37 /** The index we are considering, 0 = operator, n>0 = variable # (n-1) */
39 /** List length considering */
41 /** Whether we just bound a variable */
45 bool NaryMatchTrie::getMatches(Node n
, NotifyMatch
* ntm
) const
47 NodeManager
* nm
= NodeManager::currentNM();
48 std::vector
<Node
> vars
;
49 std::vector
<Node
> subs
;
50 std::map
<Node
, Node
> smap
;
52 std::map
<Node
, NaryMatchTrie
>::const_iterator itc
;
54 std::vector
<NaryMatchFrame
> visit
;
55 visit
.push_back(NaryMatchFrame({n
}, this));
57 while (!visit
.empty())
59 NaryMatchFrame
& curr
= visit
.back();
60 // currently, copy the symbols from previous frame TODO: improve?
61 std::vector
<Node
> syms
= curr
.d_syms
;
62 const NaryMatchTrie
* mt
= curr
.d_trie
;
65 // if we matched, there must be a data member at this node
66 Assert(!mt
->d_data
.isNull());
68 Assert(n
== expr::narySubstitute(mt
->d_data
, vars
, subs
));
69 Trace("match-debug") << "notify : " << mt
->d_data
<< std::endl
;
70 if (!ntm
->notify(n
, mt
->d_data
, vars
, subs
))
78 // clean up if we previously bound a variable
81 Assert(!vars
.empty());
82 Assert(smap
.find(vars
.back()) != smap
.end());
83 smap
.erase(vars
.back());
86 curr
.d_boundVar
= false;
89 if (curr
.d_index
== 0)
92 // finished matching variables, try to match the operator
93 Node next
= syms
.back();
95 (!next
.isNull() && next
.hasOperator()) ? next
.getOperator() : next
;
96 itc
= mt
->d_children
.find(op
);
97 if (itc
!= mt
->d_children
.end())
100 // push the children + null termination marker, in reverse order
101 if (NodeManager::isNAryKind(next
.getKind()))
103 syms
.push_back(Node::null());
105 if (next
.hasOperator())
107 syms
.insert(syms
.end(), next
.rbegin(), next
.rend());
110 visit
.push_back(NaryMatchFrame(syms
, &itc
->second
));
113 else if (curr
.d_index
<= mt
->d_vars
.size())
115 // try to match the next (variable, length)
120 var
= mt
->d_vars
[curr
.d_index
- 1];
121 Assert(mt
->d_children
.find(var
) != mt
->d_children
.end());
122 std::vector
<Node
> currChildren
;
125 // get the length of the list we want to consider
126 size_t l
= curr
.d_variant
;
128 // match with l, or increment d_index otherwise
129 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 for (size_t i
= 0; i
< l
; i
++)
136 Assert(!syms
.empty());
137 Node s
= syms
.back();
140 foundChildren
= false;
143 currChildren
.push_back(s
);
148 // we are matching the next list
149 next
= nm
->mkNode(SEXPR
, currChildren
);
153 // otherwise, we have run out of variants, go to next variable
162 // we could be at the end of an n-ary operator, in which case we
166 currChildren
.push_back(next
);
168 // check subtyping in the (non-list) case
169 if (!var
.getType().isSubtypeOf(next
.getType()))
177 // check if it is already bound, do the binding if necessary
178 std::map
<Node
, Node
>::iterator its
= smap
.find(var
);
179 if (its
!= smap
.end())
181 if (its
->second
!= next
)
186 // otherwise, successfully matched, nothing to do
192 subs
.push_back(next
);
194 curr
.d_boundVar
= true;
199 // if we failed, revert changes to syms
200 syms
.insert(syms
.end(), currChildren
.rbegin(), currChildren
.rend());
202 } while (next
.isNull() && curr
.d_index
<= mt
->d_vars
.size());
205 // we are out of variables to match, finished with this frame
209 Trace("match-debug") << "recurse var : " << var
<< std::endl
;
210 itc
= mt
->d_children
.find(var
);
211 Assert(itc
!= mt
->d_children
.end());
212 visit
.push_back(NaryMatchFrame(syms
, &itc
->second
));
216 // no variables to match, we are done
223 void NaryMatchTrie::addTerm(Node n
)
226 std::vector
<Node
> visit
;
228 NaryMatchTrie
* curr
= this;
229 while (!visit
.empty())
231 Node cn
= visit
.back();
235 curr
= &(curr
->d_children
[cn
]);
237 else if (cn
.hasOperator())
239 curr
= &(curr
->d_children
[cn
.getOperator()]);
240 // add null terminator if an n-ary kind
241 if (NodeManager::isNAryKind(cn
.getKind()))
243 visit
.push_back(Node::null());
245 // note children are processed left to right
246 visit
.insert(visit
.end(), cn
.rbegin(), cn
.rend());
251 && std::find(curr
->d_vars
.begin(), curr
->d_vars
.end(), cn
)
252 == curr
->d_vars
.end())
254 curr
->d_vars
.push_back(cn
);
256 curr
= &(curr
->d_children
[cn
]);
262 void NaryMatchTrie::clear()
266 d_data
= Node::null();
269 std::string
NaryMatchTrie::debugPrint() const
271 std::stringstream ss
;
272 std::vector
<std::tuple
<const NaryMatchTrie
*, size_t, Node
>> visit
;
273 visit
.emplace_back(this, 0, Node::null());
276 std::tuple
<const NaryMatchTrie
*, size_t, Node
> curr
= visit
.back();
278 size_t indent
= std::get
<1>(curr
);
279 for (size_t i
= 0; i
< indent
; i
++)
283 Node n
= std::get
<2>(curr
);
292 ss
<< ((!n
.isNull() && isListVar(n
)) ? " [*]" : "");
294 const NaryMatchTrie
* mt
= std::get
<0>(curr
);
295 for (const std::pair
<const Node
, NaryMatchTrie
>& c
: mt
->d_children
)
297 visit
.emplace_back(&c
.second
, indent
+ 1, c
.first
);
299 } while (!visit
.empty());