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