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 : : * Implementation of term utilities class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/term_util.h"
14 : :
15 : : #include "expr/array_store_all.h"
16 : : #include "expr/function_array_const.h"
17 : : #include "expr/node_algorithm.h"
18 : : #include "expr/sequence.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "theory/arith/arith_msum.h"
21 : : #include "theory/bv/theory_bv_utils.h"
22 : : #include "theory/quantifiers/term_database.h"
23 : : #include "theory/quantifiers/term_enumeration.h"
24 : : #include "theory/rewriter.h"
25 : : #include "theory/strings/word.h"
26 : : #include "util/bitvector.h"
27 : : #include "util/rational.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace quantifiers {
34 : :
35 : 6619 : size_t TermUtil::getVariableNum(Node q, Node v)
36 : : {
37 : 6619 : Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
38 [ - + ][ - + ]: 6619 : Assert(it != q[0].end());
[ - - ]
39 : 6619 : return it - q[0].begin();
40 : : }
41 : :
42 : 27405 : Node TermUtil::getRemoveQuantifiers2(Node n, std::map<Node, Node>& visited)
43 : : {
44 : 27405 : std::map<Node, Node>::iterator it = visited.find(n);
45 [ + + ]: 27405 : if (it != visited.end())
46 : : {
47 : 10070 : return it->second;
48 : : }
49 : : else
50 : : {
51 : 17335 : Node ret = n;
52 [ + + ]: 17335 : if (n.getKind() == Kind::FORALL)
53 : : {
54 : 1060 : ret = getRemoveQuantifiers2(n[1], visited);
55 : : }
56 [ + + ]: 16275 : else if (n.getNumChildren() > 0)
57 : : {
58 : 11504 : std::vector<Node> children;
59 : 11504 : bool childrenChanged = false;
60 [ + + ]: 36777 : for (unsigned i = 0; i < n.getNumChildren(); i++)
61 : : {
62 : 25273 : Node ni = getRemoveQuantifiers2(n[i], visited);
63 [ + + ][ + + ]: 25273 : childrenChanged = childrenChanged || ni != n[i];
[ + + ][ - - ]
64 : 25273 : children.push_back(ni);
65 : 25273 : }
66 [ + + ]: 11504 : if (childrenChanged)
67 : : {
68 [ - + ]: 12 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
69 : : {
70 : 0 : children.insert(children.begin(), n.getOperator());
71 : : }
72 : 12 : ret = n.getNodeManager()->mkNode(n.getKind(), children);
73 : : }
74 : 11504 : }
75 : 17335 : visited[n] = ret;
76 : 17335 : return ret;
77 : 17335 : }
78 : : }
79 : :
80 : 16894437 : Node TermUtil::getInstConstAttr(Node n)
81 : : {
82 [ + + ]: 16894437 : if (!n.hasAttribute(InstConstantAttribute()))
83 : : {
84 : 1133872 : Node q;
85 [ + + ]: 1133872 : if (n.isVar())
86 : : {
87 : : // If it is a purification variable, it may correspond to a term
88 : : // with instantiation constants in it. We get the unpurified form here
89 : : // to handle this case.
90 : 176250 : Node un = SkolemManager::getUnpurifiedForm(n);
91 [ + - ][ + + ]: 176250 : if (!un.isNull() && un != n)
[ + + ]
92 : : {
93 : 79490 : q = getInstConstAttr(un);
94 : : }
95 : 176250 : }
96 : : else
97 : : {
98 [ + + ]: 2151952 : for (const Node& nc : n)
99 : : {
100 : 1425426 : q = getInstConstAttr(nc);
101 [ + + ]: 1425426 : if (!q.isNull())
102 : : {
103 : 231096 : break;
104 : : }
105 [ + + ]: 1425426 : }
106 [ + + ]: 957622 : if (q.isNull())
107 : : {
108 [ + + ]: 726526 : if (n.hasOperator())
109 : : {
110 : 616480 : q = getInstConstAttr(n.getOperator());
111 : : }
112 : : }
113 : : }
114 : : InstConstantAttribute ica;
115 : 1133872 : n.setAttribute(ica, q);
116 : 1133872 : }
117 : 33788874 : return n.getAttribute(InstConstantAttribute());
118 : : }
119 : :
120 : 8271026 : bool TermUtil::hasInstConstAttr(Node n)
121 : : {
122 : 8271026 : return !getInstConstAttr(n).isNull();
123 : : }
124 : :
125 : : // remove quantifiers
126 : 1072 : Node TermUtil::getRemoveQuantifiers(Node n)
127 : : {
128 : 1072 : std::map<Node, Node> visited;
129 : 2144 : return getRemoveQuantifiers2(n, visited);
130 : 1072 : }
131 : :
132 : 271070 : void TermUtil::computeInstConstContainsForQuant(Node q,
133 : : Node n,
134 : : std::vector<Node>& vars)
135 : : {
136 : 271070 : std::unordered_set<Node> ics;
137 : 271070 : expr::getSubtermsKind(Kind::INST_CONSTANT, n, ics);
138 [ + + ]: 1030892 : for (const Node& v : ics)
139 : : {
140 [ + - ]: 759822 : if (v.getAttribute(InstConstantAttribute()) == q)
141 : : {
142 [ + + ]: 759822 : if (std::find(vars.begin(), vars.end(), v) == vars.end())
143 : : {
144 : 759820 : vars.push_back(v);
145 : : }
146 : : }
147 : : }
148 : 271070 : }
149 : :
150 : 0 : int TermUtil::getTermDepth(Node n)
151 : : {
152 [ - - ]: 0 : if (!n.hasAttribute(TermDepthAttribute()))
153 : : {
154 : 0 : int maxDepth = -1;
155 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
156 : : {
157 : 0 : int depth = getTermDepth(n[i]);
158 [ - - ]: 0 : if (depth > maxDepth)
159 : : {
160 : 0 : maxDepth = depth;
161 : : }
162 : : }
163 : : TermDepthAttribute tda;
164 : 0 : n.setAttribute(tda, 1 + maxDepth);
165 : : }
166 : 0 : return n.getAttribute(TermDepthAttribute());
167 : : }
168 : :
169 : 3078242 : bool TermUtil::containsUninterpretedConstant(Node n)
170 : : {
171 [ + + ]: 3078242 : if (n.hasAttribute(ContainsUConstAttribute()))
172 : : {
173 : 3036025 : return n.getAttribute(ContainsUConstAttribute()) != 0;
174 : : }
175 : 42217 : bool ret = false;
176 : 42217 : Kind k = n.getKind();
177 [ + + ]: 42217 : if (k == Kind::UNINTERPRETED_SORT_VALUE)
178 : : {
179 [ - + ][ - + ]: 1463 : Assert(n.getType().isUninterpretedSort());
[ - - ]
180 : 1463 : ret = true;
181 : : }
182 [ + + ]: 40754 : else if (k == Kind::STORE_ALL)
183 : : {
184 : 14 : ret = containsUninterpretedConstant(n.getConst<ArrayStoreAll>().getValue());
185 : : }
186 [ + + ]: 40740 : else if (k == Kind::FUNCTION_ARRAY_CONST)
187 : : {
188 : 6 : ret = containsUninterpretedConstant(
189 : 6 : n.getConst<FunctionArrayConst>().getArrayValue());
190 : : }
191 [ + + ]: 40734 : else if (k == Kind::CONST_SEQUENCE)
192 : : {
193 : 6 : const std::vector<Node>& charVec = n.getConst<Sequence>().getVec();
194 [ - + ]: 6 : for (const Node& nc : charVec)
195 : : {
196 [ - - ]: 0 : if (containsUninterpretedConstant(nc))
197 : : {
198 : 0 : ret = true;
199 : 0 : break;
200 : : }
201 : : }
202 : : }
203 : : else
204 : : {
205 [ + + ]: 75302 : for (const Node& nc : n)
206 : : {
207 [ - + ]: 34574 : if (containsUninterpretedConstant(nc))
208 : : {
209 : 0 : ret = true;
210 : 0 : break;
211 : : }
212 [ + - ]: 34574 : }
213 : : }
214 : : ContainsUConstAttribute cuca;
215 [ + + ]: 42217 : n.setAttribute(cuca, ret ? 1 : 0);
216 : 42217 : return ret;
217 : : }
218 : :
219 : 12900 : Node TermUtil::simpleNegate(Node n)
220 : : {
221 [ - + ][ - + ]: 12900 : Assert(n.getType().isBoolean());
[ - - ]
222 : 12900 : NodeManager* nm = n.getNodeManager();
223 [ + + ][ + + ]: 12900 : if (n.getKind() == Kind::OR || n.getKind() == Kind::AND)
[ + + ]
224 : : {
225 : 2607 : std::vector<Node> children;
226 [ + + ]: 10206 : for (const Node& cn : n)
227 : : {
228 : 7599 : children.push_back(simpleNegate(cn));
229 : 7599 : }
230 [ + + ]: 2607 : return nm->mkNode(n.getKind() == Kind::OR ? Kind::AND : Kind::OR, children);
231 : 2607 : }
232 [ + + ]: 10293 : else if (n.isConst())
233 : : {
234 : 6320 : return nm->mkConst(!n.getConst<bool>());
235 : : }
236 : 7133 : return n.negate();
237 : : }
238 : :
239 : 7899 : Node TermUtil::mkNegate(Kind notk, Node n)
240 : : {
241 [ + + ]: 7899 : if (n.getKind() == notk)
242 : : {
243 : 612 : return n[0];
244 : : }
245 : 7287 : return NodeManager::mkNode(notk, n);
246 : : }
247 : :
248 : 16678 : bool TermUtil::isNegate(Kind k)
249 : : {
250 [ + + ][ + + ]: 15993 : return k == Kind::NOT || k == Kind::BITVECTOR_NOT || k == Kind::BITVECTOR_NEG
251 [ + + ][ - + ]: 32671 : || k == Kind::NEG;
252 : : }
253 : :
254 : 263774 : bool TermUtil::isAssoc(Kind k, bool reqNAry)
255 : : {
256 [ + + ]: 263774 : if (reqNAry)
257 : : {
258 [ + + ][ + + ]: 262865 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
259 : : {
260 : 98 : return false;
261 : : }
262 : : }
263 [ + + ][ + + ]: 244898 : return k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT
264 [ + + ][ + + ]: 239339 : || k == Kind::AND || k == Kind::OR || k == Kind::XOR
[ + + ]
265 [ + + ][ + + ]: 161242 : || k == Kind::BITVECTOR_ADD || k == Kind::BITVECTOR_MULT
266 [ + + ][ + + ]: 152446 : || k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR
267 [ + + ][ + - ]: 142465 : || k == Kind::BITVECTOR_XOR || k == Kind::BITVECTOR_XNOR
268 [ + + ][ + + ]: 142293 : || k == Kind::BITVECTOR_CONCAT || k == Kind::STRING_CONCAT
269 [ + + ][ + + ]: 138942 : || k == Kind::SET_UNION || k == Kind::SET_INTER
270 [ + - ][ + - ]: 138934 : || k == Kind::RELATION_JOIN || k == Kind::RELATION_TABLE_JOIN
271 [ + + ][ + - ]: 508574 : || k == Kind::RELATION_PRODUCT || k == Kind::SEP_STAR;
[ - + ]
272 : : }
273 : :
274 : 853920 : bool TermUtil::isComm(Kind k, bool reqNAry)
275 : : {
276 [ - + ]: 853920 : if (reqNAry)
277 : : {
278 [ - - ][ - - ]: 0 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
279 : : {
280 : 0 : return false;
281 : : }
282 : : }
283 [ + + ][ + + ]: 728324 : return k == Kind::EQUAL || k == Kind::ADD || k == Kind::MULT
284 [ + + ][ + + ]: 652359 : || k == Kind::NONLINEAR_MULT || k == Kind::AND || k == Kind::OR
[ + + ]
285 [ + + ][ + + ]: 524003 : || k == Kind::XOR || k == Kind::BITVECTOR_ADD
286 [ + + ][ + + ]: 519588 : || k == Kind::BITVECTOR_MULT || k == Kind::BITVECTOR_AND
287 [ + + ][ + + ]: 509396 : || k == Kind::BITVECTOR_OR || k == Kind::BITVECTOR_XOR
288 [ + - ][ + + ]: 503602 : || k == Kind::BITVECTOR_XNOR || k == Kind::SET_UNION
289 [ + + ][ + + ]: 1582244 : || k == Kind::SET_INTER || k == Kind::SEP_STAR;
[ + + ]
290 : : }
291 : :
292 : 263135 : bool TermUtil::isNonAdditive(Kind k)
293 : : {
294 [ + + ][ + + ]: 221216 : return k == Kind::AND || k == Kind::OR || k == Kind::BITVECTOR_AND
295 [ + + ][ + + ]: 484351 : || k == Kind::BITVECTOR_OR;
296 : : }
297 : :
298 : 720710 : bool TermUtil::isBoolConnective(Kind k)
299 : : {
300 [ + + ][ + + ]: 624450 : return k == Kind::OR || k == Kind::AND || k == Kind::EQUAL || k == Kind::ITE
[ + + ]
301 [ + + ][ + + ]: 1345160 : || k == Kind::FORALL || k == Kind::NOT || k == Kind::SEP_STAR;
[ + + ][ + + ]
302 : : }
303 : :
304 : 613907 : bool TermUtil::isBoolConnectiveTerm(TNode n)
305 : : {
306 : 613907 : return isBoolConnective(n.getKind())
307 : 1041348 : && (n.getKind() != Kind::EQUAL || n[0].getType().isBoolean())
308 [ + + ][ + + ]: 2269162 : && (n.getKind() != Kind::ITE || n.getType().isBoolean());
[ + + ][ + + ]
[ + + ][ - - ]
309 : : }
310 : :
311 : 85892 : Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
312 : : {
313 : 85892 : Node n;
314 [ + + ]: 85892 : if (tn.isRealOrInt())
315 : : {
316 : 6530 : Rational c(val);
317 : 6530 : n = tn.getNodeManager()->mkConstRealOrInt(tn, c);
318 : 6530 : }
319 [ + + ]: 79362 : else if (tn.isBitVector())
320 : : {
321 : : // cast to unsigned
322 : 802 : uint32_t uv = static_cast<uint32_t>(val);
323 : 802 : BitVector bval(tn.getConst<BitVectorSize>(), uv);
324 : 802 : n = tn.getNodeManager()->mkConst<BitVector>(bval);
325 : 802 : }
326 [ + + ]: 78560 : else if (tn.isBoolean())
327 : : {
328 [ + + ]: 78078 : if (val == 0)
329 : : {
330 : 77516 : n = tn.getNodeManager()->mkConst(false);
331 : : }
332 : : }
333 [ + + ]: 482 : else if (tn.isStringLike())
334 : : {
335 [ + + ]: 386 : if (val == 0)
336 : : {
337 : 208 : n = strings::Word::mkEmptyWord(tn);
338 : : }
339 : : }
340 : 85892 : return n;
341 : 0 : }
342 : :
343 : 79504 : Node TermUtil::mkTypeMaxValue(TypeNode tn)
344 : : {
345 : 79504 : Node n;
346 : 79504 : NodeManager* nm = tn.getNodeManager();
347 [ + + ]: 79504 : if (tn.isBitVector())
348 : : {
349 : 142 : n = bv::utils::mkOnes(nm, tn.getConst<BitVectorSize>());
350 : : }
351 [ + + ]: 79362 : else if (tn.isBoolean())
352 : : {
353 : 77220 : n = nm->mkConst(true);
354 : : }
355 : 79504 : return n;
356 : 0 : }
357 : :
358 : 8 : Node TermUtil::mkTypeValueOffset(TypeNode tn,
359 : : Node val,
360 : : int32_t offset,
361 : : int32_t& status)
362 : : {
363 : 8 : Assert(val.isConst() && val.getType() == tn);
364 : 8 : Node val_o;
365 : 8 : status = -1;
366 [ + - ]: 8 : if (tn.isRealOrInt())
367 : : {
368 : 8 : Rational vval = val.getConst<Rational>();
369 : 8 : Rational oval(offset);
370 : 8 : status = 0;
371 : 16 : return NodeManager::mkConstRealOrInt(tn, vval + oval);
372 : 8 : }
373 [ - - ]: 0 : else if (tn.isBitVector())
374 : : {
375 : 0 : BitVector vval = val.getConst<BitVector>();
376 : 0 : uint32_t uv = static_cast<uint32_t>(offset);
377 : 0 : BitVector oval(tn.getConst<BitVectorSize>(), uv);
378 : 0 : return tn.getNodeManager()->mkConst(vval + oval);
379 : 0 : }
380 : 0 : return val_o;
381 : 8 : }
382 : :
383 : 0 : Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
384 : : {
385 : 0 : return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
386 : : }
387 : :
388 : 0 : bool TermUtil::isAntisymmetric(Kind k, Kind& dk)
389 : : {
390 [ - - ]: 0 : if (k == Kind::GT)
391 : : {
392 : 0 : dk = Kind::LT;
393 : 0 : return true;
394 : : }
395 [ - - ]: 0 : else if (k == Kind::GEQ)
396 : : {
397 : 0 : dk = Kind::LEQ;
398 : 0 : return true;
399 : : }
400 [ - - ]: 0 : else if (k == Kind::BITVECTOR_UGT)
401 : : {
402 : 0 : dk = Kind::BITVECTOR_ULT;
403 : 0 : return true;
404 : : }
405 [ - - ]: 0 : else if (k == Kind::BITVECTOR_UGE)
406 : : {
407 : 0 : dk = Kind::BITVECTOR_ULE;
408 : 0 : return true;
409 : : }
410 [ - - ]: 0 : else if (k == Kind::BITVECTOR_SGT)
411 : : {
412 : 0 : dk = Kind::BITVECTOR_SLT;
413 : 0 : return true;
414 : : }
415 [ - - ]: 0 : else if (k == Kind::BITVECTOR_SGE)
416 : : {
417 : 0 : dk = Kind::BITVECTOR_SLE;
418 : 0 : return true;
419 : : }
420 : 0 : return false;
421 : : }
422 : :
423 : 1966 : bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
424 : : {
425 : : // these should all be binary operators
426 : : // Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
427 : : // ik!=BITVECTOR_UDIV );
428 : 1966 : TypeNode tn = n.getType();
429 [ + + ]: 1966 : if (n == mkTypeValue(tn, 0))
430 : : {
431 [ + + ][ + + ]: 774 : if (ik == Kind::ADD || ik == Kind::OR || ik == Kind::XOR
[ + - ]
432 [ + + ][ + + ]: 622 : || ik == Kind::BITVECTOR_ADD || ik == Kind::BITVECTOR_OR
433 [ + + ][ + + ]: 598 : || ik == Kind::BITVECTOR_XOR || ik == Kind::STRING_CONCAT)
434 : : {
435 : 202 : return true;
436 : : }
437 [ + + ][ + - ]: 572 : else if (ik == Kind::SUB || ik == Kind::BITVECTOR_SHL
438 [ + + ][ + + ]: 472 : || ik == Kind::BITVECTOR_LSHR || ik == Kind::BITVECTOR_ASHR
439 [ + + ][ + + ]: 464 : || ik == Kind::BITVECTOR_SUB || ik == Kind::BITVECTOR_UREM)
440 : : {
441 : 116 : return arg == 1;
442 : : }
443 : : }
444 [ + + ]: 1192 : else if (n == mkTypeValue(tn, 1))
445 : : {
446 [ + + ][ - + ]: 556 : if (ik == Kind::MULT || ik == Kind::BITVECTOR_MULT)
447 : : {
448 : 10 : return true;
449 : : }
450 [ + + ][ + - ]: 546 : else if (ik == Kind::DIVISION || ik == Kind::DIVISION_TOTAL
451 [ + - ][ + - ]: 538 : || ik == Kind::INTS_DIVISION || ik == Kind::INTS_DIVISION_TOTAL
452 [ + - ][ + - ]: 538 : || ik == Kind::INTS_MODULUS || ik == Kind::INTS_MODULUS_TOTAL
453 [ + + ][ + + ]: 538 : || ik == Kind::BITVECTOR_UDIV || ik == Kind::BITVECTOR_SDIV)
454 : : {
455 : 20 : return arg == 1;
456 : : }
457 : : }
458 [ + + ]: 636 : else if (n == mkTypeMaxValue(tn))
459 : : {
460 [ + - ][ + - ]: 174 : if (ik == Kind::EQUAL || ik == Kind::BITVECTOR_AND
461 [ - + ]: 174 : || ik == Kind::BITVECTOR_XNOR)
462 : : {
463 : 0 : return true;
464 : : }
465 : : }
466 : 1618 : return false;
467 : 1966 : }
468 : :
469 : 1686 : Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
470 : : {
471 : 1686 : TypeNode tn = n.getType();
472 [ + + ]: 1686 : if (n == mkTypeValue(tn, 0))
473 : : {
474 [ + + ][ + + ]: 514 : if (ik == Kind::AND || ik == Kind::MULT || ik == Kind::BITVECTOR_AND
[ + + ]
475 [ - + ]: 450 : || ik == Kind::BITVECTOR_MULT)
476 : : {
477 : 64 : return n;
478 : : }
479 [ + - ][ + + ]: 450 : else if (ik == Kind::BITVECTOR_SHL || ik == Kind::BITVECTOR_LSHR
480 [ + + ][ + + ]: 448 : || ik == Kind::BITVECTOR_ASHR || ik == Kind::BITVECTOR_UREM)
481 : : {
482 [ + - ]: 6 : if (arg == 0)
483 : : {
484 : 6 : return n;
485 : : }
486 : : }
487 [ + + ][ - + ]: 444 : else if (ik == Kind::BITVECTOR_UDIV || ik == Kind::BITVECTOR_SDIV)
488 : : {
489 [ + + ]: 8 : if (arg == 0)
490 : : {
491 : 4 : return n;
492 : : }
493 [ + - ]: 4 : else if (arg == 1)
494 : : {
495 : 4 : return mkTypeMaxValue(tn);
496 : : }
497 : : }
498 [ + + ][ + - ]: 436 : else if (ik == Kind::DIVISION || ik == Kind::DIVISION_TOTAL
499 [ + - ][ + - ]: 432 : || ik == Kind::INTS_DIVISION || ik == Kind::INTS_DIVISION_TOTAL
500 [ + + ][ - + ]: 432 : || ik == Kind::INTS_MODULUS || ik == Kind::INTS_MODULUS_TOTAL)
501 : : {
502 [ + + ]: 10 : if (arg == 0)
503 : : {
504 : 6 : return n;
505 : : }
506 : : }
507 [ - + ]: 426 : else if (ik == Kind::STRING_SUBSTR)
508 : : {
509 [ - - ]: 0 : if (arg == 0)
510 : : {
511 : 0 : return n;
512 : : }
513 [ - - ]: 0 : else if (arg == 2)
514 : : {
515 : 0 : return mkTypeValue(n.getNodeManager()->stringType(), 0);
516 : : }
517 : : }
518 [ - + ]: 426 : else if (ik == Kind::STRING_INDEXOF)
519 : : {
520 [ - - ][ - - ]: 0 : if (arg == 0 || arg == 1)
521 : : {
522 : 0 : return mkTypeValue(n.getNodeManager()->integerType(), -1);
523 : : }
524 : : }
525 : : }
526 [ + + ]: 1172 : else if (n == mkTypeValue(tn, 1))
527 : : {
528 [ + + ]: 536 : if (ik == Kind::BITVECTOR_UREM)
529 : : {
530 : 4 : return mkTypeValue(tn, 0);
531 : : }
532 : : }
533 [ + + ]: 636 : else if (n == mkTypeMaxValue(tn))
534 : : {
535 [ + + ][ - + ]: 174 : if (ik == Kind::OR || ik == Kind::BITVECTOR_OR)
536 : : {
537 : 44 : return n;
538 : : }
539 : : }
540 : : else
541 : : {
542 [ + + ][ - + ]: 462 : if (n.getType().isInteger() && n.getConst<Rational>().sgn() < 0)
[ + - ][ - + ]
[ - - ]
543 : : {
544 : : // negative arguments
545 [ - - ][ - - ]: 0 : if (ik == Kind::STRING_SUBSTR || ik == Kind::STRING_CHARAT)
546 : : {
547 : 0 : return mkTypeValue(n.getNodeManager()->stringType(), 0);
548 : : }
549 [ - - ]: 0 : else if (ik == Kind::STRING_INDEXOF)
550 : : {
551 : 0 : Assert(arg == 2);
552 : 0 : return mkTypeValue(n.getNodeManager()->integerType(), -1);
553 : : }
554 : : }
555 : : }
556 : 1554 : return Node::null();
557 : 1686 : }
558 : :
559 : 1072 : bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
560 : : {
561 [ + + ]: 1072 : if (ik == Kind::LT)
562 : : {
563 [ + + ][ + - ]: 8 : Assert(arg == 0 || arg == 1);
[ - + ][ - + ]
[ - - ]
564 [ + + ]: 8 : offset = arg == 0 ? 1 : -1;
565 : 8 : ok = Kind::LEQ;
566 : 8 : return true;
567 : : }
568 [ - + ]: 1064 : else if (ik == Kind::BITVECTOR_ULT)
569 : : {
570 : 0 : Assert(arg == 0 || arg == 1);
571 [ - - ]: 0 : offset = arg == 0 ? 1 : -1;
572 : 0 : ok = Kind::BITVECTOR_ULE;
573 : 0 : return true;
574 : : }
575 [ - + ]: 1064 : else if (ik == Kind::BITVECTOR_SLT)
576 : : {
577 : 0 : Assert(arg == 0 || arg == 1);
578 [ - - ]: 0 : offset = arg == 0 ? 1 : -1;
579 : 0 : ok = Kind::BITVECTOR_SLE;
580 : 0 : return true;
581 : : }
582 : 1064 : return false;
583 : : }
584 : :
585 : 369 : Node TermUtil::ensureType(Node n, TypeNode tn)
586 : : {
587 : 369 : TypeNode ntn = n.getType();
588 [ + + ]: 369 : if (ntn == tn)
589 : : {
590 : 360 : return n;
591 : : }
592 [ - + ]: 9 : if (tn.isInteger())
593 : : {
594 : 0 : return NodeManager::mkNode(Kind::TO_INTEGER, n);
595 : : }
596 [ + - ]: 9 : else if (tn.isReal())
597 : : {
598 : 9 : return NodeManager::mkNode(Kind::TO_REAL, n);
599 : : }
600 : 0 : return Node::null();
601 : 369 : }
602 : :
603 : : } // namespace quantifiers
604 : : } // namespace theory
605 : : } // namespace cvc5::internal
|
