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 common functions for dealing with nodes.
11 : : */
12 : :
13 : : #include "theory/arith/arith_utilities.h"
14 : :
15 : : #include <cmath>
16 : :
17 : : #include "theory/bv/theory_bv_utils.h"
18 : : #include "util/bitvector.h"
19 : :
20 : : using namespace cvc5::internal::kind;
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace arith {
25 : :
26 : 32882 : Kind joinKinds(Kind k1, Kind k2)
27 : : {
28 [ + + ]: 32882 : if (k2 < k1)
29 : : {
30 : 10612 : return joinKinds(k2, k1);
31 : : }
32 [ - + ]: 22270 : else if (k1 == k2)
33 : : {
34 : 0 : return k1;
35 : : }
36 [ - + ][ - + ]: 22270 : Assert(isRelationOperator(k1));
[ - - ]
37 [ - + ][ - + ]: 22270 : Assert(isRelationOperator(k2));
[ - - ]
38 [ + + ]: 22270 : if (k1 == Kind::EQUAL)
39 : : {
40 [ + + ][ + - ]: 3550 : if (k2 == Kind::LEQ || k2 == Kind::GEQ)
41 : : {
42 : 3550 : return k1;
43 : : }
44 : : }
45 [ + + ]: 18720 : else if (k1 == Kind::LT)
46 : : {
47 [ + - ]: 4028 : if (k2 == Kind::LEQ)
48 : : {
49 : 4028 : return k1;
50 : : }
51 : : }
52 [ + + ]: 14692 : else if (k1 == Kind::LEQ)
53 : : {
54 [ + - ]: 90 : if (k2 == Kind::GEQ)
55 : : {
56 : 90 : return Kind::EQUAL;
57 : : }
58 : : }
59 [ + - ]: 14602 : else if (k1 == Kind::GT)
60 : : {
61 [ + - ]: 14602 : if (k2 == Kind::GEQ)
62 : : {
63 : 14602 : return k1;
64 : : }
65 : : }
66 : 0 : return Kind::UNDEFINED_KIND;
67 : : }
68 : :
69 : 0 : Kind transKinds(Kind k1, Kind k2)
70 : : {
71 [ - - ]: 0 : if (k2 < k1)
72 : : {
73 : 0 : return transKinds(k2, k1);
74 : : }
75 [ - - ]: 0 : else if (k1 == k2)
76 : : {
77 : 0 : return k1;
78 : : }
79 : 0 : Assert(isRelationOperator(k1));
80 : 0 : Assert(isRelationOperator(k2));
81 [ - - ]: 0 : if (k1 == Kind::EQUAL)
82 : : {
83 : 0 : return k2;
84 : : }
85 [ - - ]: 0 : else if (k1 == Kind::LT)
86 : : {
87 [ - - ]: 0 : if (k2 == Kind::LEQ)
88 : : {
89 : 0 : return k1;
90 : : }
91 : : }
92 [ - - ]: 0 : else if (k1 == Kind::GT)
93 : : {
94 [ - - ]: 0 : if (k2 == Kind::GEQ)
95 : : {
96 : 0 : return k1;
97 : : }
98 : : }
99 : 0 : return Kind::UNDEFINED_KIND;
100 : : }
101 : :
102 : 402938 : Node mkZero(const TypeNode& tn) { return NodeManager::mkConstRealOrInt(tn, 0); }
103 : :
104 : 30559 : bool isZero(const Node& n)
105 : : {
106 [ - + ][ - + ]: 30559 : Assert(n.getType().isRealOrInt());
[ - - ]
107 [ + + ][ + + ]: 30559 : return n.isConst() && n.getConst<Rational>().sgn() == 0;
108 : : }
109 : :
110 : 137777 : Node mkOne(const TypeNode& tn, bool isNeg)
111 : : {
112 [ - + ]: 137777 : return NodeManager::mkConstRealOrInt(tn, isNeg ? -1 : 1);
113 : : }
114 : :
115 : 6356345 : bool isTranscendentalKind(Kind k)
116 : : {
117 [ + + ]: 6356345 : switch (k)
118 : : {
119 : 18808 : case Kind::PI:
120 : : case Kind::EXPONENTIAL:
121 : : case Kind::SINE:
122 : : case Kind::COSINE:
123 : : case Kind::TANGENT:
124 : : case Kind::COSECANT:
125 : : case Kind::SECANT:
126 : : case Kind::COTANGENT:
127 : : case Kind::ARCSINE:
128 : : case Kind::ARCCOSINE:
129 : : case Kind::ARCTANGENT:
130 : : case Kind::ARCCOSECANT:
131 : : case Kind::ARCSECANT:
132 : : case Kind::ARCCOTANGENT:
133 : 18808 : case Kind::SQRT: return true;
134 : 6337537 : default: break;
135 : : }
136 : 6337537 : return false;
137 : : }
138 : :
139 : 4334853 : bool isExtendedNonLinearKind(Kind k)
140 : : {
141 [ + + ]: 4334853 : switch (k)
142 : : {
143 : 1045 : case Kind::IAND:
144 : : case Kind::POW2:
145 : 1045 : case Kind::POW: return true;
146 : 4333808 : default: break;
147 : : }
148 : 4333808 : return false;
149 : : }
150 : :
151 : 4158 : Node getApproximateConstant(Node c, bool isLower, unsigned prec)
152 : : {
153 [ - + ]: 4158 : if (!c.isConst())
154 : : {
155 : 0 : DebugUnhandled() << "getApproximateConstant: non-constant input " << c;
156 : : return Node::null();
157 : : }
158 : 4158 : Rational cr = c.getConst<Rational>();
159 : :
160 : 4158 : unsigned lower = 0;
161 : 4158 : unsigned upper = std::pow(10, prec);
162 : :
163 : 4158 : Rational den = Rational(upper);
164 [ + + ]: 4158 : if (cr.getDenominator() < den.getNumerator())
165 : : {
166 : : // denominator is not more than precision, we return it
167 : 1571 : return c;
168 : : }
169 : :
170 : 2587 : int csign = cr.sgn();
171 [ - + ][ - + ]: 2587 : Assert(csign != 0);
[ - - ]
172 [ + + ]: 2587 : if (csign == -1)
173 : : {
174 : 35 : cr = -cr;
175 : : }
176 : 2587 : Rational one = Rational(1);
177 : 2587 : Rational ten = Rational(10);
178 : 2587 : Rational pow_ten = Rational(1);
179 : : // inefficient for large numbers
180 [ + + ]: 7776 : while (cr >= one)
181 : : {
182 : 5189 : cr = cr / ten;
183 : 5189 : pow_ten = pow_ten * ten;
184 : : }
185 : 2587 : Rational allow_err = one / den;
186 : :
187 : : // now do binary search
188 : 2587 : Rational two = Rational(2);
189 : 2587 : NodeManager* nm = c.getNodeManager();
190 : 2587 : Node cret;
191 : : do
192 : : {
193 : 35922 : unsigned curr = (lower + upper) / 2;
194 : 35922 : Rational curr_r = Rational(curr) / den;
195 : 35922 : Rational err = cr - curr_r;
196 : 35922 : int esign = err.sgn();
197 [ + + ]: 35922 : if (err.abs() <= allow_err)
198 : : {
199 [ + + ][ - + ]: 2587 : if (esign == 1 && !isLower)
200 : : {
201 : 0 : curr_r = Rational(curr + 1) / den;
202 : : }
203 [ + + ][ + - ]: 2587 : else if (esign == -1 && isLower)
204 : : {
205 : 427 : curr_r = Rational(curr - 1) / den;
206 : : }
207 : 2587 : curr_r = curr_r * pow_ten;
208 [ + + ]: 2587 : cret = nm->mkConst(Kind::CONST_RATIONAL, csign == 1 ? curr_r : -curr_r);
209 : : }
210 : : else
211 : : {
212 [ - + ][ - + ]: 33335 : Assert(esign != 0);
[ - - ]
213 : : // update lower/upper
214 [ + + ]: 33335 : if (esign == -1)
215 : : {
216 : 15896 : upper = curr;
217 : : }
218 [ + - ]: 17439 : else if (esign == 1)
219 : : {
220 : 17439 : lower = curr;
221 : : }
222 : : }
223 [ + + ]: 35922 : } while (cret.isNull());
224 : 2587 : return cret;
225 : 4158 : }
226 : :
227 : 4158 : void printRationalApprox(const char* c, Node cr, unsigned prec)
228 : : {
229 [ - + ]: 4158 : if (!cr.isConst())
230 : : {
231 : 0 : DebugUnhandled() << "printRationalApprox: non-constant input " << cr;
232 : : Trace(c) << cr;
233 : : return;
234 : : }
235 : 4158 : Node ca = getApproximateConstant(cr, true, prec);
236 [ + + ]: 4158 : if (ca != cr)
237 : : {
238 [ + - ]: 2587 : Trace(c) << "(+ ";
239 : : }
240 [ + - ]: 4158 : Trace(c) << ca;
241 [ + + ]: 4158 : if (ca != cr)
242 : : {
243 [ + - ]: 2587 : Trace(c) << " [0,10^" << prec << "])";
244 : : }
245 : 4158 : }
246 : :
247 : 106 : Node mkBounded(Node l, Node a, Node u)
248 : : {
249 : : return NodeManager::mkNode(Kind::AND,
250 : 212 : NodeManager::mkNode(Kind::GEQ, a, l),
251 : 318 : NodeManager::mkNode(Kind::LEQ, a, u));
252 : : }
253 : :
254 : 1566 : Rational leastIntGreaterThan(const Rational& q) { return q.floor() + 1; }
255 : :
256 : 20742 : Rational greatestIntLessThan(const Rational& q) { return q.ceiling() - 1; }
257 : :
258 : 12470 : Node negateProofLiteral(TNode n)
259 : : {
260 [ - - ][ + + ]: 12470 : switch (n.getKind())
[ + - ]
261 : : {
262 : 0 : case Kind::GT:
263 : : {
264 : 0 : return NodeManager::mkNode(Kind::LEQ, n[0], n[1]);
265 : : }
266 : 0 : case Kind::LT:
267 : : {
268 : 0 : return NodeManager::mkNode(Kind::GEQ, n[0], n[1]);
269 : : }
270 : 4860 : case Kind::LEQ:
271 : : {
272 : 4860 : return NodeManager::mkNode(Kind::GT, n[0], n[1]);
273 : : }
274 : 4597 : case Kind::GEQ:
275 : : {
276 : 4597 : return NodeManager::mkNode(Kind::LT, n[0], n[1]);
277 : : }
278 : 3013 : case Kind::EQUAL:
279 : : case Kind::NOT:
280 : : {
281 : 3013 : return n.negate();
282 : : }
283 : 0 : default: Unhandled() << n;
284 : : }
285 : : }
286 : :
287 : 114 : Node multConstants(const Node& c1, const Node& c2)
288 : : {
289 [ + - ][ + - ]: 114 : Assert(!c1.isNull() && c1.isConst());
[ - + ][ - + ]
[ - - ]
290 [ + - ][ + - ]: 114 : Assert(!c2.isNull() && c2.isConst());
[ - + ][ - + ]
[ - - ]
291 : 114 : NodeManager* nm = c1.getNodeManager();
292 : : // real type if either has type real
293 : 114 : TypeNode tn = c1.getType();
294 [ + - ]: 114 : if (tn.isInteger())
295 : : {
296 : 114 : tn = c2.getType();
297 : : }
298 [ - + ][ - + ]: 114 : Assert(tn.isRealOrInt());
[ - - ]
299 : : return nm->mkConstRealOrInt(
300 : 342 : tn, Rational(c1.getConst<Rational>() * c2.getConst<Rational>()));
301 : 114 : }
302 : :
303 : 250601 : Node mkEquality(const Node& a, const Node& b)
304 : : {
305 [ - + ][ - + ]: 250601 : Assert(a.getType().isRealOrInt());
[ - - ]
306 [ - + ][ - + ]: 250601 : Assert(b.getType().isRealOrInt());
[ - - ]
307 : : // if they have the same type, just make them equal
308 [ + + ]: 250601 : if (a.getType() == b.getType())
309 : : {
310 : 237964 : return NodeManager::mkNode(Kind::EQUAL, a, b);
311 : : }
312 : : // otherwise subtract and set equal to zero
313 : 25274 : Node diff = NodeManager::mkNode(Kind::SUB, a, b);
314 : 12637 : return NodeManager::mkNode(Kind::EQUAL, diff, mkZero(diff.getType()));
315 : 12637 : }
316 : :
317 : 18250 : Node castToReal(NodeManager* nm, const Node& n)
318 : : {
319 : 18250 : return n.isConst() ? nm->mkConstReal(n.getConst<Rational>())
320 [ + + ][ + + ]: 18250 : : nm->mkNode(Kind::TO_REAL, n);
[ - - ]
321 : : }
322 : :
323 : 164474 : std::pair<Node,Node> mkSameType(const Node& a, const Node& b)
324 : : {
325 : 164474 : TypeNode at = a.getType();
326 : 164474 : TypeNode bt = b.getType();
327 [ + + ]: 164474 : if (at == bt)
328 : : {
329 : 163412 : return {a, b};
330 : : }
331 [ + + ][ + - ]: 1062 : if (at.isInteger() && bt.isReal())
[ + + ]
332 : : {
333 : 468 : return {NodeManager::mkNode(Kind::TO_REAL, a), b};
334 : : }
335 [ + - ][ + - ]: 828 : Assert(at.isReal() && bt.isInteger());
[ - + ][ - + ]
[ - - ]
336 : 1656 : return {a, NodeManager::mkNode(Kind::TO_REAL, b)};
337 : 164474 : }
338 : :
339 : : /* ------------------------------------------------------------------------- */
340 : :
341 : 82 : Node eliminateBv2Nat(TNode node)
342 : : {
343 : 82 : const unsigned size = bv::utils::getSize(node[0]);
344 : 82 : NodeManager* const nm = node.getNodeManager();
345 : 82 : const Node z = nm->mkConstInt(Rational(0));
346 : 82 : const Node bvone = bv::utils::mkOne(nm, 1);
347 : :
348 : 82 : Integer i = 1;
349 : 82 : std::vector<Node> children;
350 [ + + ]: 598 : for (unsigned bit = 0; bit < size; ++bit, i *= 2)
351 : : {
352 : : Node cond =
353 : : nm->mkNode(Kind::EQUAL,
354 : 1032 : nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
355 : 1548 : bvone);
356 : 516 : children.push_back(
357 : 1032 : nm->mkNode(Kind::ITE, cond, nm->mkConstInt(Rational(i)), z));
358 : 516 : }
359 : : // avoid plus with one child
360 [ + + ]: 164 : return children.size() == 1 ? children[0] : nm->mkNode(Kind::ADD, children);
361 : 82 : }
362 : :
363 : 64 : Node eliminateInt2Bv(TNode node)
364 : : {
365 : 64 : const uint32_t size = node.getOperator().getConst<IntToBitVector>().d_size;
366 : 64 : NodeManager* const nm = node.getNodeManager();
367 : 64 : const Node bvzero = bv::utils::mkZero(nm, 1);
368 : 64 : const Node bvone = bv::utils::mkOne(nm, 1);
369 : :
370 : 64 : std::vector<Node> v;
371 : 64 : Integer i = 2;
372 [ + + ]: 328 : while (v.size() < size)
373 : : {
374 : : Node cond = nm->mkNode(
375 : : Kind::GEQ,
376 : 528 : nm->mkNode(
377 : 528 : Kind::INTS_MODULUS_TOTAL, node[0], nm->mkConstInt(Rational(i))),
378 : 1056 : nm->mkConstInt(Rational(i, 2)));
379 : 264 : v.push_back(nm->mkNode(Kind::ITE, cond, bvone, bvzero));
380 : 264 : i *= 2;
381 : 264 : }
382 [ - + ]: 64 : if (v.size() == 1)
383 : : {
384 : 0 : return v[0];
385 : : }
386 : 64 : NodeBuilder result(nm, Kind::BITVECTOR_CONCAT);
387 : 64 : result.append(v.rbegin(), v.rend());
388 : 64 : return Node(result);
389 : 64 : }
390 : :
391 : : } // namespace arith
392 : : } // namespace theory
393 : : } // namespace cvc5::internal
|
