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 : : * Common functions for dealing with nodes.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
16 : : #define CVC5__THEORY__ARITH__ARITH_UTILITIES_H
17 : :
18 : : #include <unordered_map>
19 : : #include <unordered_set>
20 : : #include <vector>
21 : :
22 : : #include "context/cdhashset.h"
23 : : #include "expr/node.h"
24 : : #include "expr/subs.h"
25 : : #include "util/dense_map.h"
26 : : #include "util/integer.h"
27 : : #include "util/rational.h"
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace arith {
32 : :
33 : : // Sets of Nodes
34 : : typedef std::unordered_set<Node> NodeSet;
35 : : typedef std::unordered_set<TNode> TNodeSet;
36 : : typedef context::CDHashSet<Node> CDNodeSet;
37 : :
38 : 11503 : inline Node mkBoolNode(NodeManager* nm, bool b) { return nm->mkConst<bool>(b); }
39 : :
40 : : /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
41 : 163994736 : inline bool isRelationOperator(Kind k)
42 : : {
43 [ + + ]: 163994736 : switch (k)
44 : : {
45 : 7260253 : case Kind::LT:
46 : : case Kind::LEQ:
47 : : case Kind::EQUAL:
48 : : case Kind::GEQ:
49 : 7260253 : case Kind::GT: return true;
50 : 156734483 : default: return false;
51 : : }
52 : : }
53 : :
54 : : /**
55 : : * Given a relational kind, k, return the kind k' s.t.
56 : : * swapping the lefthand and righthand side is equivalent.
57 : : *
58 : : * The following equivalence should hold,
59 : : * (k l r) <=> (k' r l)
60 : : */
61 : 197533 : inline Kind reverseRelationKind(Kind k)
62 : : {
63 [ + + ][ + + ]: 197533 : switch (k)
[ + - ]
64 : : {
65 : 21007 : case Kind::LT: return Kind::GT;
66 : 3255 : case Kind::LEQ: return Kind::GEQ;
67 : 37571 : case Kind::EQUAL: return Kind::EQUAL;
68 : 98583 : case Kind::GEQ: return Kind::LEQ;
69 : 37117 : case Kind::GT: return Kind::LT;
70 : :
71 : 0 : default: Unreachable();
72 : : }
73 : : }
74 : :
75 : 0 : inline bool evaluateConstantPredicate(Kind k,
76 : : const Rational& left,
77 : : const Rational& right)
78 : : {
79 [ - - ][ - - ]: 0 : switch (k)
[ - - ]
80 : : {
81 : 0 : case Kind::LT: return left < right;
82 : 0 : case Kind::LEQ: return left <= right;
83 : 0 : case Kind::EQUAL: return left == right;
84 : 0 : case Kind::GEQ: return left >= right;
85 : 0 : case Kind::GT: return left > right;
86 : 0 : default: Unreachable(); return true;
87 : : }
88 : : }
89 : :
90 : : /**
91 : : * Returns the appropriate coefficient for the infinitesimal given the kind
92 : : * for an arithmetic atom inorder to represent strict inequalities as
93 : : * inequalities. x < c becomes x <= c + (-1) * \f$ \delta \f$ x > c becomes
94 : : * x >= x + ( 1) * \f$ \delta \f$ Non-strict inequalities have a coefficient of
95 : : * zero.
96 : : */
97 : 2404398 : inline int deltaCoeff(Kind k)
98 : : {
99 [ + - ][ + ]: 2404398 : switch (k)
100 : : {
101 : 650885 : case Kind::LT: return -1;
102 : 0 : case Kind::GT: return 1;
103 : 1753513 : default: return 0;
104 : : }
105 : : }
106 : :
107 : : /**
108 : : * Given a literal to TheoryArith return a single kind to
109 : : * to indicate its underlying structure.
110 : : * The function returns the following in each case:
111 : : * - (K left right) -> K where is a wildcard for EQUAL, LT, GT, LEQ, or GEQ:
112 : : * - (NOT (EQUAL left right)) -> DISTINCT
113 : : * - (NOT (LEQ left right)) -> GT
114 : : * - (NOT (GEQ left right)) -> LT
115 : : * - (NOT (LT left right)) -> GEQ
116 : : * - (NOT (GT left right)) -> LEQ
117 : : * If none of these match, it returns UNDEFINED_KIND.
118 : : */
119 : 2605 : inline Kind oldSimplifiedKind(TNode literal)
120 : : {
121 [ + - ][ - ]: 2605 : switch (literal.getKind())
122 : : {
123 : 2605 : case Kind::LT:
124 : : case Kind::GT:
125 : : case Kind::LEQ:
126 : : case Kind::GEQ:
127 : 2605 : case Kind::EQUAL: return literal.getKind();
128 : 0 : case Kind::NOT:
129 : : {
130 : 0 : TNode atom = literal[0];
131 : 0 : switch (atom.getKind())
132 : : {
133 : 0 : case Kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
134 : 0 : return Kind::GT;
135 : 0 : case Kind::GEQ: //(not (GEQ x c)) <=> (LT x c)
136 : 0 : return Kind::LT;
137 : 0 : case Kind::LT: //(not (LT x c)) <=> (GEQ x c)
138 : 0 : return Kind::GEQ;
139 : 0 : case Kind::GT: //(not (GT x c) <=> (LEQ x c)
140 : 0 : return Kind::LEQ;
141 : 0 : case Kind::EQUAL: return Kind::DISTINCT;
142 : 0 : default: Unreachable(); return Kind::UNDEFINED_KIND;
143 : : }
144 : 0 : }
145 : 0 : default: Unreachable(); return Kind::UNDEFINED_KIND;
146 : : }
147 : : }
148 : :
149 : 143863 : inline Kind negateKind(Kind k)
150 : : {
151 [ - - ][ + + ]: 143863 : switch (k)
[ + - ][ - ]
152 : : {
153 : 0 : case Kind::LT: return Kind::GEQ;
154 : 0 : case Kind::GT: return Kind::LEQ;
155 : 58404 : case Kind::LEQ: return Kind::GT;
156 : 85451 : case Kind::GEQ: return Kind::LT;
157 : 8 : case Kind::EQUAL: return Kind::DISTINCT;
158 : 0 : case Kind::DISTINCT: return Kind::EQUAL;
159 : 0 : default: return Kind::UNDEFINED_KIND;
160 : : }
161 : : }
162 : :
163 : : inline Node negateConjunctionAsClause(TNode conjunction)
164 : : {
165 : : Assert(conjunction.getKind() == Kind::AND);
166 : : NodeBuilder orBuilder(conjunction.getNodeManager(), Kind::OR);
167 : :
168 : : for (TNode::iterator i = conjunction.begin(), end = conjunction.end();
169 : : i != end;
170 : : ++i)
171 : : {
172 : : TNode child = *i;
173 : : Node negatedChild = NodeBuilder(conjunction.getNodeManager(), Kind::NOT)
174 : : << (child);
175 : : orBuilder << negatedChild;
176 : : }
177 : : return orBuilder;
178 : : }
179 : :
180 : : inline Node maybeUnaryConvert(NodeBuilder& builder)
181 : : {
182 : : Assert(builder.getKind() == Kind::OR || builder.getKind() == Kind::AND
183 : : || builder.getKind() == Kind::ADD || builder.getKind() == Kind::MULT);
184 : : Assert(builder.getNumChildren() >= 1);
185 : : if (builder.getNumChildren() == 1)
186 : : {
187 : : return builder[0];
188 : : }
189 : : else
190 : : {
191 : : return builder;
192 : : }
193 : : }
194 : :
195 : 7661 : inline void flattenAnd(Node n, std::vector<TNode>& out)
196 : : {
197 [ - + ][ - + ]: 7661 : Assert(n.getKind() == Kind::AND);
[ - - ]
198 [ + + ]: 34474 : for (Node::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i)
199 : : {
200 : 26813 : Node curr = *i;
201 [ + + ]: 26813 : if (curr.getKind() == Kind::AND)
202 : : {
203 : 3609 : flattenAnd(curr, out);
204 : : }
205 : : else
206 : : {
207 : 23204 : out.push_back(curr);
208 : : }
209 : 26813 : }
210 : 7661 : }
211 : :
212 : 4052 : inline Node flattenAnd(Node n)
213 : : {
214 : 4052 : std::vector<TNode> out;
215 : 4052 : flattenAnd(n, out);
216 : 8104 : return n.getNodeManager()->mkNode(Kind::AND, out);
217 : 4052 : }
218 : :
219 : : /** Make zero of the given type */
220 : : Node mkZero(const TypeNode& tn);
221 : :
222 : : /** Is n (integer or real) zero? */
223 : : bool isZero(const Node& n);
224 : :
225 : : /** Make one of the given type, maybe negated */
226 : : Node mkOne(const TypeNode& tn, bool isNeg = false);
227 : :
228 : : // Returns an node that is the identity of a select few kinds.
229 : 6305 : inline Node getIdentityType(const TypeNode& tn, Kind k)
230 : : {
231 [ - + ][ - ]: 6305 : switch (k)
232 : : {
233 : 0 : case Kind::ADD: return mkZero(tn);
234 : 6305 : case Kind::MULT:
235 : 6305 : case Kind::NONLINEAR_MULT: return NodeManager::mkConstRealOrInt(tn, 1);
236 : 0 : default: Unreachable(); return Node::null(); // silence warning
237 : : }
238 : : }
239 : :
240 : 4665213 : inline Node mkAndFromBuilder(NodeManager* nm, NodeBuilder& nb)
241 : : {
242 [ - + ][ - + ]: 4665213 : Assert(nb.getKind() == Kind::AND);
[ - - ]
243 [ - + ][ + ]: 4665213 : switch (nb.getNumChildren())
244 : : {
245 : 0 : case 0: return mkBoolNode(nm, true);
246 : 3309794 : case 1: return nb[0];
247 : 1355419 : default: return (Node)nb;
248 : : }
249 : : }
250 : :
251 : 73468 : inline Node safeConstructNaryType(const TypeNode& tn,
252 : : Kind k,
253 : : const std::vector<Node>& children)
254 : : {
255 [ + + ][ + ]: 73468 : switch (children.size())
256 : : {
257 : 6305 : case 0: return getIdentityType(tn, k);
258 : 47503 : case 1: return children[0];
259 : 19660 : default: return tn.getNodeManager()->mkNode(k, children);
260 : : }
261 : : }
262 : :
263 : : // Returns the multiplication of a and b.
264 : : inline Node mkMult(Node a, Node b)
265 : : {
266 : : return NodeManager::mkNode(Kind::MULT, a, b);
267 : : }
268 : :
269 : : // Return a constraint that is equivalent to term being is in the range
270 : : // [start, end). This includes start and excludes end.
271 : 908 : inline Node mkInRange(Node term, Node start, Node end)
272 : : {
273 : 1816 : Node above_start = NodeManager::mkNode(Kind::LEQ, start, term);
274 : 1816 : Node below_end = NodeManager::mkNode(Kind::LT, term, end);
275 : 1816 : return NodeManager::mkNode(Kind::AND, above_start, below_end);
276 : 908 : }
277 : :
278 : : // Creates an expression that constrains q to be equal to one of two expressions
279 : : // when n is 0 or not. Useful for division by 0 logic.
280 : : // (ite (= n 0) (= q if_zero) (= q not_zero))
281 : : inline Node mkOnZeroIte(Node n, Node q, Node if_zero, Node not_zero)
282 : : {
283 : : Node zero = mkZero(n.getType());
284 : : return n.eqNode(zero).iteNode({q.eqNode(if_zero), q.eqNode(not_zero)});
285 : : }
286 : :
287 : 3915 : inline Node mkPi(NodeManager* nm)
288 : : {
289 : 7830 : return nm->mkNullaryOperator(nm->realType(), Kind::PI);
290 : : }
291 : : /** Join kinds, where k1 and k2 are arithmetic relations returns an
292 : : * arithmetic relation ret such that
293 : : * if (a <k1> b) and (a <k2> b), then (a <ret> b).
294 : : */
295 : : Kind joinKinds(Kind k1, Kind k2);
296 : :
297 : : /** Transitive kinds, where k1 and k2 are arithmetic relations returns an
298 : : * arithmetic relation ret such that
299 : : * if (a <k1> b) and (b <k2> c) then (a <ret> c).
300 : : */
301 : : Kind transKinds(Kind k1, Kind k2);
302 : :
303 : : /** Is k a transcendental function kind? */
304 : : bool isTranscendentalKind(Kind k);
305 : :
306 : : /**
307 : : * Is k an extended non-linear function kind? These kinds are treated by the
308 : : * non-linear solver. We distinguish these kinds by the fact that they do not
309 : : * generate irrational outputs given rational inputs. Examples of extended
310 : : * non-linear kinds include IAND and POW2. All kinds that are non-linear
311 : : * and arithmetic should return true for either isTranscendentalKind or
312 : : * isExtendedNonLinearKind.
313 : : */
314 : : bool isExtendedNonLinearKind(Kind k);
315 : :
316 : : /**
317 : : * Get a lower/upper approximation of the constant r within the given
318 : : * level of precision. In other words, this returns a constant c' such that
319 : : * c' <= c <= c' + 1/(10^prec) if isLower is true, or
320 : : * c' + 1/(10^prec) <= c <= c' if isLower is false.
321 : : * where c' is a rational of the form n/d for some n and d <= 10^prec.
322 : : */
323 : : Node getApproximateConstant(Node c, bool isLower, unsigned prec);
324 : :
325 : : /** print rational approximation of cr with precision prec on trace c */
326 : : void printRationalApprox(const char* c, Node cr, unsigned prec = 5);
327 : :
328 : : /** Make the node u >= a ^ a >= l */
329 : : Node mkBounded(Node l, Node a, Node u);
330 : :
331 : : Rational leastIntGreaterThan(const Rational&);
332 : :
333 : : Rational greatestIntLessThan(const Rational&);
334 : :
335 : : /** Negates a node in arithmetic proof normal form. */
336 : : Node negateProofLiteral(TNode n);
337 : :
338 : : /**
339 : : * Return the result of multiplying constant integer or real nodes c1 and c2.
340 : : * The returned type is real if either have type real.
341 : : */
342 : : Node multConstants(const Node& c1, const Node& c2);
343 : :
344 : : /**
345 : : * Make the equality (= a b) or (= (- a b) zero) if a and b have different
346 : : * types, where zero has the same type as (- a b).
347 : : * Use this utility to ensure an equality is properly typed.
348 : : */
349 : : Node mkEquality(const Node& a, const Node& b);
350 : :
351 : : /**
352 : : * Return the real cast of n. If n is a constant integer, we return a
353 : : * constant real. Otherwise we apply TO_REAL to n.
354 : : */
355 : : Node castToReal(NodeManager* nm, const Node& n);
356 : :
357 : : /**
358 : : * Ensures that the returned pair has equal type, where a and b have
359 : : * real or integer type. We add TO_REAL if not.
360 : : */
361 : : std::pair<Node, Node> mkSameType(const Node& a, const Node& b);
362 : :
363 : : /**
364 : : * Returns the rewritten form of node, which is a term of the form bv2nat(x).
365 : : * The return value of this method is the integer sum:
366 : : * (+ ite( (= ((_ extract (n-1) (n-1)) x) 1) (^ 2 (n-1)) 0)
367 : : * ...
368 : : * ite( (= ((_ extract 0 0) x) 1) (^ 2 0) 0))
369 : : * where n is the bitwidth of x.
370 : : */
371 : : Node eliminateBv2Nat(TNode node);
372 : : /**
373 : : * Returns the rewritten form of node, which is a term of the form int2bv(x).
374 : : * The return value of this method is the concatenation term:
375 : : * (bvconcat ite( (>= (mod x (^ 2 n)) (^ 2 (n-1))) (_ bv1 1) (_ bv1 0))
376 : : * ...
377 : : * ite( (>= (mod x (^ 2 1)) (^ 2 0)) (_ bv1 1) (_ bv1 0)))
378 : : * where n is the bit-width of x.
379 : : */
380 : : Node eliminateInt2Bv(TNode node);
381 : :
382 : : } // namespace arith
383 : : } // namespace theory
384 : : } // namespace cvc5::internal
385 : :
386 : : #endif /* CVC5__THEORY__ARITH__ARITH_UTILITIES_H */
|
