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 : 27421 : Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
43 : 27421 : std::map< Node, Node >::iterator it = visited.find( n );
44 [ + + ]: 27421 : if( it!=visited.end() ){
45 : 10110 : return it->second;
46 : : }else{
47 : 17311 : Node ret = n;
48 [ + + ]: 17311 : if (n.getKind() == Kind::FORALL)
49 : : {
50 : 1060 : ret = getRemoveQuantifiers2( n[1], visited );
51 : : }
52 [ + + ]: 16251 : else if (n.getNumChildren() > 0)
53 : : {
54 : 11480 : std::vector< Node > children;
55 : 11480 : bool childrenChanged = false;
56 [ + + ]: 36769 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
57 : 25289 : Node ni = getRemoveQuantifiers2( n[i], visited );
58 [ + + ][ + + ]: 25289 : childrenChanged = childrenChanged || ni!=n[i];
[ + + ][ - - ]
59 : 25289 : children.push_back( ni );
60 : 25289 : }
61 [ + + ]: 11480 : 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 : 11480 : }
68 : 17311 : visited[n] = ret;
69 : 17311 : return ret;
70 : 17311 : }
71 : : }
72 : :
73 : 13965423 : Node TermUtil::getInstConstAttr( Node n ) {
74 [ + + ]: 13965423 : if (!n.hasAttribute(InstConstantAttribute()))
75 : : {
76 : 1099840 : Node q;
77 [ + + ]: 1099840 : 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 : 172322 : Node un = SkolemManager::getUnpurifiedForm(n);
83 [ + - ][ + + ]: 172322 : if (!un.isNull() && un != n)
[ + + ]
84 : : {
85 : 76481 : q = getInstConstAttr(un);
86 : : }
87 : 172322 : }
88 : : else
89 : : {
90 [ + + ]: 2238270 : for (const Node& nc : n)
91 : : {
92 : 1540560 : q = getInstConstAttr(nc);
93 [ + + ]: 1540560 : if (!q.isNull())
94 : : {
95 : 229808 : break;
96 : : }
97 [ + + ]: 1540560 : }
98 [ + + ]: 927518 : if (q.isNull())
99 : : {
100 [ + + ]: 697710 : if (n.hasOperator())
101 : : {
102 : 590096 : q = getInstConstAttr(n.getOperator());
103 : : }
104 : : }
105 : : }
106 : : InstConstantAttribute ica;
107 : 1099840 : n.setAttribute(ica, q);
108 : 1099840 : }
109 : 27930846 : return n.getAttribute(InstConstantAttribute());
110 : : }
111 : :
112 : 7818165 : bool TermUtil::hasInstConstAttr(Node n)
113 : : {
114 : 7818165 : 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 : 271048 : void TermUtil::computeInstConstContainsForQuant(Node q,
124 : : Node n,
125 : : std::vector<Node>& vars)
126 : : {
127 : 271048 : std::unordered_set<Node> ics;
128 : 271048 : expr::getSubtermsKind(Kind::INST_CONSTANT, n, ics);
129 [ + + ]: 1032676 : for (const Node& v : ics)
130 : : {
131 [ + - ]: 761628 : if (v.getAttribute(InstConstantAttribute()) == q)
132 : : {
133 [ + + ]: 761628 : if (std::find(vars.begin(), vars.end(), v) == vars.end())
134 : : {
135 : 761626 : vars.push_back(v);
136 : : }
137 : : }
138 : : }
139 : 271048 : }
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 : 504721 : bool TermUtil::containsUninterpretedConstant( Node n ) {
157 [ + + ]: 504721 : if (n.hasAttribute(ContainsUConstAttribute()))
158 : : {
159 : 464370 : return n.getAttribute(ContainsUConstAttribute()) != 0;
160 : : }
161 : 40351 : bool ret = false;
162 : 40351 : Kind k = n.getKind();
163 [ + + ]: 40351 : if (k == Kind::UNINTERPRETED_SORT_VALUE)
164 : : {
165 [ - + ][ - + ]: 1431 : Assert(n.getType().isUninterpretedSort());
[ - - ]
166 : 1431 : ret = true;
167 : : }
168 [ + + ]: 38920 : else if (k == Kind::STORE_ALL)
169 : : {
170 : 8 : ret = containsUninterpretedConstant(n.getConst<ArrayStoreAll>().getValue());
171 : : }
172 [ - + ]: 38912 : else if (k == Kind::FUNCTION_ARRAY_CONST)
173 : : {
174 : 0 : ret = containsUninterpretedConstant(
175 : 0 : n.getConst<FunctionArrayConst>().getArrayValue());
176 : : }
177 [ + + ]: 38912 : 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 [ + + ]: 70922 : for (const Node& nc : n)
192 : : {
193 [ - + ]: 32016 : if (containsUninterpretedConstant(nc))
194 : : {
195 : 0 : ret = true;
196 : 0 : break;
197 : : }
198 [ + - ]: 32016 : }
199 : : }
200 : : ContainsUConstAttribute cuca;
201 [ + + ]: 40351 : n.setAttribute(cuca, ret ? 1 : 0);
202 : 40351 : return ret;
203 : : }
204 : :
205 : 15058 : Node TermUtil::simpleNegate(Node n)
206 : : {
207 [ - + ][ - + ]: 15058 : Assert(n.getType().isBoolean());
[ - - ]
208 : 15058 : NodeManager* nm = n.getNodeManager();
209 [ + + ][ + + ]: 15058 : if (n.getKind() == Kind::OR || n.getKind() == Kind::AND)
[ + + ]
210 : : {
211 : 3513 : std::vector< Node > children;
212 [ + + ]: 13034 : for (const Node& cn : n)
213 : : {
214 : 9521 : children.push_back(simpleNegate(cn));
215 : 9521 : }
216 [ + + ]: 3513 : return nm->mkNode(n.getKind() == Kind::OR ? Kind::AND : Kind::OR, children);
217 : 3513 : }
218 [ + + ]: 11545 : else if (n.isConst())
219 : : {
220 : 6320 : return nm->mkConst(!n.getConst<bool>());
221 : : }
222 : 8385 : return n.negate();
223 : : }
224 : :
225 : 6819 : Node TermUtil::mkNegate(Kind notk, Node n)
226 : : {
227 [ + + ]: 6819 : if (n.getKind() == notk)
228 : : {
229 : 592 : return n[0];
230 : : }
231 : 6227 : return NodeManager::mkNode(notk, n);
232 : : }
233 : :
234 : 15452 : bool TermUtil::isNegate(Kind k)
235 : : {
236 [ + + ][ + + ]: 14817 : return k == Kind::NOT || k == Kind::BITVECTOR_NOT || k == Kind::BITVECTOR_NEG
237 [ + + ][ - + ]: 30269 : || k == Kind::NEG;
238 : : }
239 : :
240 : 247859 : bool TermUtil::isAssoc(Kind k, bool reqNAry)
241 : : {
242 [ + + ]: 247859 : if (reqNAry)
243 : : {
244 [ + + ][ + + ]: 246946 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
245 : : {
246 : 62 : return false;
247 : : }
248 : : }
249 [ + + ][ + + ]: 229027 : return k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT
250 [ + + ][ + + ]: 223482 : || k == Kind::AND || k == Kind::OR || k == Kind::XOR
[ + + ]
251 [ + + ][ + + ]: 148189 : || k == Kind::BITVECTOR_ADD || k == Kind::BITVECTOR_MULT
252 [ + + ][ + + ]: 139879 : || k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR
253 [ + + ][ + - ]: 130516 : || k == Kind::BITVECTOR_XOR || k == Kind::BITVECTOR_XNOR
254 [ + + ][ + + ]: 130402 : || k == Kind::BITVECTOR_CONCAT || k == Kind::STRING_CONCAT
255 [ + + ][ + + ]: 127647 : || k == Kind::SET_UNION || k == Kind::SET_INTER
256 [ + - ][ + - ]: 127639 : || k == Kind::RELATION_JOIN || k == Kind::RELATION_TABLE_JOIN
257 [ + + ][ + - ]: 476824 : || k == Kind::RELATION_PRODUCT || k == Kind::SEP_STAR;
[ - + ]
258 : : }
259 : :
260 : 830145 : bool TermUtil::isComm(Kind k, bool reqNAry)
261 : : {
262 [ - + ]: 830145 : if (reqNAry)
263 : : {
264 [ - - ][ - - ]: 0 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
265 : : {
266 : 0 : return false;
267 : : }
268 : : }
269 [ + + ][ + + ]: 708320 : return k == Kind::EQUAL || k == Kind::ADD || k == Kind::MULT
270 [ + + ][ + + ]: 636037 : || k == Kind::NONLINEAR_MULT || k == Kind::AND || k == Kind::OR
[ + + ]
271 [ + + ][ + + ]: 511479 : || k == Kind::XOR || k == Kind::BITVECTOR_ADD
272 [ + + ][ + + ]: 507519 : || k == Kind::BITVECTOR_MULT || k == Kind::BITVECTOR_AND
273 [ + + ][ + + ]: 497734 : || k == Kind::BITVECTOR_OR || k == Kind::BITVECTOR_XOR
274 [ + - ][ + + ]: 492309 : || k == Kind::BITVECTOR_XNOR || k == Kind::SET_UNION
275 [ + + ][ + + ]: 1538465 : || k == Kind::SET_INTER || k == Kind::SEP_STAR;
[ + + ]
276 : : }
277 : :
278 : 247218 : bool TermUtil::isNonAdditive( Kind k ) {
279 [ + + ][ + + ]: 207009 : return k == Kind::AND || k == Kind::OR || k == Kind::BITVECTOR_AND
280 [ + + ][ + + ]: 454227 : || k == Kind::BITVECTOR_OR;
281 : : }
282 : :
283 : 712554 : bool TermUtil::isBoolConnective( Kind k ) {
284 [ + + ][ + + ]: 617563 : return k == Kind::OR || k == Kind::AND || k == Kind::EQUAL || k == Kind::ITE
[ + + ]
285 [ + + ][ + + ]: 1330117 : || k == Kind::FORALL || k == Kind::NOT || k == Kind::SEP_STAR;
[ + + ][ + + ]
286 : : }
287 : :
288 : 608283 : bool TermUtil::isBoolConnectiveTerm( TNode n ) {
289 : 608283 : return isBoolConnective(n.getKind())
290 : 1032228 : && (n.getKind() != Kind::EQUAL || n[0].getType().isBoolean())
291 [ + + ][ + + ]: 2248794 : && (n.getKind() != Kind::ITE || n.getType().isBoolean());
[ + + ][ + + ]
[ + + ][ - - ]
292 : : }
293 : :
294 : 83148 : Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
295 : : {
296 : 83148 : Node n;
297 [ + + ]: 83148 : if (tn.isRealOrInt())
298 : : {
299 : 6550 : Rational c(val);
300 : 6550 : n = tn.getNodeManager()->mkConstRealOrInt(tn, c);
301 : 6550 : }
302 [ + + ]: 76598 : 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 [ + + ]: 75796 : else if (tn.isBoolean())
310 : : {
311 [ + + ]: 75290 : if (val == 0)
312 : : {
313 : 74728 : 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 : 83148 : return n;
324 : 0 : }
325 : :
326 : 76732 : Node TermUtil::mkTypeMaxValue(TypeNode tn)
327 : : {
328 : 76732 : Node n;
329 : 76732 : NodeManager* nm = tn.getNodeManager();
330 [ + + ]: 76732 : if (tn.isBitVector())
331 : : {
332 : 142 : n = bv::utils::mkOnes(nm, tn.getConst<BitVectorSize>());
333 : : }
334 [ + + ]: 76590 : else if (tn.isBoolean())
335 : : {
336 : 74432 : n = nm->mkConst(true);
337 : : }
338 : 76732 : 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
|
