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