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 : : * N-ary term utilities
11 : : */
12 : :
13 : : #include "expr/nary_term_util.h"
14 : :
15 : : #include "expr/aci_norm.h"
16 : : #include "expr/attribute.h"
17 : : #include "expr/emptyset.h"
18 : : #include "expr/node_algorithm.h"
19 : : #include "expr/sort_to_term.h"
20 : : #include "theory/bv/theory_bv_utils.h"
21 : : #include "theory/strings/word.h"
22 : : #include "util/bitvector.h"
23 : : #include "util/finite_field_value.h"
24 : : #include "util/rational.h"
25 : : #include "util/regexp.h"
26 : : #include "util/string.h"
27 : :
28 : : using namespace cvc5::internal::kind;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace expr {
32 : :
33 : : struct IsListTag
34 : : {
35 : : };
36 : : using IsListAttr = expr::Attribute<IsListTag, bool>;
37 : :
38 : 2142306 : void markListVar(TNode fv)
39 : : {
40 [ - + ][ - + ]: 2142306 : Assert(fv.isVar());
[ - - ]
41 : 2142306 : fv.setAttribute(IsListAttr(), true);
42 : 2142306 : }
43 : :
44 : 123056635 : bool isListVar(TNode fv) { return fv.getAttribute(IsListAttr()); }
45 : :
46 : 2 : bool hasListVar(TNode n)
47 : : {
48 : 2 : std::unordered_set<TNode> visited;
49 : 2 : std::unordered_set<TNode>::iterator it;
50 : 2 : std::vector<TNode> visit;
51 : 2 : TNode cur;
52 : 2 : visit.push_back(n);
53 : : do
54 : : {
55 : 12 : cur = visit.back();
56 : 12 : visit.pop_back();
57 : 12 : it = visited.find(cur);
58 : :
59 [ + + ]: 12 : if (it == visited.end())
60 : : {
61 : 9 : visited.insert(cur);
62 [ - + ]: 9 : if (isListVar(cur))
63 : : {
64 : 0 : return true;
65 : : }
66 : 9 : visit.insert(visit.end(), cur.begin(), cur.end());
67 : : }
68 [ + + ]: 12 : } while (!visit.empty());
69 : 2 : return false;
70 : 2 : }
71 : :
72 : 5530790 : bool getListVarContext(TNode n, std::map<Node, Node>& context)
73 : : {
74 : 5530790 : std::unordered_set<TNode> visited;
75 : 5530790 : std::unordered_set<TNode>::iterator it;
76 : 5530790 : std::map<Node, Node>::iterator itc;
77 : 5530790 : std::vector<TNode> visit;
78 : 5530790 : TNode cur;
79 : 5530790 : visit.push_back(n);
80 : : do
81 : : {
82 : 45877553 : cur = visit.back();
83 : 45877553 : visit.pop_back();
84 : 45877553 : it = visited.find(cur);
85 [ + + ]: 45877553 : if (it == visited.end())
86 : : {
87 : 38253464 : visited.insert(cur);
88 [ - + ]: 38253464 : if (isListVar(cur))
89 : : {
90 : : // top-level list variable, undefined
91 : 0 : return false;
92 : : }
93 [ + + ]: 80462493 : for (const Node& cn : cur)
94 : : {
95 [ + + ]: 42209029 : if (isListVar(cn))
96 : : {
97 : 1862266 : itc = context.find(cn);
98 [ + + ]: 1862266 : if (itc == context.end())
99 : : {
100 [ - + ]: 1071153 : if (!NodeManager::isNAryKind(cur.getKind()))
101 : : {
102 : 0 : return false;
103 : : }
104 : 1071153 : context[cn] = cur;
105 : : }
106 [ - + ]: 791113 : else if (itc->second.getKind() != cur.getKind())
107 : : {
108 : 0 : return false;
109 : : }
110 : 1862266 : continue;
111 : : }
112 : 40346763 : visit.push_back(cn);
113 [ + - ][ + ]: 42209029 : }
114 : : }
115 [ + + ]: 45877553 : } while (!visit.empty());
116 : 5530790 : return true;
117 : 5530790 : }
118 : :
119 : 3370901 : Node narySubstitute(Node src,
120 : : const std::vector<Node>& vars,
121 : : const std::vector<Node>& subs)
122 : : {
123 : 3370901 : std::unordered_map<TNode, Node> visited;
124 : 6741802 : return narySubstitute(src, vars, subs, visited);
125 : 3370901 : }
126 : :
127 : 3589913 : Node narySubstitute(Node src,
128 : : const std::vector<Node>& vars,
129 : : const std::vector<Node>& subs,
130 : : std::unordered_map<TNode, Node>& visited)
131 : : {
132 : : // assumes all variables are list variables
133 : 3589913 : NodeManager* nm = src.getNodeManager();
134 : 3589913 : std::unordered_map<TNode, Node>::iterator it;
135 : 3589913 : std::vector<TNode> visit;
136 : 3589913 : std::vector<Node>::const_iterator itv;
137 : 3589913 : TNode cur;
138 : 3589913 : visit.push_back(src);
139 : : do
140 : : {
141 : 37287670 : cur = visit.back();
142 : 37287670 : it = visited.find(cur);
143 [ + + ]: 37287670 : if (it == visited.end())
144 : : {
145 [ + + ]: 18026668 : if (!expr::hasBoundVar(cur))
146 : : {
147 : 1424677 : visited[cur] = cur;
148 : 1424677 : visit.pop_back();
149 : 1424677 : continue;
150 : : }
151 : : // if it is a non-list variable, do the replacement
152 : 16601991 : itv = std::find(vars.begin(), vars.end(), cur);
153 [ + + ]: 16601991 : if (itv != vars.end())
154 : : {
155 : 7036539 : size_t d = std::distance(vars.begin(), itv);
156 [ + + ]: 7036539 : if (!isListVar(vars[d]))
157 : : {
158 : 6408331 : visited[cur] = subs[d];
159 : 6408331 : continue;
160 : : }
161 : : }
162 : 10193660 : visited[cur] = Node::null();
163 : 10193660 : visit.insert(visit.end(), cur.begin(), cur.end());
164 : 10193660 : continue;
165 : 10193660 : }
166 : 19261002 : visit.pop_back();
167 [ + + ]: 19261002 : if (it->second.isNull())
168 : : {
169 : 10193504 : Node ret = cur;
170 : 10193504 : bool childChanged = false;
171 : 10193504 : std::vector<Node> children;
172 [ + + ]: 27289270 : for (const Node& cn : cur)
173 : : {
174 : : // if it is a list variable, insert the corresponding list as children;
175 : 17095766 : itv = std::find(vars.begin(), vars.end(), cn);
176 [ + + ]: 17095766 : if (itv != vars.end())
177 : : {
178 : 8381716 : childChanged = true;
179 : 8381716 : size_t d = std::distance(vars.begin(), itv);
180 [ - + ][ - + ]: 8381716 : Assert(d < subs.size());
[ - - ]
181 : 8381716 : Node sd = subs[d];
182 [ + + ]: 8381716 : if (isListVar(vars[d]))
183 : : {
184 [ - + ][ - + ]: 731265 : Assert(sd.getKind() == Kind::SEXPR);
[ - - ]
185 : : // add its children
186 : 731265 : children.insert(children.end(), sd.begin(), sd.end());
187 : : }
188 : : else
189 : : {
190 : 7650451 : children.push_back(sd);
191 : : }
192 : 8381716 : continue;
193 : 8381716 : }
194 : 8714050 : it = visited.find(cn);
195 [ - + ][ - + ]: 8714050 : Assert(it != visited.end());
[ - - ]
196 [ - + ][ - + ]: 8714050 : Assert(!it->second.isNull());
[ - - ]
197 [ + + ][ + + ]: 8714050 : childChanged = childChanged || cn != it->second;
198 : 8714050 : children.push_back(it->second);
199 [ + + ]: 17095766 : }
200 [ + + ]: 10193504 : if (childChanged)
201 : : {
202 [ + + ]: 7561826 : if (children.size() != cur.getNumChildren())
203 : : {
204 : : // n-ary operators cannot be parameterized
205 [ - + ][ - + ]: 502885 : Assert(cur.getMetaKind() != metakind::PARAMETERIZED);
[ - - ]
206 [ + + ]: 502885 : if (children.empty())
207 : : {
208 : 184 : ret = getNullTerminator(nm, cur.getKind(), cur.getType());
209 : : // if we don't know the null terminator, just return null now
210 [ + - ]: 184 : if (ret.isNull())
211 : : {
212 : 184 : return ret;
213 : : }
214 : : }
215 : : else
216 : : {
217 [ + + ]: 1005402 : ret = (children.size() == 1 ? children[0]
218 : 502701 : : nm->mkNode(cur.getKind(), children));
219 : : }
220 : : }
221 : : else
222 : : {
223 [ + + ]: 7058941 : if (cur.getMetaKind() == metakind::PARAMETERIZED)
224 : : {
225 : 110778 : children.insert(children.begin(), cur.getOperator());
226 : : }
227 : 7058941 : Kind k = cur.getKind();
228 : : // We treat @set.empty_of_type, @seq.empty_of_type, @type_of as
229 : : // macros in this method, meaning they are immediately evaluated
230 : : // as soon as RARE rules are instantiated.
231 [ + + ][ + ]: 7058941 : switch (k)
232 : : {
233 : 22010 : case Kind::SET_EMPTY_OF_TYPE:
234 : : case Kind::SEQ_EMPTY_OF_TYPE:
235 : : {
236 [ + - ]: 22010 : if (children[0].getKind() == Kind::SORT_TO_TERM)
237 : : {
238 : 22010 : const SortToTerm& st = children[0].getConst<SortToTerm>();
239 : 22010 : TypeNode tn = st.getType();
240 [ + + ]: 22010 : if (k == Kind::SET_EMPTY_OF_TYPE)
241 : : {
242 : 2358 : ret = nm->mkConst(EmptySet(tn));
243 : : }
244 : : else
245 : : {
246 [ - + ][ - + ]: 19652 : Assert(k == Kind::SEQ_EMPTY_OF_TYPE);
[ - - ]
247 : 19652 : ret = theory::strings::Word::mkEmptyWord(tn);
248 : : }
249 : 22010 : }
250 : : else
251 : : {
252 : 0 : ret = nm->mkNode(k, children);
253 : : }
254 : : }
255 : 22010 : break;
256 : 22010 : case Kind::TYPE_OF:
257 : 22010 : ret = nm->mkConst(SortToTerm(children[0].getType()));
258 : 22010 : break;
259 : 7014921 : default: ret = nm->mkNode(k, children); break;
260 : : }
261 : : }
262 : : }
263 : 10193320 : visited[cur] = ret;
264 [ + + ][ + + ]: 10193688 : }
265 : :
266 [ + + ]: 37287486 : } while (!visit.empty());
267 [ - + ][ - + ]: 3589729 : Assert(visited.find(src) != visited.end());
[ - - ]
268 [ - + ][ - + ]: 3589729 : Assert(!visited.find(src)->second.isNull());
[ - - ]
269 : 3589729 : return visited[src];
270 : 3589913 : }
271 : :
272 : : } // namespace expr
273 : : } // namespace cvc5::internal
|
