Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
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 : : * Implementation of term utilities class.
14 : : */
15 : :
16 : : #include "theory/quantifiers/term_util.h"
17 : :
18 : : #include "expr/array_store_all.h"
19 : : #include "expr/function_array_const.h"
20 : : #include "expr/node_algorithm.h"
21 : : #include "expr/sequence.h"
22 : : #include "expr/skolem_manager.h"
23 : : #include "theory/arith/arith_msum.h"
24 : : #include "theory/bv/theory_bv_utils.h"
25 : : #include "theory/quantifiers/term_database.h"
26 : : #include "theory/quantifiers/term_enumeration.h"
27 : : #include "theory/rewriter.h"
28 : : #include "theory/strings/word.h"
29 : : #include "util/bitvector.h"
30 : : #include "util/rational.h"
31 : :
32 : : using namespace cvc5::internal::kind;
33 : :
34 : : namespace cvc5::internal {
35 : : namespace theory {
36 : : namespace quantifiers {
37 : :
38 : 6530 : size_t TermUtil::getVariableNum(Node q, Node v)
39 : : {
40 : 6530 : Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
41 [ - + ][ - + ]: 6530 : Assert(it != q[0].end());
[ - - ]
42 : 6530 : return it - q[0].begin();
43 : : }
44 : :
45 : 26485 : Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
46 : 26485 : std::map< Node, Node >::iterator it = visited.find( n );
47 [ + + ]: 26485 : if( it!=visited.end() ){
48 : 9941 : return it->second;
49 : : }else{
50 : 33088 : Node ret = n;
51 [ + + ]: 16544 : if (n.getKind() == Kind::FORALL)
52 : : {
53 : 997 : ret = getRemoveQuantifiers2( n[1], visited );
54 : : }
55 [ + + ]: 15547 : else if (n.getNumChildren() > 0)
56 : : {
57 : 22070 : std::vector< Node > children;
58 : 11035 : bool childrenChanged = false;
59 [ + + ]: 35514 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
60 : 48958 : Node ni = getRemoveQuantifiers2( n[i], visited );
61 [ + + ][ + + ]: 24479 : childrenChanged = childrenChanged || ni!=n[i];
[ + + ][ - - ]
62 : 24479 : children.push_back( ni );
63 : : }
64 [ + + ]: 11035 : if( childrenChanged ){
65 [ - + ]: 12 : if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
66 : 0 : children.insert( children.begin(), n.getOperator() );
67 : : }
68 : 12 : ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
69 : : }
70 : : }
71 : 16544 : visited[n] = ret;
72 : 16544 : return ret;
73 : : }
74 : : }
75 : :
76 : 15296700 : Node TermUtil::getInstConstAttr( Node n ) {
77 [ + + ]: 15296700 : if (!n.hasAttribute(InstConstantAttribute()))
78 : : {
79 : 2353560 : Node q;
80 [ + + ]: 1176780 : if (n.isVar())
81 : : {
82 : : // If it is a purification variable, it may correspond to a term
83 : : // with instantiation constants in it. We get the unpurified form here
84 : : // to handle this case.
85 : 358222 : Node un = SkolemManager::getUnpurifiedForm(n);
86 [ + - ][ + + ]: 179111 : if (!un.isNull() && un != n)
[ + + ]
87 : : {
88 : 76753 : q = getInstConstAttr(un);
89 : : }
90 : : }
91 : : else
92 : : {
93 [ + + ]: 2412620 : for (const Node& nc : n)
94 : : {
95 : 1672020 : q = getInstConstAttr(nc);
96 [ + + ]: 1672020 : if (!q.isNull())
97 : : {
98 : 257078 : break;
99 : : }
100 : : }
101 [ + + ]: 997668 : if (q.isNull())
102 : : {
103 [ + + ]: 740590 : if (n.hasOperator())
104 : : {
105 : 640736 : q = getInstConstAttr(n.getOperator());
106 : : }
107 : : }
108 : : }
109 : : InstConstantAttribute ica;
110 : 1176780 : n.setAttribute(ica, q);
111 : : }
112 : 30593400 : return n.getAttribute(InstConstantAttribute());
113 : : }
114 : :
115 : 8394780 : bool TermUtil::hasInstConstAttr(Node n)
116 : : {
117 : 8394780 : return !getInstConstAttr(n).isNull();
118 : : }
119 : :
120 : 350506 : Node TermUtil::getBoundVarAttr( Node n ) {
121 [ + + ]: 350506 : if (!n.hasAttribute(BoundVarAttribute()) ){
122 : 345664 : Node bv;
123 [ + + ]: 172832 : if (n.getKind() == Kind::BOUND_VARIABLE)
124 : : {
125 : 12249 : bv = n;
126 : : }
127 : : else
128 : : {
129 [ + + ]: 214205 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
130 : 178860 : bv = getBoundVarAttr(n[i]);
131 [ + + ]: 178860 : if( !bv.isNull() ){
132 : 125238 : break;
133 : : }
134 : : }
135 : : }
136 : : BoundVarAttribute bva;
137 : 172832 : n.setAttribute(bva, bv);
138 : : }
139 : 701012 : return n.getAttribute(BoundVarAttribute());
140 : : }
141 : :
142 : 171646 : bool TermUtil::hasBoundVarAttr( Node n ) {
143 : 171646 : return !getBoundVarAttr(n).isNull();
144 : : }
145 : :
146 : : //remove quantifiers
147 : 1009 : Node TermUtil::getRemoveQuantifiers( Node n ) {
148 : 1009 : std::map< Node, Node > visited;
149 : 2018 : return getRemoveQuantifiers2( n, visited );
150 : : }
151 : :
152 : 433983 : void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
153 : : {
154 : 433983 : computeVarContainsInternal(n, Kind::INST_CONSTANT, ics);
155 : 433983 : }
156 : :
157 : 0 : void TermUtil::computeVarContains(Node n, std::vector<Node>& vars)
158 : : {
159 : 0 : computeVarContainsInternal(n, Kind::BOUND_VARIABLE, vars);
160 : 0 : }
161 : :
162 : 3313 : void TermUtil::computeQuantContains(Node n, std::vector<Node>& quants)
163 : : {
164 : 3313 : computeVarContainsInternal(n, Kind::FORALL, quants);
165 : 3313 : }
166 : :
167 : 437296 : void TermUtil::computeVarContainsInternal(Node n,
168 : : Kind k,
169 : : std::vector<Node>& vars)
170 : : {
171 : 874592 : std::unordered_set<TNode> visited;
172 : 437296 : std::unordered_set<TNode>::iterator it;
173 : 874592 : std::vector<TNode> visit;
174 : 874592 : TNode cur;
175 : 437296 : visit.push_back(n);
176 : 3468610 : do
177 : : {
178 : 3905900 : cur = visit.back();
179 : 3905900 : visit.pop_back();
180 : 3905900 : it = visited.find(cur);
181 : :
182 [ + + ]: 3905900 : if (it == visited.end())
183 : : {
184 : 3571410 : visited.insert(cur);
185 [ + + ]: 3571410 : if (cur.getKind() == k)
186 : : {
187 [ + - ]: 1148260 : if (std::find(vars.begin(), vars.end(), cur) == vars.end())
188 : : {
189 : 1148260 : vars.push_back(cur);
190 : : }
191 : : }
192 : : else
193 : : {
194 [ + + ]: 2423150 : if (cur.hasOperator())
195 : : {
196 : 1109210 : visit.push_back(cur.getOperator());
197 : : }
198 [ + + ]: 4782540 : for (const Node& cn : cur)
199 : : {
200 : 2359400 : visit.push_back(cn);
201 : : }
202 : : }
203 : : }
204 [ + + ]: 3905900 : } while (!visit.empty());
205 : 437296 : }
206 : :
207 : 312337 : void TermUtil::computeInstConstContainsForQuant(Node q,
208 : : Node n,
209 : : std::vector<Node>& vars)
210 : : {
211 : 624674 : std::vector<Node> ics;
212 : 312337 : computeInstConstContains(n, ics);
213 [ + + ]: 1192130 : for (const Node& v : ics)
214 : : {
215 [ + - ]: 879796 : if (v.getAttribute(InstConstantAttribute()) == q)
216 : : {
217 [ + + ]: 879796 : if (std::find(vars.begin(), vars.end(), v) == vars.end())
218 : : {
219 : 879794 : vars.push_back(v);
220 : : }
221 : : }
222 : : }
223 : 312337 : }
224 : :
225 : 0 : int TermUtil::getTermDepth( Node n ) {
226 [ - - ]: 0 : if (!n.hasAttribute(TermDepthAttribute()) ){
227 : 0 : int maxDepth = -1;
228 [ - - ]: 0 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
229 : 0 : int depth = getTermDepth( n[i] );
230 [ - - ]: 0 : if( depth>maxDepth ){
231 : 0 : maxDepth = depth;
232 : : }
233 : : }
234 : : TermDepthAttribute tda;
235 : 0 : n.setAttribute(tda,1+maxDepth);
236 : : }
237 : 0 : return n.getAttribute(TermDepthAttribute());
238 : : }
239 : :
240 : 556983 : bool TermUtil::containsUninterpretedConstant( Node n ) {
241 [ + + ]: 556983 : if (n.hasAttribute(ContainsUConstAttribute()))
242 : : {
243 : 512010 : return n.getAttribute(ContainsUConstAttribute()) != 0;
244 : : }
245 : 44973 : bool ret = false;
246 : 44973 : Kind k = n.getKind();
247 [ + + ]: 44973 : if (k == Kind::UNINTERPRETED_SORT_VALUE)
248 : : {
249 [ - + ][ - + ]: 1509 : Assert(n.getType().isUninterpretedSort());
[ - - ]
250 : 1509 : ret = true;
251 : : }
252 [ + + ]: 43464 : else if (k == Kind::STORE_ALL)
253 : : {
254 : 6 : ret = containsUninterpretedConstant(n.getConst<ArrayStoreAll>().getValue());
255 : : }
256 [ - + ]: 43458 : else if (k == Kind::FUNCTION_ARRAY_CONST)
257 : : {
258 : 0 : ret = containsUninterpretedConstant(
259 : 0 : n.getConst<FunctionArrayConst>().getArrayValue());
260 : : }
261 [ + + ]: 43458 : else if (k == Kind::CONST_SEQUENCE)
262 : : {
263 : 7 : const std::vector<Node>& charVec = n.getConst<Sequence>().getVec();
264 [ - + ]: 7 : for (const Node& nc : charVec)
265 : : {
266 [ - - ]: 0 : if (containsUninterpretedConstant(nc))
267 : : {
268 : 0 : ret = true;
269 : 0 : break;
270 : : }
271 : : }
272 : : }
273 : : else
274 : : {
275 [ + + ]: 79976 : for (const Node& nc : n)
276 : : {
277 [ - + ]: 36525 : if (containsUninterpretedConstant(nc))
278 : : {
279 : 0 : ret = true;
280 : 0 : break;
281 : : }
282 : : }
283 : : }
284 : : ContainsUConstAttribute cuca;
285 [ + + ]: 44973 : n.setAttribute(cuca, ret ? 1 : 0);
286 : 44973 : return ret;
287 : : }
288 : :
289 : 18565 : Node TermUtil::simpleNegate(Node n)
290 : : {
291 [ - + ][ - + ]: 18565 : Assert(n.getType().isBoolean());
[ - - ]
292 : 18565 : NodeManager* nm = NodeManager::currentNM();
293 [ + + ][ + + ]: 18565 : if (n.getKind() == Kind::OR || n.getKind() == Kind::AND)
[ + + ]
294 : : {
295 : 8148 : std::vector< Node > children;
296 [ + + ]: 15214 : for (const Node& cn : n)
297 : : {
298 : 11140 : children.push_back(simpleNegate(cn));
299 : : }
300 [ + + ]: 4074 : return nm->mkNode(n.getKind() == Kind::OR ? Kind::AND : Kind::OR, children);
301 : : }
302 [ + + ]: 14491 : else if (n.isConst())
303 : : {
304 : 8418 : return nm->mkConst(!n.getConst<bool>());
305 : : }
306 : 10282 : return n.negate();
307 : : }
308 : :
309 : 6736 : Node TermUtil::mkNegate(Kind notk, Node n)
310 : : {
311 [ + + ]: 6736 : if (n.getKind() == notk)
312 : : {
313 : 588 : return n[0];
314 : : }
315 : 6148 : return NodeManager::mkNode(notk, n);
316 : : }
317 : :
318 : 15998 : bool TermUtil::isNegate(Kind k)
319 : : {
320 [ + + ][ + + ]: 15351 : return k == Kind::NOT || k == Kind::BITVECTOR_NOT || k == Kind::BITVECTOR_NEG
321 [ + + ][ - + ]: 31349 : || k == Kind::NEG;
322 : : }
323 : :
324 : 253808 : bool TermUtil::isAssoc(Kind k, bool reqNAry)
325 : : {
326 [ + + ]: 253808 : if (reqNAry)
327 : : {
328 [ + + ][ + + ]: 252914 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
329 : : {
330 : 62 : return false;
331 : : }
332 : : }
333 [ + + ][ + + ]: 234224 : return k == Kind::ADD || k == Kind::MULT || k == Kind::NONLINEAR_MULT
334 [ + + ][ + + ]: 228612 : || k == Kind::AND || k == Kind::OR || k == Kind::XOR
[ + + ]
335 [ + + ][ + + ]: 153353 : || k == Kind::BITVECTOR_ADD || k == Kind::BITVECTOR_MULT
336 [ + + ][ + + ]: 144643 : || k == Kind::BITVECTOR_AND || k == Kind::BITVECTOR_OR
337 [ + + ][ + - ]: 135268 : || k == Kind::BITVECTOR_XOR || k == Kind::BITVECTOR_XNOR
338 [ + + ][ + + ]: 135148 : || k == Kind::BITVECTOR_CONCAT || k == Kind::STRING_CONCAT
339 [ + + ][ + + ]: 131891 : || k == Kind::SET_UNION || k == Kind::SET_INTER
340 [ + - ][ + - ]: 131883 : || k == Kind::RELATION_JOIN || k == Kind::RELATION_TABLE_JOIN
341 [ + + ][ + - ]: 487970 : || k == Kind::RELATION_PRODUCT || k == Kind::SEP_STAR;
[ - + ]
342 : : }
343 : :
344 : 894517 : bool TermUtil::isComm(Kind k, bool reqNAry)
345 : : {
346 [ - + ]: 894517 : if (reqNAry)
347 : : {
348 [ - - ][ - - ]: 0 : if (k == Kind::SET_UNION || k == Kind::SET_INTER)
349 : : {
350 : 0 : return false;
351 : : }
352 : : }
353 [ + + ][ + + ]: 764063 : return k == Kind::EQUAL || k == Kind::ADD || k == Kind::MULT
354 [ + + ][ + + ]: 685832 : || k == Kind::NONLINEAR_MULT || k == Kind::AND || k == Kind::OR
[ + + ]
355 [ + + ][ + + ]: 556000 : || k == Kind::XOR || k == Kind::BITVECTOR_ADD
356 [ + + ][ + + ]: 551563 : || k == Kind::BITVECTOR_MULT || k == Kind::BITVECTOR_AND
357 [ + + ][ + + ]: 541822 : || k == Kind::BITVECTOR_OR || k == Kind::BITVECTOR_XOR
358 [ + - ][ + + ]: 536419 : || k == Kind::BITVECTOR_XNOR || k == Kind::SET_UNION
359 [ + + ][ + + ]: 1658580 : || k == Kind::SET_INTER || k == Kind::SEP_STAR;
[ + + ]
360 : : }
361 : :
362 : 253186 : bool TermUtil::isNonAdditive( Kind k ) {
363 [ + + ][ + + ]: 212875 : return k == Kind::AND || k == Kind::OR || k == Kind::BITVECTOR_AND
364 [ + + ][ + + ]: 466061 : || k == Kind::BITVECTOR_OR;
365 : : }
366 : :
367 : 796318 : bool TermUtil::isBoolConnective( Kind k ) {
368 [ + + ][ + + ]: 689592 : return k == Kind::OR || k == Kind::AND || k == Kind::EQUAL || k == Kind::ITE
[ + + ]
369 [ + + ][ + + ]: 1485910 : || k == Kind::FORALL || k == Kind::NOT || k == Kind::SEP_STAR;
[ + + ][ + + ]
370 : : }
371 : :
372 : 683533 : bool TermUtil::isBoolConnectiveTerm( TNode n ) {
373 : 683533 : return isBoolConnective(n.getKind())
374 : 1159650 : && (n.getKind() != Kind::EQUAL || n[0].getType().isBoolean())
375 [ + + ][ + + ]: 2526710 : && (n.getKind() != Kind::ITE || n.getType().isBoolean());
[ + + ][ + + ]
[ + + ][ - - ]
376 : : }
377 : :
378 : 82966 : Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
379 : : {
380 : 82966 : Node n;
381 [ + + ]: 82966 : if (tn.isRealOrInt())
382 : : {
383 : 6238 : Rational c(val);
384 : 6238 : n = NodeManager::currentNM()->mkConstRealOrInt(tn, c);
385 : : }
386 [ + + ]: 76728 : else if (tn.isBitVector())
387 : : {
388 : : // cast to unsigned
389 : 802 : uint32_t uv = static_cast<uint32_t>(val);
390 : 802 : BitVector bval(tn.getConst<BitVectorSize>(), uv);
391 : 802 : n = NodeManager::currentNM()->mkConst<BitVector>(bval);
392 : : }
393 [ + + ]: 75926 : else if (tn.isBoolean())
394 : : {
395 [ + + ]: 75346 : if (val == 0)
396 : : {
397 : 74790 : n = NodeManager::currentNM()->mkConst(false);
398 : : }
399 : : }
400 [ + + ]: 580 : else if (tn.isStringLike())
401 : : {
402 [ + + ]: 412 : if (val == 0)
403 : : {
404 : 222 : n = strings::Word::mkEmptyWord(tn);
405 : : }
406 : : }
407 : 82966 : return n;
408 : : }
409 : :
410 : 76744 : Node TermUtil::mkTypeMaxValue(TypeNode tn)
411 : : {
412 : 76744 : Node n;
413 [ + + ]: 76744 : if (tn.isBitVector())
414 : : {
415 : 142 : n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
416 : : }
417 [ + + ]: 76602 : else if (tn.isBoolean())
418 : : {
419 : 74492 : n = NodeManager::currentNM()->mkConst(true);
420 : : }
421 : 76744 : return n;
422 : : }
423 : :
424 : 8 : Node TermUtil::mkTypeValueOffset(TypeNode tn,
425 : : Node val,
426 : : int32_t offset,
427 : : int32_t& status)
428 : : {
429 : 16 : Assert(val.isConst() && val.getType() == tn);
430 : 16 : Node val_o;
431 : 8 : status = -1;
432 [ + - ]: 8 : if (tn.isRealOrInt())
433 : : {
434 : 16 : Rational vval = val.getConst<Rational>();
435 : 8 : Rational oval(offset);
436 : 8 : status = 0;
437 : 16 : return NodeManager::currentNM()->mkConstRealOrInt(tn, vval + oval);
438 : : }
439 [ - - ]: 0 : else if (tn.isBitVector())
440 : : {
441 : 0 : BitVector vval = val.getConst<BitVector>();
442 : 0 : uint32_t uv = static_cast<uint32_t>(offset);
443 : 0 : BitVector oval(tn.getConst<BitVectorSize>(), uv);
444 : 0 : return NodeManager::currentNM()->mkConst(vval + oval);
445 : : }
446 : 0 : return val_o;
447 : : }
448 : :
449 : 2 : Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
450 : : {
451 : 2 : return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
452 : : }
453 : :
454 : 0 : bool TermUtil::isAntisymmetric(Kind k, Kind& dk)
455 : : {
456 [ - - ]: 0 : if (k == Kind::GT)
457 : : {
458 : 0 : dk = Kind::LT;
459 : 0 : return true;
460 : : }
461 [ - - ]: 0 : else if (k == Kind::GEQ)
462 : : {
463 : 0 : dk = Kind::LEQ;
464 : 0 : return true;
465 : : }
466 [ - - ]: 0 : else if (k == Kind::BITVECTOR_UGT)
467 : : {
468 : 0 : dk = Kind::BITVECTOR_ULT;
469 : 0 : return true;
470 : : }
471 [ - - ]: 0 : else if (k == Kind::BITVECTOR_UGE)
472 : : {
473 : 0 : dk = Kind::BITVECTOR_ULE;
474 : 0 : return true;
475 : : }
476 [ - - ]: 0 : else if (k == Kind::BITVECTOR_SGT)
477 : : {
478 : 0 : dk = Kind::BITVECTOR_SLT;
479 : 0 : return true;
480 : : }
481 [ - - ]: 0 : else if (k == Kind::BITVECTOR_SGE)
482 : : {
483 : 0 : dk = Kind::BITVECTOR_SLE;
484 : 0 : return true;
485 : : }
486 : 0 : return false;
487 : : }
488 : :
489 : 1922 : bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
490 : : {
491 : : // these should all be binary operators
492 : : // Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
493 : : // ik!=BITVECTOR_UDIV );
494 : 3844 : TypeNode tn = n.getType();
495 [ + + ]: 1922 : if (n == mkTypeValue(tn, 0))
496 : : {
497 [ + + ][ + + ]: 751 : if (ik == Kind::ADD || ik == Kind::OR || ik == Kind::XOR
[ + - ]
498 [ + + ][ + + ]: 603 : || ik == Kind::BITVECTOR_ADD || ik == Kind::BITVECTOR_OR
499 [ + + ][ + + ]: 579 : || ik == Kind::BITVECTOR_XOR || ik == Kind::STRING_CONCAT)
500 : : {
501 : 200 : return true;
502 : : }
503 [ + + ][ + - ]: 551 : else if (ik == Kind::SUB || ik == Kind::BITVECTOR_SHL
504 [ + + ][ + + ]: 451 : || ik == Kind::BITVECTOR_LSHR || ik == Kind::BITVECTOR_ASHR
505 [ + + ][ + + ]: 443 : || ik == Kind::BITVECTOR_SUB || ik == Kind::BITVECTOR_UREM)
506 : : {
507 : 116 : return arg == 1;
508 : : }
509 : : }
510 [ + + ]: 1171 : else if (n == mkTypeValue(tn, 1))
511 : : {
512 [ + + ][ - + ]: 534 : if (ik == Kind::MULT || ik == Kind::BITVECTOR_MULT)
513 : : {
514 : 10 : return true;
515 : : }
516 [ + + ][ + - ]: 524 : else if (ik == Kind::DIVISION || ik == Kind::DIVISION_TOTAL
517 [ + - ][ + - ]: 516 : || ik == Kind::INTS_DIVISION || ik == Kind::INTS_DIVISION_TOTAL
518 [ + - ][ + - ]: 516 : || ik == Kind::INTS_MODULUS || ik == Kind::INTS_MODULUS_TOTAL
519 [ + + ][ + + ]: 516 : || ik == Kind::BITVECTOR_UDIV || ik == Kind::BITVECTOR_SDIV)
520 : : {
521 : 20 : return arg == 1;
522 : : }
523 : : }
524 [ + + ]: 637 : else if (n == mkTypeMaxValue(tn))
525 : : {
526 [ + - ][ + - ]: 171 : if (ik == Kind::EQUAL || ik == Kind::BITVECTOR_AND
527 [ - + ]: 171 : || ik == Kind::BITVECTOR_XNOR)
528 : : {
529 : 0 : return true;
530 : : }
531 : : }
532 : 1576 : return false;
533 : : }
534 : :
535 : 1644 : Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
536 : : {
537 : 3288 : TypeNode tn = n.getType();
538 [ + + ]: 1644 : if (n == mkTypeValue(tn, 0))
539 : : {
540 [ + + ][ + + ]: 493 : if (ik == Kind::AND || ik == Kind::MULT || ik == Kind::BITVECTOR_AND
[ + + ]
541 [ - + ]: 427 : || ik == Kind::BITVECTOR_MULT)
542 : : {
543 : 66 : return n;
544 : : }
545 [ + - ][ + + ]: 427 : else if (ik == Kind::BITVECTOR_SHL || ik == Kind::BITVECTOR_LSHR
546 [ + + ][ + + ]: 425 : || ik == Kind::BITVECTOR_ASHR || ik == Kind::BITVECTOR_UREM)
547 : : {
548 [ + - ]: 6 : if (arg == 0)
549 : : {
550 : 6 : return n;
551 : : }
552 : : }
553 [ + + ][ - + ]: 421 : else if (ik == Kind::BITVECTOR_UDIV || ik == Kind::BITVECTOR_SDIV)
554 : : {
555 [ + + ]: 8 : if (arg == 0)
556 : : {
557 : 4 : return n;
558 : : }
559 [ + - ]: 4 : else if (arg == 1)
560 : : {
561 : 4 : return mkTypeMaxValue(tn);
562 : : }
563 : : }
564 [ + + ][ + - ]: 413 : else if (ik == Kind::DIVISION || ik == Kind::DIVISION_TOTAL
565 [ + - ][ + - ]: 409 : || ik == Kind::INTS_DIVISION || ik == Kind::INTS_DIVISION_TOTAL
566 [ + + ][ - + ]: 409 : || ik == Kind::INTS_MODULUS || ik == Kind::INTS_MODULUS_TOTAL)
567 : : {
568 [ + + ]: 10 : if (arg == 0)
569 : : {
570 : 6 : return n;
571 : : }
572 : : }
573 [ - + ]: 403 : else if (ik == Kind::STRING_SUBSTR)
574 : : {
575 [ - - ]: 0 : if (arg == 0)
576 : : {
577 : 0 : return n;
578 : : }
579 [ - - ]: 0 : else if (arg == 2)
580 : : {
581 : 0 : return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
582 : : }
583 : : }
584 [ - + ]: 403 : else if (ik == Kind::STRING_INDEXOF)
585 : : {
586 [ - - ][ - - ]: 0 : if (arg == 0 || arg == 1)
587 : : {
588 : 0 : return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
589 : : }
590 : : }
591 : : }
592 [ + + ]: 1151 : else if (n == mkTypeValue(tn, 1))
593 : : {
594 [ + + ]: 514 : if (ik == Kind::BITVECTOR_UREM)
595 : : {
596 : 4 : return mkTypeValue(tn, 0);
597 : : }
598 : : }
599 [ + + ]: 637 : else if (n == mkTypeMaxValue(tn))
600 : : {
601 [ + + ][ - + ]: 171 : if (ik == Kind::OR || ik == Kind::BITVECTOR_OR)
602 : : {
603 : 40 : return n;
604 : : }
605 : : }
606 : : else
607 : : {
608 [ + + ][ - + ]: 466 : if (n.getType().isInteger() && n.getConst<Rational>().sgn() < 0)
[ + - ][ - + ]
[ - - ]
609 : : {
610 : : // negative arguments
611 [ - - ][ - - ]: 0 : if (ik == Kind::STRING_SUBSTR || ik == Kind::STRING_CHARAT)
612 : : {
613 : 0 : return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
614 : : }
615 [ - - ]: 0 : else if (ik == Kind::STRING_INDEXOF)
616 : : {
617 : 0 : Assert(arg == 2);
618 : 0 : return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
619 : : }
620 : : }
621 : : }
622 : 1514 : return Node::null();
623 : : }
624 : :
625 : 1034 : bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
626 : : {
627 [ + + ]: 1034 : if (ik == Kind::LT)
628 : : {
629 [ + + ][ - + ]: 8 : Assert(arg == 0 || arg == 1);
[ - + ][ - - ]
630 [ + + ]: 8 : offset = arg == 0 ? 1 : -1;
631 : 8 : ok = Kind::LEQ;
632 : 8 : return true;
633 : : }
634 [ - + ]: 1026 : else if (ik == Kind::BITVECTOR_ULT)
635 : : {
636 : 0 : Assert(arg == 0 || arg == 1);
637 [ - - ]: 0 : offset = arg == 0 ? 1 : -1;
638 : 0 : ok = Kind::BITVECTOR_ULE;
639 : 0 : return true;
640 : : }
641 [ - + ]: 1026 : else if (ik == Kind::BITVECTOR_SLT)
642 : : {
643 : 0 : Assert(arg == 0 || arg == 1);
644 [ - - ]: 0 : offset = arg == 0 ? 1 : -1;
645 : 0 : ok = Kind::BITVECTOR_SLE;
646 : 0 : return true;
647 : : }
648 : 1026 : return false;
649 : : }
650 : :
651 : 606 : Node TermUtil::ensureType(Node n, TypeNode tn)
652 : : {
653 : 1212 : TypeNode ntn = n.getType();
654 [ + + ]: 606 : if (ntn == tn)
655 : : {
656 : 588 : return n;
657 : : }
658 [ - + ]: 18 : if (tn.isInteger())
659 : : {
660 : 0 : return NodeManager::mkNode(Kind::TO_INTEGER, n);
661 : : }
662 [ + - ]: 18 : else if (tn.isReal())
663 : : {
664 : 18 : return NodeManager::mkNode(Kind::TO_REAL, n);
665 : : }
666 : 0 : return Node::null();
667 : : }
668 : :
669 : : } // namespace quantifiers
670 : : } // namespace theory
671 : : } // namespace cvc5::internal
|
