Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mudathir Mohamed
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 : : * A class for representing abstract types.
14 : : */
15 : :
16 : : #include "theory/builtin/generic_op.h"
17 : :
18 : : #include <iostream>
19 : :
20 : : #include "expr/dtype.h"
21 : : #include "expr/dtype_cons.h"
22 : : #include "theory/evaluator.h"
23 : : #include "theory/datatypes/project_op.h"
24 : : #include "theory/datatypes/theory_datatypes_utils.h"
25 : : #include "util/bitvector.h"
26 : : #include "util/floatingpoint.h"
27 : : #include "util/iand.h"
28 : : #include "util/rational.h"
29 : : #include "util/regexp.h"
30 : :
31 : : using namespace cvc5::internal::kind;
32 : :
33 : : namespace cvc5::internal {
34 : :
35 : 0 : std::ostream& operator<<(std::ostream& out, const GenericOp& op)
36 : : {
37 : 0 : return out << "(GenericOp " << op.getKind() << ')';
38 : : }
39 : :
40 : 624831 : size_t GenericOpHashFunction::operator()(const GenericOp& op) const
41 : : {
42 : 624831 : return kind::KindHashFunction()(op.getKind());
43 : : }
44 : :
45 : 519863 : GenericOp::GenericOp(Kind k) : d_kind(k) {}
46 : :
47 : 26246 : GenericOp::GenericOp(const GenericOp& op) : d_kind(op.getKind()) {}
48 : :
49 : 2478410 : Kind GenericOp::getKind() const { return d_kind; }
50 : :
51 : 546093 : bool GenericOp::operator==(const GenericOp& op) const
52 : : {
53 : 546093 : return getKind() == op.getKind();
54 : : }
55 : :
56 : 5580240 : bool GenericOp::isNumeralIndexedOperatorKind(Kind k)
57 : : {
58 [ + + ]: 5566570 : return k == Kind::REGEXP_LOOP || k == Kind::BITVECTOR_EXTRACT
59 [ + + ][ + + ]: 4595450 : || k == Kind::BITVECTOR_REPEAT || k == Kind::BITVECTOR_ZERO_EXTEND
60 [ + + ][ + + ]: 4400730 : || k == Kind::BITVECTOR_SIGN_EXTEND || k == Kind::BITVECTOR_ROTATE_LEFT
61 [ + + ][ + + ]: 4151440 : || k == Kind::BITVECTOR_ROTATE_RIGHT || k == Kind::INT_TO_BITVECTOR
62 [ + + ][ + + ]: 4069610 : || k == Kind::BITVECTOR_BIT || k == Kind::IAND
63 [ + + ]: 4033020 : || k == Kind::FLOATINGPOINT_TO_FP_FROM_FP
64 [ + - ]: 4033010 : || k == Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV
65 [ + + ]: 4033010 : || k == Kind::FLOATINGPOINT_TO_FP_FROM_SBV
66 [ + + ]: 4032950 : || k == Kind::FLOATINGPOINT_TO_FP_FROM_REAL
67 [ + + ]: 4032910 : || k == Kind::FLOATINGPOINT_TO_FP_FROM_UBV
68 [ + - ][ + - ]: 4032580 : || k == Kind::FLOATINGPOINT_TO_SBV || k == Kind::FLOATINGPOINT_TO_UBV
69 [ + - ]: 4032580 : || k == Kind::FLOATINGPOINT_TO_SBV_TOTAL
70 [ + - ]: 4032580 : || k == Kind::FLOATINGPOINT_TO_UBV_TOTAL
71 [ + - ][ + - ]: 4032580 : || k == Kind::RELATION_AGGREGATE || k == Kind::RELATION_PROJECT
72 [ + + ][ + - ]: 4032580 : || k == Kind::RELATION_GROUP || k == Kind::TABLE_PROJECT
73 [ + - ][ + - ]: 4032580 : || k == Kind::RELATION_TABLE_JOIN || k == Kind::TABLE_AGGREGATE
74 [ + + ][ + - ]: 11146800 : || k == Kind::TABLE_JOIN || k == Kind::TABLE_GROUP;
[ + + ]
75 : : }
76 : :
77 : 4712410 : bool GenericOp::isIndexedOperatorKind(Kind k)
78 : : {
79 [ + + ]: 8628760 : return isNumeralIndexedOperatorKind(k) || k == Kind::APPLY_UPDATER
80 [ + + ][ + + ]: 8628760 : || k == Kind::APPLY_TESTER;
81 : : }
82 : :
83 : 54287 : std::vector<Node> GenericOp::getIndicesForOperator(Kind k, Node n)
84 : : {
85 : 54287 : NodeManager* nm = NodeManager::currentNM();
86 : 54287 : std::vector<Node> indices;
87 [ + + ][ + + ]: 54287 : switch (k)
[ + + ][ + + ]
[ + + ][ + - ]
[ + + ][ + - ]
[ - - ][ - + ]
[ + + ][ - ]
88 : : {
89 : 30 : case Kind::REGEXP_LOOP:
90 : : {
91 : 30 : const RegExpLoop& op = n.getConst<RegExpLoop>();
92 : 30 : indices.push_back(nm->mkConstInt(Rational(op.d_loopMinOcc)));
93 : 30 : indices.push_back(nm->mkConstInt(Rational(op.d_loopMaxOcc)));
94 : 30 : break;
95 : : }
96 : 14531 : case Kind::BITVECTOR_EXTRACT:
97 : : {
98 : 14531 : const BitVectorExtract& p = n.getConst<BitVectorExtract>();
99 : 14531 : indices.push_back(nm->mkConstInt(Rational(p.d_high)));
100 : 14531 : indices.push_back(nm->mkConstInt(Rational(p.d_low)));
101 : 14531 : break;
102 : : }
103 : 493 : case Kind::BITVECTOR_REPEAT:
104 : 493 : indices.push_back(nm->mkConstInt(
105 : 986 : Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
106 : 493 : break;
107 : 8934 : case Kind::BITVECTOR_ZERO_EXTEND:
108 : 8934 : indices.push_back(nm->mkConstInt(
109 : 17868 : Rational(n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount)));
110 : 8934 : break;
111 : 9045 : case Kind::BITVECTOR_SIGN_EXTEND:
112 : 9045 : indices.push_back(nm->mkConstInt(
113 : 18090 : Rational(n.getConst<BitVectorSignExtend>().d_signExtendAmount)));
114 : 9045 : break;
115 : 497 : case Kind::BITVECTOR_ROTATE_LEFT:
116 : 497 : indices.push_back(nm->mkConstInt(
117 : 994 : Rational(n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount)));
118 : 497 : break;
119 : 827 : case Kind::BITVECTOR_ROTATE_RIGHT:
120 : 827 : indices.push_back(nm->mkConstInt(
121 : 1654 : Rational(n.getConst<BitVectorRotateRight>().d_rotateRightAmount)));
122 : 827 : break;
123 : 18201 : case Kind::BITVECTOR_BIT:
124 : 18201 : indices.push_back(
125 : 36402 : nm->mkConstInt(Rational(n.getConst<BitVectorBit>().d_bitIndex)));
126 : 18201 : break;
127 : 209 : case Kind::INT_TO_BITVECTOR:
128 : 209 : indices.push_back(
129 : 418 : nm->mkConstInt(Rational(n.getConst<IntToBitVector>().d_size)));
130 : 209 : break;
131 : 109 : case Kind::IAND:
132 : 109 : indices.push_back(nm->mkConstInt(Rational(n.getConst<IntAnd>().d_size)));
133 : 109 : break;
134 : 4 : case Kind::FLOATINGPOINT_TO_FP_FROM_FP:
135 : : {
136 : : const FloatingPointToFPFloatingPoint& ffp =
137 : 4 : n.getConst<FloatingPointToFPFloatingPoint>();
138 : 4 : indices.push_back(nm->mkConstInt(ffp.getSize().exponentWidth()));
139 : 4 : indices.push_back(nm->mkConstInt(ffp.getSize().significandWidth()));
140 : : }
141 : 4 : break;
142 : 0 : case Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
143 : : {
144 : : const FloatingPointToFPIEEEBitVector& fbv =
145 : 0 : n.getConst<FloatingPointToFPIEEEBitVector>();
146 : 0 : indices.push_back(nm->mkConstInt(fbv.getSize().exponentWidth()));
147 : 0 : indices.push_back(nm->mkConstInt(fbv.getSize().significandWidth()));
148 : : }
149 : 0 : break;
150 : 16 : case Kind::FLOATINGPOINT_TO_FP_FROM_SBV:
151 : : {
152 : : const FloatingPointToFPSignedBitVector& fsbv =
153 : 16 : n.getConst<FloatingPointToFPSignedBitVector>();
154 : 16 : indices.push_back(nm->mkConstInt(fsbv.getSize().exponentWidth()));
155 : 16 : indices.push_back(nm->mkConstInt(fsbv.getSize().significandWidth()));
156 : : }
157 : 16 : break;
158 : 80 : case Kind::FLOATINGPOINT_TO_FP_FROM_UBV:
159 : : {
160 : : const FloatingPointToFPUnsignedBitVector& fubv =
161 : 80 : n.getConst<FloatingPointToFPUnsignedBitVector>();
162 : 80 : indices.push_back(nm->mkConstInt(fubv.getSize().exponentWidth()));
163 : 80 : indices.push_back(nm->mkConstInt(fubv.getSize().significandWidth()));
164 : : }
165 : 80 : break;
166 : 11 : case Kind::FLOATINGPOINT_TO_FP_FROM_REAL:
167 : : {
168 : 11 : const FloatingPointToFPReal& fr = n.getConst<FloatingPointToFPReal>();
169 : 11 : indices.push_back(nm->mkConstInt(fr.getSize().exponentWidth()));
170 : 11 : indices.push_back(nm->mkConstInt(fr.getSize().significandWidth()));
171 : : }
172 : 11 : break;
173 : 0 : case Kind::FLOATINGPOINT_TO_SBV:
174 : : {
175 : 0 : const FloatingPointToSBV& fsbv = n.getConst<FloatingPointToSBV>();
176 : 0 : indices.push_back(nm->mkConstInt(Rational(fsbv)));
177 : : }
178 : 0 : break;
179 : 0 : case Kind::FLOATINGPOINT_TO_UBV:
180 : : {
181 : 0 : const FloatingPointToUBV& fubv = n.getConst<FloatingPointToUBV>();
182 : 0 : indices.push_back(nm->mkConstInt(Rational(fubv)));
183 : : }
184 : 0 : break;
185 : 0 : case Kind::FLOATINGPOINT_TO_SBV_TOTAL:
186 : : {
187 : : const FloatingPointToSBVTotal& fsbv =
188 : 0 : n.getConst<FloatingPointToSBVTotal>();
189 : 0 : indices.push_back(nm->mkConstInt(Rational(fsbv)));
190 : : }
191 : 0 : break;
192 : 0 : case Kind::FLOATINGPOINT_TO_UBV_TOTAL:
193 : : {
194 : : const FloatingPointToUBVTotal& fubv =
195 : 0 : n.getConst<FloatingPointToUBVTotal>();
196 : 0 : indices.push_back(nm->mkConstInt(Rational(fubv)));
197 : : }
198 : 0 : break;
199 : 10 : case Kind::RELATION_AGGREGATE:
200 : : case Kind::RELATION_PROJECT:
201 : : case Kind::RELATION_TABLE_JOIN:
202 : : case Kind::RELATION_GROUP:
203 : : case Kind::TABLE_PROJECT:
204 : : case Kind::TABLE_AGGREGATE:
205 : : case Kind::TABLE_JOIN:
206 : : case Kind::TABLE_GROUP:
207 : : {
208 : 10 : const ProjectOp& p = n.getConst<ProjectOp>();
209 : 10 : const std::vector<uint32_t>& pi = p.getIndices();
210 [ + + ]: 30 : for (uint32_t i : pi)
211 : : {
212 : 20 : indices.push_back(nm->mkConstInt(Rational(i)));
213 : : }
214 : : }
215 : 10 : break;
216 : 1264 : case Kind::APPLY_TESTER:
217 : : {
218 : 1264 : unsigned index = DType::indexOf(n);
219 : 1264 : const DType& dt = DType::datatypeOf(n);
220 : 1264 : indices.push_back(dt[index].getConstructor());
221 : : }
222 : 1264 : break;
223 : 26 : case Kind::APPLY_UPDATER:
224 : : {
225 : 26 : unsigned index = DType::indexOf(n);
226 : 26 : const DType& dt = DType::datatypeOf(n);
227 : 26 : unsigned cindex = DType::cindexOf(n);
228 : 26 : indices.push_back(dt[cindex][index].getSelector());
229 : : }
230 : 26 : break;
231 : 0 : default:
232 : 0 : Unhandled() << "GenericOp::getOperatorIndices: unhandled kind " << k;
233 : : break;
234 : : }
235 : 54287 : return indices;
236 : : }
237 : :
238 : : /** Converts a list of constant integer terms to a list of unsigned integers */
239 : 731699 : bool convertToNumeralList(const std::vector<Node>& indices,
240 : : std::vector<uint32_t>& numerals)
241 : : {
242 [ + + ]: 779720 : for (const Node& i : indices)
243 : : {
244 : 738950 : Node in = i;
245 [ + + ]: 738950 : if (in.getKind() != Kind::CONST_INTEGER)
246 : : {
247 : : // If trivially evaluatable, take that as the numeral.
248 : : // This implies that we can concretize applications of
249 : : // APPLY_INDEXED_SYMBOLIC whose indices can evaluate. This in turn
250 : : // implies that e.g. (extract (+ 2 2) 2 x) concretizes via getConcreteApp
251 : : // to ((_ extract 4 2) x), which implies it has type (BitVec 3) based
252 : : // on the type rule for APPLY_INDEXED_SYMBOLIC.
253 : 690731 : theory::Evaluator e(nullptr);
254 : 690731 : in = e.eval(in, {}, {});
255 [ - + ][ - - ]: 690731 : if (in.isNull() || in.getKind() != Kind::CONST_INTEGER)
[ + - ]
256 : : {
257 : 690731 : return false;
258 : : }
259 : : }
260 : 48219 : const Integer& ii = in.getConst<Rational>().getNumerator();
261 [ + + ]: 48219 : if (!ii.fitsUnsignedInt())
262 : : {
263 : 198 : return false;
264 : : }
265 : 48021 : numerals.push_back(ii.toUnsignedInt());
266 : : }
267 : 40770 : return true;
268 : : }
269 : :
270 : 731699 : Node GenericOp::getOperatorForIndices(NodeManager* nm,
271 : : Kind k,
272 : : const std::vector<Node>& indices)
273 : : {
274 : : // all indices should be constant!
275 [ - + ][ - + ]: 731699 : Assert(isIndexedOperatorKind(k));
[ - - ]
276 [ + - ]: 731699 : if (isNumeralIndexedOperatorKind(k))
277 : : {
278 : 731699 : std::vector<uint32_t> numerals;
279 [ + + ]: 731699 : if (!convertToNumeralList(indices, numerals))
280 : : {
281 : : // failed to convert due to non-constant, or overflow on index
282 : 690929 : return Node::null();
283 : : }
284 [ + + ][ + + ]: 40770 : switch (k)
[ + + ][ + - ]
[ + + ][ + - ]
[ + + ][ + - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ + - ]
285 : : {
286 : 6 : case Kind::REGEXP_LOOP:
287 [ - + ][ - + ]: 6 : Assert(numerals.size() == 2);
[ - - ]
288 : 12 : return nm->mkConst(RegExpLoop(numerals[0], numerals[1]));
289 : 7079 : case Kind::BITVECTOR_EXTRACT:
290 [ - + ][ - + ]: 7079 : Assert(numerals.size() == 2);
[ - - ]
291 : 14158 : return nm->mkConst(BitVectorExtract(numerals[0], numerals[1]));
292 : 306 : case Kind::BITVECTOR_REPEAT:
293 [ - + ][ - + ]: 306 : Assert(numerals.size() == 1);
[ - - ]
294 : 612 : return nm->mkConst(BitVectorRepeat(numerals[0]));
295 : 22756 : case Kind::BITVECTOR_ZERO_EXTEND:
296 [ - + ][ - + ]: 22756 : Assert(numerals.size() == 1);
[ - - ]
297 : 45512 : return nm->mkConst(BitVectorZeroExtend(numerals[0]));
298 : 8221 : case Kind::BITVECTOR_SIGN_EXTEND:
299 [ - + ][ - + ]: 8221 : Assert(numerals.size() == 1);
[ - - ]
300 : 16442 : return nm->mkConst(BitVectorSignExtend(numerals[0]));
301 : 169 : case Kind::BITVECTOR_ROTATE_LEFT:
302 [ - + ][ - + ]: 169 : Assert(numerals.size() == 1);
[ - - ]
303 : 338 : return nm->mkConst(BitVectorRotateLeft(numerals[0]));
304 : 226 : case Kind::BITVECTOR_ROTATE_RIGHT:
305 [ - + ][ - + ]: 226 : Assert(numerals.size() == 1);
[ - - ]
306 : 452 : return nm->mkConst(BitVectorRotateRight(numerals[0]));
307 : 0 : case Kind::BITVECTOR_BIT:
308 : 0 : Assert(numerals.size() == 1);
309 : 0 : return nm->mkConst(BitVectorBit(numerals[0]));
310 : 1815 : case Kind::INT_TO_BITVECTOR:
311 [ - + ][ - + ]: 1815 : Assert(numerals.size() == 1);
[ - - ]
312 : 3630 : return nm->mkConst(IntToBitVector(numerals[0]));
313 : 50 : case Kind::IAND:
314 [ - + ][ - + ]: 50 : Assert(numerals.size() == 1);
[ - - ]
315 : 100 : return nm->mkConst(IntAnd(numerals[0]));
316 : 4 : case Kind::FLOATINGPOINT_TO_FP_FROM_FP:
317 [ - + ][ - + ]: 4 : Assert(numerals.size() == 2);
[ - - ]
318 : : return nm->mkConst(
319 : 8 : FloatingPointToFPFloatingPoint(numerals[0], numerals[1]));
320 : 0 : case Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
321 : 0 : Assert(numerals.size() == 2);
322 : : return nm->mkConst(
323 : 0 : FloatingPointToFPIEEEBitVector(numerals[0], numerals[1]));
324 : 16 : case Kind::FLOATINGPOINT_TO_FP_FROM_SBV:
325 [ - + ][ - + ]: 16 : Assert(numerals.size() == 2);
[ - - ]
326 : : return nm->mkConst(
327 : 32 : FloatingPointToFPSignedBitVector(numerals[0], numerals[1]));
328 : 106 : case Kind::FLOATINGPOINT_TO_FP_FROM_UBV:
329 [ - + ][ - + ]: 106 : Assert(numerals.size() == 2);
[ - - ]
330 : : return nm->mkConst(
331 : 212 : FloatingPointToFPUnsignedBitVector(numerals[0], numerals[1]));
332 : 12 : case Kind::FLOATINGPOINT_TO_FP_FROM_REAL:
333 [ - + ][ - + ]: 12 : Assert(numerals.size() == 2);
[ - - ]
334 : 24 : return nm->mkConst(FloatingPointToFPReal(numerals[0], numerals[1]));
335 : 0 : case Kind::FLOATINGPOINT_TO_SBV:
336 : 0 : Assert(numerals.size() == 1);
337 : 0 : return nm->mkConst(FloatingPointToSBV(numerals[0]));
338 : 0 : case Kind::FLOATINGPOINT_TO_UBV:
339 : 0 : Assert(numerals.size() == 1);
340 : 0 : return nm->mkConst(FloatingPointToUBV(numerals[0]));
341 : 0 : case Kind::FLOATINGPOINT_TO_SBV_TOTAL:
342 : 0 : Assert(numerals.size() == 1);
343 : 0 : return nm->mkConst(FloatingPointToSBVTotal(numerals[0]));
344 : 0 : case Kind::FLOATINGPOINT_TO_UBV_TOTAL:
345 : 0 : Assert(numerals.size() == 1);
346 : 0 : return nm->mkConst(FloatingPointToUBVTotal(numerals[0]));
347 : 0 : case Kind::RELATION_AGGREGATE:
348 : 0 : return nm->mkConst(Kind::RELATION_AGGREGATE_OP, ProjectOp(numerals));
349 : 0 : case Kind::RELATION_PROJECT:
350 : 0 : return nm->mkConst(Kind::RELATION_PROJECT_OP, ProjectOp(numerals));
351 : 0 : case Kind::RELATION_TABLE_JOIN:
352 : 0 : return nm->mkConst(Kind::RELATION_TABLE_JOIN_OP, ProjectOp(numerals));
353 : 0 : case Kind::RELATION_GROUP:
354 : 0 : return nm->mkConst(Kind::RELATION_GROUP_OP, ProjectOp(numerals));
355 : 0 : case Kind::TABLE_PROJECT:
356 : 0 : return nm->mkConst(Kind::TABLE_PROJECT_OP, ProjectOp(numerals));
357 : 0 : case Kind::TABLE_AGGREGATE:
358 : 0 : return nm->mkConst(Kind::TABLE_AGGREGATE_OP, ProjectOp(numerals));
359 : 0 : case Kind::TABLE_JOIN: return nm->mkConst(Kind::TABLE_JOIN_OP, ProjectOp(numerals));
360 : 8 : case Kind::TABLE_GROUP: return nm->mkConst(Kind::TABLE_GROUP_OP, ProjectOp(numerals));
361 : 0 : default:
362 : 0 : Unhandled() << "GenericOp::getOperatorForIndices: unhandled kind " << k;
363 : : break;
364 : : }
365 : : }
366 : : else
367 : : {
368 [ - - ][ - ]: 0 : switch (k)
369 : : {
370 : 0 : case Kind::APPLY_TESTER:
371 : : {
372 : 0 : Assert(indices.size() == 1);
373 : 0 : unsigned index = DType::indexOf(indices[0]);
374 : 0 : const DType& dt = DType::datatypeOf(indices[0]);
375 : 0 : return dt[index].getTester();
376 : : }
377 : : break;
378 : 0 : case Kind::APPLY_UPDATER:
379 : : {
380 : 0 : Assert(indices.size() == 1);
381 : 0 : unsigned index = DType::indexOf(indices[0]);
382 : 0 : const DType& dt = DType::datatypeOf(indices[0]);
383 : 0 : unsigned cindex = DType::cindexOf(indices[0]);
384 : 0 : return dt[cindex][index].getUpdater();
385 : : }
386 : : break;
387 : 0 : default:
388 : 0 : Unhandled() << "GenericOp::getOperatorForIndices: unhandled kind" << k;
389 : : break;
390 : : }
391 : : }
392 : 0 : return Node::null();
393 : : }
394 : :
395 : 731699 : Node GenericOp::getConcreteApp(const Node& app)
396 : : {
397 [ + - ]: 731699 : Trace("generic-op") << "getConcreteApp " << app << std::endl;
398 [ - + ][ - + ]: 731699 : Assert(app.getKind() == Kind::APPLY_INDEXED_SYMBOLIC);
[ - - ]
399 : 731699 : Kind okind = app.getOperator().getConst<GenericOp>().getKind();
400 : : // determine how many arguments should be passed to the end function. This is
401 : : // usually one, but we handle cases where it is >1.
402 : 731699 : size_t nargs = metakind::getMinArityForKind(okind);
403 : 1463400 : std::vector<Node> indices(app.begin(), app.end() - nargs);
404 : 731699 : NodeManager* nm = NodeManager::currentNM();
405 : 1463400 : Node op = getOperatorForIndices(nm, okind, indices);
406 : : // could have a bad index, in which case we don't rewrite
407 [ + + ]: 731699 : if (op.isNull())
408 : : {
409 : 690929 : return app;
410 : : }
411 : 81540 : std::vector<Node> args;
412 : 40770 : args.push_back(op);
413 : 40770 : args.insert(args.end(), app.end() - nargs, app.end());
414 : 81540 : Node ret = nm->mkNode(okind, args);
415 : : // could be ill typed, in which case we don't rewrite
416 [ + + ]: 40770 : if (ret.getTypeOrNull(true).isNull())
417 : : {
418 : 944 : return app;
419 : : }
420 : 39826 : return ret;
421 : : }
422 : :
423 : : } // namespace cvc5::internal
|
