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 : 6591 : size_t TermUtil::getVariableNum(Node q, Node v)
36 : : {
37 : 6591 : Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
38 [ - + ][ - + ]: 6591 : Assert(it != q[0].end());
[ - - ]
39 : 6591 : return it - q[0].begin();
40 : : }
41 : :
42 : 27405 : Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
43 : 27405 : std::map< Node, Node >::iterator it = visited.find( n );
44 [ + + ]: 27405 : if( it!=visited.end() ){
45 : 10070 : return it->second;
46 : : }else{
47 : 17335 : Node ret = n;
48 [ + + ]: 17335 : if (n.getKind() == Kind::FORALL)
49 : : {
50 : 1060 : ret = getRemoveQuantifiers2( n[1], visited );
51 : : }
52 [ + + ]: 16275 : else if (n.getNumChildren() > 0)
53 : : {
54 : 11504 : std::vector< Node > children;
55 : 11504 : bool childrenChanged = false;
56 [ + + ]: 36777 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
57 : 25273 : Node ni = getRemoveQuantifiers2( n[i], visited );
58 [ + + ][ + + ]: 25273 : childrenChanged = childrenChanged || ni!=n[i];
[ + + ][ - - ]
59 : 25273 : children.push_back( ni );
60 : 25273 : }
61 [ + + ]: 11504 : if( childrenChanged ){
62 [ - + ]: 12 : if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
63 : 0 : children.insert( children.begin(), n.getOperator() );
64 : : }
65 : 12 : ret = n.getNodeManager()->mkNode(n.getKind(), children);
66 : : }
67 : 11504 : }
68 : 17335 : visited[n] = ret;
69 : 17335 : return ret;
70 : 17335 : }
71 : : }
72 : :
73 : 13931654 : Node TermUtil::getInstConstAttr( Node n ) {
74 [ + + ]: 13931654 : if (!n.hasAttribute(InstConstantAttribute()))
75 : : {
76 : 1109184 : Node q;
77 [ + + ]: 1109184 : if (n.isVar())
78 : : {
79 : : // If it is a purification variable, it may correspond to a term
80 : : // with instantiation constants in it. We get the unpurified form here
81 : : // to handle this case.
82 : 173115 : Node un = SkolemManager::getUnpurifiedForm(n);
83 [ + - ][ + + ]: 173115 : if (!un.isNull() && un != n)
[ + + ]
84 : : {
85 : 76658 : q = getInstConstAttr(un);
86 : : }
87 : 173115 : }
88 : : else
89 : : {
90 [ + + ]: 2088883 : for (const Node& nc : n)
91 : : {
92 : 1383655 : q = getInstConstAttr(nc);
93 [ + + ]: 1383655 : if (!q.isNull())
94 : : {
95 : 230841 : break;
96 : : }
97 [ + + ]: 1383655 : }
98 [ + + ]: 936069 : if (q.isNull())
99 : : {
100 [ + + ]: 705228 : if (n.hasOperator())
101 : : {
102 : 596342 : q = getInstConstAttr(n.getOperator());
103 : : }
104 : : }
105 : : }
106 : : InstConstantAttribute ica;
107 : 1109184 : n.setAttribute(ica, q);
108 : 1109184 : }
109 : 27863308 : return n.getAttribute(InstConstantAttribute());
110 : : }
111 : :
112 : 7923183 : bool TermUtil::hasInstConstAttr(Node n)
113 : : {
114 : 7923183 : return !getInstConstAttr(n).isNull();
115 : : }
116 : :
117 : : //remove quantifiers
118 : 1072 : Node TermUtil::getRemoveQuantifiers( Node n ) {
119 : 1072 : std::map< Node, Node > visited;
120 : 2144 : return getRemoveQuantifiers2( n, visited );
121 : 1072 : }
122 : :
123 : 271769 : void TermUtil::computeInstConstContainsForQuant(Node q,
124 : : Node n,
125 : : std::vector<Node>& vars)
126 : : {
127 : 271769 : std::unordered_set<Node> ics;
128 : 271769 : expr::getSubtermsKind(Kind::INST_CONSTANT, n, ics);
129 [ + + ]: 1034301 : for (const Node& v : ics)
130 : : {
131 [ + - ]: 762532 : if (v.getAttribute(InstConstantAttribute()) == q)
132 : : {
133 [ + + ]: 762532 : if (std::find(vars.begin(), vars.end(), v) == vars.end())
134 : : {
135 : 762530 : vars.push_back(v);
136 : : }
137 : : }
138 : : }
139 : 271769 : }
140 : :
141 : 0 : int TermUtil::getTermDepth( Node n ) {
142 [ - - ]: 0 : if (!n.hasAttribute(TermDepthAttribute()) ){
143 : 0 : int maxDepth = -1;
144 [ - - ]: 0 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
145 : 0 : int depth = getTermDepth( n[i] );
146 [ - - ]: 0 : if( depth>maxDepth ){
147 : 0 : maxDepth = depth;
148 : : }
149 : : }
150 : : TermDepthAttribute tda;
151 : 0 : n.setAttribute(tda,1+maxDepth);
152 : : }
153 : 0 : return n.getAttribute(TermDepthAttribute());
154 : : }
155 : :
156 : 509516 : bool TermUtil::containsUninterpretedConstant( Node n ) {
157 [ + + ]: 509516 : if (n.hasAttribute(ContainsUConstAttribute()))
158 : : {
159 : 468886 : return n.getAttribute(ContainsUConstAttribute()) != 0;
160 : : }
161 : 40630 : bool ret = false;
162 : 40630 : Kind k = n.getKind();
163 [ + + ]: 40630 : if (k == Kind::UNINTERPRETED_SORT_VALUE)
164 : : {
165 [ - + ][ - + ]: 1431 : Assert(n.getType().isUninterpretedSort());
[ - - ]
166 : 1431 : ret = true;
167 : : }
168 [ + + ]: 39199 : else if (k == Kind::STORE_ALL)
169 : : {
170 : 8 : ret = containsUninterpretedConstant(n.getConst<ArrayStoreAll>().getValue());
171 : : }
172 [ - + ]: 39191 : else if (k == Kind::FUNCTION_ARRAY_CONST)
173 : : {
174 : 0 : ret = containsUninterpretedConstant(
175 : 0 : n.getConst<FunctionArrayConst>().getArrayValue());
176 : : }
177 [ + + ]: 39191 : else if (k == Kind::CONST_SEQUENCE)
178 : : {
179 : 6 : const std::vector<Node>& charVec = n.getConst<Sequence>().getVec();
180 [ - + ]: 6 : for (const Node& nc : charVec)
181 : : {
182 [ - - ]: 0 : if (containsUninterpretedConstant(nc))
183 : : {
184 : 0 : ret = true;
185 : 0 : break;
186 : : }
187 : : }
188 : : }
189 : : else
190 : : {
191 [ + + ]: 71342 : for (const Node& nc : n)
192 : : {
193 [ - + ]: 32157 : if (containsUninterpretedConstant(nc))
194 : : {
195 : 0 : ret = true;
196 : 0 : break;
197 : : }
198 [ + - ]: 32157 : }
199 : : }
200 : : ContainsUConstAttribute cuca;
201 [ + + ]: 40630 : n.setAttribute(cuca, ret ? 1 : 0);
202 : 40630 : return ret;
203 : : }
204 : :
205 : 15366 : Node TermUtil::simpleNegate(Node n)
206 : : {
207 [ - + ][ - + ]: 15366 : Assert(n.getType().isBoolean());
[ - - ]
208 : 15366 : NodeManager* nm = n.getNodeManager();
209 [ + + ][ + + ]: 15366 : if (n.getKind() == Kind::OR || n.getKind() == Kind::AND)
[ + + ]
210 : : {
211 : 3569 : std::vector< Node > children;
212 [ + + ]: 13366 : for (const Node& cn : n)
213 : : {
214 : 9797 : children.push_back(simpleNegate(cn));
215 : 9797 : }
216 [ + + ]: 3569 : return nm->mkNode(n.getKind() == Kind::OR ? Kind::AND : Kind::OR, children);
217 : 3569 : }
218 [ + + ]: 11797 : else if (n.isConst())
219 : : {
220 : 6320 : return nm->mkConst(!n.getConst<bool>());
221 : : }
222 : 8637 : return n.negate();
223 : : }
224 : :
225 : 6927 : Node TermUtil::mkNegate(Kind notk, Node n)
226 : : {
227 [ + + ]: 6927 : if (n.getKind() == notk)
228 : : {
229 : 592 : return n[0];
230 : : }
231 : 6335 : return NodeManager::mkNode(notk, n);
232 : : }
233 : :
234 : 16340 : bool TermUtil::isNegate(Kind k)
235 : : {
236 [ + + ][ + + ]: 15705 : return k == Kind::NOT || k == Kind::BITVECTOR_NOT || k == Kind::BITVECTOR_NEG
237 [ + + ][ - + ]: 32045 : || k == Kind::NEG;
238 : : }
239 : :
240 : 255438 : bool TermUtil::isAssoc(Kind k, bool reqNAry)
241 : : {
242 [ + + ]: 255438 : if (reqNAry)
243 : : {
244 [ + + ][ + + ]: 254525 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
245 : : {
246 : 62 : return false;
247 : : }
248 : : }
249 [ + + ][ + + ]: 236606 : return k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT
250 [ + + ][ + + ]: 231061 : || k == Kind::AND || k == Kind::OR || k == Kind::XOR
[ + + ]
251 [ + + ][ + + ]: 154373 : || k == Kind::BITVECTOR_ADD || k == Kind::BITVECTOR_MULT
252 [ + + ][ + + ]: 145721 : || k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR
253 [ + + ][ + - ]: 135788 : || k == Kind::BITVECTOR_XOR || k == Kind::BITVECTOR_XNOR
254 [ + + ][ + + ]: 135640 : || k == Kind::BITVECTOR_CONCAT || k == Kind::STRING_CONCAT
255 [ + + ][ + + ]: 132303 : || k == Kind::SET_UNION || k == Kind::SET_INTER
256 [ + - ][ + - ]: 132295 : || k == Kind::RELATION_JOIN || k == Kind::RELATION_TABLE_JOIN
257 [ + + ][ + - ]: 491982 : || k == Kind::RELATION_PRODUCT || k == Kind::SEP_STAR;
[ - + ]
258 : : }
259 : :
260 : 839366 : bool TermUtil::isComm(Kind k, bool reqNAry)
261 : : {
262 [ - + ]: 839366 : if (reqNAry)
263 : : {
264 [ - - ][ - - ]: 0 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
265 : : {
266 : 0 : return false;
267 : : }
268 : : }
269 [ + + ][ + + ]: 716063 : return k == Kind::EQUAL || k == Kind::ADD || k == Kind::MULT
270 [ + + ][ + + ]: 643756 : || k == Kind::NONLINEAR_MULT || k == Kind::AND || k == Kind::OR
[ + + ]
271 [ + + ][ + + ]: 517681 : || k == Kind::XOR || k == Kind::BITVECTOR_ADD
272 [ + + ][ + + ]: 513379 : || k == Kind::BITVECTOR_MULT || k == Kind::BITVECTOR_AND
273 [ + + ][ + + ]: 503241 : || k == Kind::BITVECTOR_OR || k == Kind::BITVECTOR_XOR
274 [ + - ][ + + ]: 497495 : || k == Kind::BITVECTOR_XNOR || k == Kind::SET_UNION
275 [ + + ][ + + ]: 1555429 : || k == Kind::SET_INTER || k == Kind::SEP_STAR;
[ + + ]
276 : : }
277 : :
278 : 254797 : bool TermUtil::isNonAdditive( Kind k ) {
279 [ + + ][ + + ]: 213585 : return k == Kind::AND || k == Kind::OR || k == Kind::BITVECTOR_AND
280 [ + + ][ + + ]: 468382 : || k == Kind::BITVECTOR_OR;
281 : : }
282 : :
283 : 715102 : bool TermUtil::isBoolConnective( Kind k ) {
284 [ + + ][ + + ]: 619839 : return k == Kind::OR || k == Kind::AND || k == Kind::EQUAL || k == Kind::ITE
[ + + ]
285 [ + + ][ + + ]: 1334941 : || k == Kind::FORALL || k == Kind::NOT || k == Kind::SEP_STAR;
[ + + ][ + + ]
286 : : }
287 : :
288 : 610194 : bool TermUtil::isBoolConnectiveTerm( TNode n ) {
289 : 610194 : return isBoolConnective(n.getKind())
290 : 1035383 : && (n.getKind() != Kind::EQUAL || n[0].getType().isBoolean())
291 [ + + ][ + + ]: 2255771 : && (n.getKind() != Kind::ITE || n.getType().isBoolean());
[ + + ][ + + ]
[ + + ][ - - ]
292 : : }
293 : :
294 : 84529 : Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
295 : : {
296 : 84529 : Node n;
297 [ + + ]: 84529 : if (tn.isRealOrInt())
298 : : {
299 : 6550 : Rational c(val);
300 : 6550 : n = tn.getNodeManager()->mkConstRealOrInt(tn, c);
301 : 6550 : }
302 [ + + ]: 77979 : else if (tn.isBitVector())
303 : : {
304 : : // cast to unsigned
305 : 802 : uint32_t uv = static_cast<uint32_t>(val);
306 : 802 : BitVector bval(tn.getConst<BitVectorSize>(), uv);
307 : 802 : n = tn.getNodeManager()->mkConst<BitVector>(bval);
308 : 802 : }
309 [ + + ]: 77177 : else if (tn.isBoolean())
310 : : {
311 [ + + ]: 76671 : if (val == 0)
312 : : {
313 : 76109 : n = tn.getNodeManager()->mkConst(false);
314 : : }
315 : : }
316 [ + + ]: 506 : else if (tn.isStringLike())
317 : : {
318 [ + + ]: 386 : if (val == 0)
319 : : {
320 : 208 : n = strings::Word::mkEmptyWord(tn);
321 : : }
322 : : }
323 : 84529 : return n;
324 : 0 : }
325 : :
326 : 78113 : Node TermUtil::mkTypeMaxValue(TypeNode tn)
327 : : {
328 : 78113 : Node n;
329 : 78113 : NodeManager* nm = tn.getNodeManager();
330 [ + + ]: 78113 : if (tn.isBitVector())
331 : : {
332 : 142 : n = bv::utils::mkOnes(nm, tn.getConst<BitVectorSize>());
333 : : }
334 [ + + ]: 77971 : else if (tn.isBoolean())
335 : : {
336 : 75813 : n = nm->mkConst(true);
337 : : }
338 : 78113 : return n;
339 : 0 : }
340 : :
341 : 8 : Node TermUtil::mkTypeValueOffset(TypeNode tn,
342 : : Node val,
343 : : int32_t offset,
344 : : int32_t& status)
345 : : {
346 : 8 : Assert(val.isConst() && val.getType() == tn);
347 : 8 : Node val_o;
348 : 8 : status = -1;
349 [ + - ]: 8 : if (tn.isRealOrInt())
350 : : {
351 : 8 : Rational vval = val.getConst<Rational>();
352 : 8 : Rational oval(offset);
353 : 8 : status = 0;
354 : 16 : return NodeManager::mkConstRealOrInt(tn, vval + oval);
355 : 8 : }
356 [ - - ]: 0 : else if (tn.isBitVector())
357 : : {
358 : 0 : BitVector vval = val.getConst<BitVector>();
359 : 0 : uint32_t uv = static_cast<uint32_t>(offset);
360 : 0 : BitVector oval(tn.getConst<BitVectorSize>(), uv);
361 : 0 : return tn.getNodeManager()->mkConst(vval + oval);
362 : 0 : }
363 : 0 : return val_o;
364 : 8 : }
365 : :
366 : 0 : Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
367 : : {
368 : 0 : return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
369 : : }
370 : :
371 : 0 : bool TermUtil::isAntisymmetric(Kind k, Kind& dk)
372 : : {
373 [ - - ]: 0 : if (k == Kind::GT)
374 : : {
375 : 0 : dk = Kind::LT;
376 : 0 : return true;
377 : : }
378 [ - - ]: 0 : else if (k == Kind::GEQ)
379 : : {
380 : 0 : dk = Kind::LEQ;
381 : 0 : return true;
382 : : }
383 [ - - ]: 0 : else if (k == Kind::BITVECTOR_UGT)
384 : : {
385 : 0 : dk = Kind::BITVECTOR_ULT;
386 : 0 : return true;
387 : : }
388 [ - - ]: 0 : else if (k == Kind::BITVECTOR_UGE)
389 : : {
390 : 0 : dk = Kind::BITVECTOR_ULE;
391 : 0 : return true;
392 : : }
393 [ - - ]: 0 : else if (k == Kind::BITVECTOR_SGT)
394 : : {
395 : 0 : dk = Kind::BITVECTOR_SLT;
396 : 0 : return true;
397 : : }
398 [ - - ]: 0 : else if (k == Kind::BITVECTOR_SGE)
399 : : {
400 : 0 : dk = Kind::BITVECTOR_SLE;
401 : 0 : return true;
402 : : }
403 : 0 : return false;
404 : : }
405 : :
406 : 1974 : bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
407 : : {
408 : : // these should all be binary operators
409 : : // Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
410 : : // ik!=BITVECTOR_UDIV );
411 : 1974 : TypeNode tn = n.getType();
412 [ + + ]: 1974 : if (n == mkTypeValue(tn, 0))
413 : : {
414 [ + + ][ + + ]: 776 : if (ik == Kind::ADD || ik == Kind::OR || ik == Kind::XOR
[ + - ]
415 [ + + ][ + + ]: 624 : || ik == Kind::BITVECTOR_ADD || ik == Kind::BITVECTOR_OR
416 [ + + ][ + + ]: 600 : || ik == Kind::BITVECTOR_XOR || ik == Kind::STRING_CONCAT)
417 : : {
418 : 202 : return true;
419 : : }
420 [ + + ][ + - ]: 574 : else if (ik == Kind::SUB || ik == Kind::BITVECTOR_SHL
421 [ + + ][ + + ]: 474 : || ik == Kind::BITVECTOR_LSHR || ik == Kind::BITVECTOR_ASHR
422 [ + + ][ + + ]: 466 : || ik == Kind::BITVECTOR_SUB || ik == Kind::BITVECTOR_UREM)
423 : : {
424 : 116 : return arg == 1;
425 : : }
426 : : }
427 [ + + ]: 1198 : else if (n == mkTypeValue(tn, 1))
428 : : {
429 [ + + ][ - + ]: 558 : if (ik == Kind::MULT || ik == Kind::BITVECTOR_MULT)
430 : : {
431 : 10 : return true;
432 : : }
433 [ + + ][ + - ]: 548 : else if (ik == Kind::DIVISION || ik == Kind::DIVISION_TOTAL
434 [ + - ][ + - ]: 540 : || ik == Kind::INTS_DIVISION || ik == Kind::INTS_DIVISION_TOTAL
435 [ + - ][ + - ]: 540 : || ik == Kind::INTS_MODULUS || ik == Kind::INTS_MODULUS_TOTAL
436 [ + + ][ + + ]: 540 : || ik == Kind::BITVECTOR_UDIV || ik == Kind::BITVECTOR_SDIV)
437 : : {
438 : 20 : return arg == 1;
439 : : }
440 : : }
441 [ + + ]: 640 : else if (n == mkTypeMaxValue(tn))
442 : : {
443 [ + - ][ + - ]: 174 : if (ik == Kind::EQUAL || ik == Kind::BITVECTOR_AND
444 [ - + ]: 174 : || ik == Kind::BITVECTOR_XNOR)
445 : : {
446 : 0 : return true;
447 : : }
448 : : }
449 : 1626 : return false;
450 : 1974 : }
451 : :
452 : 1694 : Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
453 : : {
454 : 1694 : TypeNode tn = n.getType();
455 [ + + ]: 1694 : if (n == mkTypeValue(tn, 0))
456 : : {
457 [ + + ][ + + ]: 516 : if (ik == Kind::AND || ik == Kind::MULT || ik == Kind::BITVECTOR_AND
[ + + ]
458 [ - + ]: 452 : || ik == Kind::BITVECTOR_MULT)
459 : : {
460 : 64 : return n;
461 : : }
462 [ + - ][ + + ]: 452 : else if (ik == Kind::BITVECTOR_SHL || ik == Kind::BITVECTOR_LSHR
463 [ + + ][ + + ]: 450 : || ik == Kind::BITVECTOR_ASHR || ik == Kind::BITVECTOR_UREM)
464 : : {
465 [ + - ]: 6 : if (arg == 0)
466 : : {
467 : 6 : return n;
468 : : }
469 : : }
470 [ + + ][ - + ]: 446 : else if (ik == Kind::BITVECTOR_UDIV || ik == Kind::BITVECTOR_SDIV)
471 : : {
472 [ + + ]: 8 : if (arg == 0)
473 : : {
474 : 4 : return n;
475 : : }
476 [ + - ]: 4 : else if (arg == 1)
477 : : {
478 : 4 : return mkTypeMaxValue(tn);
479 : : }
480 : : }
481 [ + + ][ + - ]: 438 : else if (ik == Kind::DIVISION || ik == Kind::DIVISION_TOTAL
482 [ + - ][ + - ]: 434 : || ik == Kind::INTS_DIVISION || ik == Kind::INTS_DIVISION_TOTAL
483 [ + + ][ - + ]: 434 : || ik == Kind::INTS_MODULUS || ik == Kind::INTS_MODULUS_TOTAL)
484 : : {
485 [ + + ]: 10 : if (arg == 0)
486 : : {
487 : 6 : return n;
488 : : }
489 : : }
490 [ - + ]: 428 : else if (ik == Kind::STRING_SUBSTR)
491 : : {
492 [ - - ]: 0 : if (arg == 0)
493 : : {
494 : 0 : return n;
495 : : }
496 [ - - ]: 0 : else if (arg == 2)
497 : : {
498 : 0 : return mkTypeValue(n.getNodeManager()->stringType(), 0);
499 : : }
500 : : }
501 [ - + ]: 428 : else if (ik == Kind::STRING_INDEXOF)
502 : : {
503 [ - - ][ - - ]: 0 : if (arg == 0 || arg == 1)
504 : : {
505 : 0 : return mkTypeValue(n.getNodeManager()->integerType(), -1);
506 : : }
507 : : }
508 : : }
509 [ + + ]: 1178 : else if (n == mkTypeValue(tn, 1))
510 : : {
511 [ + + ]: 538 : if (ik == Kind::BITVECTOR_UREM)
512 : : {
513 : 4 : return mkTypeValue(tn, 0);
514 : : }
515 : : }
516 [ + + ]: 640 : else if (n == mkTypeMaxValue(tn))
517 : : {
518 [ + + ][ - + ]: 174 : if (ik == Kind::OR || ik == Kind::BITVECTOR_OR)
519 : : {
520 : 44 : return n;
521 : : }
522 : : }
523 : : else
524 : : {
525 [ + + ][ - + ]: 466 : if (n.getType().isInteger() && n.getConst<Rational>().sgn() < 0)
[ + - ][ - + ]
[ - - ]
526 : : {
527 : : // negative arguments
528 [ - - ][ - - ]: 0 : if (ik == Kind::STRING_SUBSTR || ik == Kind::STRING_CHARAT)
529 : : {
530 : 0 : return mkTypeValue(n.getNodeManager()->stringType(), 0);
531 : : }
532 [ - - ]: 0 : else if (ik == Kind::STRING_INDEXOF)
533 : : {
534 : 0 : Assert(arg == 2);
535 : 0 : return mkTypeValue(n.getNodeManager()->integerType(), -1);
536 : : }
537 : : }
538 : : }
539 : 1562 : return Node::null();
540 : 1694 : }
541 : :
542 : 1076 : bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
543 : : {
544 [ + + ]: 1076 : if (ik == Kind::LT)
545 : : {
546 [ + + ][ + - ]: 8 : Assert(arg == 0 || arg == 1);
[ - + ][ - + ]
[ - - ]
547 [ + + ]: 8 : offset = arg == 0 ? 1 : -1;
548 : 8 : ok = Kind::LEQ;
549 : 8 : return true;
550 : : }
551 [ - + ]: 1068 : else if (ik == Kind::BITVECTOR_ULT)
552 : : {
553 : 0 : Assert(arg == 0 || arg == 1);
554 [ - - ]: 0 : offset = arg == 0 ? 1 : -1;
555 : 0 : ok = Kind::BITVECTOR_ULE;
556 : 0 : return true;
557 : : }
558 [ - + ]: 1068 : else if (ik == Kind::BITVECTOR_SLT)
559 : : {
560 : 0 : Assert(arg == 0 || arg == 1);
561 [ - - ]: 0 : offset = arg == 0 ? 1 : -1;
562 : 0 : ok = Kind::BITVECTOR_SLE;
563 : 0 : return true;
564 : : }
565 : 1068 : return false;
566 : : }
567 : :
568 : 525 : Node TermUtil::ensureType(Node n, TypeNode tn)
569 : : {
570 : 525 : TypeNode ntn = n.getType();
571 [ + + ]: 525 : if (ntn == tn)
572 : : {
573 : 516 : return n;
574 : : }
575 [ - + ]: 9 : if (tn.isInteger())
576 : : {
577 : 0 : return NodeManager::mkNode(Kind::TO_INTEGER, n);
578 : : }
579 [ + - ]: 9 : else if (tn.isReal())
580 : : {
581 : 9 : return NodeManager::mkNode(Kind::TO_REAL, n);
582 : : }
583 : 0 : return Node::null();
584 : 525 : }
585 : :
586 : : } // namespace quantifiers
587 : : } // namespace theory
588 : : } // namespace cvc5::internal
|
