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 : : * Utilities for rewriting atoms in the arithmetic rewriter.
11 : : */
12 : :
13 : : #include "theory/arith/rewriter/rewrite_atom.h"
14 : :
15 : : #include "base/check.h"
16 : : #include "theory/arith/rewriter/node_utils.h"
17 : :
18 : : namespace cvc5::internal {
19 : : namespace theory {
20 : : namespace arith {
21 : : namespace rewriter {
22 : :
23 : : namespace {
24 : :
25 : : /**
26 : : * Evaluate the given relation based on values l and r. Expects that the
27 : : * relational operators `operator<(L,R)`, `operator==(L,R)`, etc are defined.
28 : : */
29 : : template <typename L>
30 : 595685 : bool evaluateRelation(Kind rel, const L& l, const L& r)
31 : : {
32 [ - + ][ + - ]: 595685 : switch (rel)
[ + - ][ - ]
33 : : {
34 : 0 : case Kind::LT: return l < r;
35 : 59406 : case Kind::LEQ: return l <= r;
36 : 261594 : case Kind::EQUAL: return l == r;
37 : 0 : case Kind::DISTINCT: return l != r;
38 : 274685 : case Kind::GEQ: return l >= r;
39 : 0 : case Kind::GT: return l > r;
40 : 0 : default: Unreachable(); return false;
41 : : }
42 : : }
43 : :
44 : 7786386 : auto getLTermIt(Sum& sum)
45 : : {
46 : 7786386 : auto ltermit = sum.begin();
47 [ + + ]: 7786386 : if (ltermit->first.isConst())
48 : : {
49 : 3897972 : ++ltermit;
50 : : }
51 : 7786386 : return ltermit;
52 : : }
53 : :
54 : 2786993 : auto& getLTerm(Sum& sum)
55 : : {
56 [ - + ][ - + ]: 2786993 : Assert(getLTermIt(sum) != sum.end());
[ - - ]
57 : 2786993 : return *getLTermIt(sum);
58 : : }
59 : :
60 : : /**
61 : : * Normalize the sum, making the leading coefficient to be one or minus one.
62 : : */
63 : 945488 : void normalizeLCoeffAbsOne(Sum& sum)
64 : : {
65 [ - + ]: 1866352 : if (sum.empty()) return;
66 [ + + ]: 945488 : if (sum.size() == 1)
67 : : {
68 : 129842 : auto& front = *sum.begin();
69 : : // Trivial if there is only one summand
70 [ + + ]: 129842 : front.second = Integer(front.second.sgn() > 0 ? 1 : -1);
71 : 129842 : return;
72 : : }
73 : : // LCoeff is first coefficient of non-constant monomial
74 : 815646 : RealAlgebraicNumber lcoeff = getLTerm(sum).second;
75 : : ;
76 [ + + ]: 815646 : if (lcoeff.sgn() < 0)
77 : : {
78 : 456962 : lcoeff = -lcoeff;
79 : : }
80 [ + + ]: 815646 : if (lcoeff.isOne()) return;
81 [ + + ]: 112130 : for (auto& s : sum)
82 : : {
83 : 87506 : s.second = s.second / lcoeff;
84 : : }
85 [ + + ]: 815646 : }
86 : :
87 : : /**
88 : : * Normalize the sum, making all coefficients integral and their gcd one.
89 : : * If followLCoeffSign is true, the leading coefficient is made positive,
90 : : * possibly negating all other coefficients. If this is the case return true to
91 : : * indicate that the relational operator needs to be negated.
92 : : * Otherwise return false.
93 : : */
94 : 3964181 : bool normalizeGCDLCM(Sum& sum, bool followLCoeffSign = false)
95 : : {
96 [ + + ]: 3964181 : if (sum.empty()) return false;
97 : 3963666 : Integer denLCM(1);
98 : 3963666 : Integer numGCD;
99 : 3963666 : auto it = sum.begin();
100 [ + + ]: 3963666 : if (!it->first.isConst())
101 : : {
102 : 2043970 : Rational r = it->second.toRational();
103 : 2043970 : denLCM = r.getDenominator();
104 : 2043970 : numGCD = r.getNumerator().abs();
105 : 2043970 : }
106 : 3963666 : ++it;
107 [ + + ]: 8435895 : for (; it != sum.end(); ++it)
108 : : {
109 [ - + ]: 4472229 : if (it->first.isConst()) continue;
110 [ - + ][ - + ]: 4472229 : Assert(it->second.isRational());
[ - - ]
111 : 4472229 : Rational r = it->second.toRational();
112 : 4472229 : denLCM = denLCM.lcm(r.getDenominator());
113 [ + + ]: 4472229 : if (numGCD.isZero())
114 : 1906945 : numGCD = r.getNumerator().abs();
115 : : else
116 : 2565284 : numGCD = numGCD.gcd(r.getNumerator().abs());
117 : 4472229 : }
118 [ + + ]: 3963666 : if (numGCD.isZero()) return false;
119 : 3950915 : Rational mult(denLCM, numGCD);
120 : :
121 : 3950915 : bool negate = false;
122 [ + + ]: 3950915 : if (followLCoeffSign)
123 : : {
124 [ + + ]: 1971347 : if (getLTerm(sum).second.sgn() < 0)
125 : : {
126 : 333924 : negate = true;
127 : 333924 : mult = -mult;
128 : : }
129 : : }
130 : :
131 [ + + ]: 12374059 : for (auto& s : sum)
132 : : {
133 : 8423144 : s.second *= mult;
134 : : }
135 : 3950915 : return negate;
136 : 3963666 : }
137 : :
138 : 1907089 : std::pair<Node, RealAlgebraicNumber> removeMinAbsCoeff(NodeManager* nm,
139 : : Sum& sum)
140 : : {
141 : 1907089 : auto minit = getLTermIt(sum);
142 [ + + ]: 5120568 : for (auto it = minit; it != sum.end(); ++it)
143 : : {
144 [ - + ]: 3213479 : if (it->first.isConst()) continue;
145 [ + + ]: 3213479 : if (it->second.toRational().absCmp(minit->second.toRational()) < 0)
146 : : {
147 : 28162 : minit = it;
148 : : }
149 : : }
150 [ + + ]: 1907089 : if (minit == sum.end())
151 : : {
152 : 11840 : return std::make_pair(mkConst(nm, Integer(1)), Integer(0));
153 : : }
154 [ - + ][ - + ]: 1901169 : Assert(minit != sum.end());
[ - - ]
155 : 1901169 : auto res = *minit;
156 : 1901169 : sum.erase(minit);
157 : 1901169 : return res;
158 : 1901169 : }
159 : :
160 : 3000608 : RealAlgebraicNumber removeConstant(Sum& sum)
161 : : {
162 : 3000608 : RealAlgebraicNumber res;
163 [ + + ]: 3000608 : if (!sum.empty())
164 : : {
165 : 3000093 : auto constantit = sum.begin();
166 [ + + ]: 3000093 : if (constantit->first.isConst())
167 : : {
168 [ - + ][ - + ]: 1561573 : Assert(constantit->first.getConst<Rational>().isOne());
[ - - ]
169 : 1561573 : res = constantit->second;
170 : 1561573 : sum.erase(constantit);
171 : : }
172 : : }
173 : 3000608 : return res;
174 : 0 : }
175 : :
176 : 305311 : std::pair<Node, RealAlgebraicNumber> removeLTerm(NodeManager* nm, Sum& sum)
177 : : {
178 : 305311 : auto it = getLTermIt(sum);
179 [ - + ]: 305311 : if (it == sum.end())
180 : : {
181 : 0 : return std::make_pair(mkConst(nm, Integer(1)), Integer(0));
182 : : }
183 [ - + ][ - + ]: 305311 : Assert(it != sum.end());
[ - - ]
184 : 305311 : auto res = *it;
185 : 305311 : sum.erase(it);
186 : 305311 : return res;
187 : 305311 : }
188 : :
189 : : } // namespace
190 : :
191 : 10943157 : std::optional<bool> tryEvaluateRelation(Kind rel, TNode left, TNode right)
192 : : {
193 [ + + ]: 10943157 : if (left.isConst())
194 : : {
195 : 830185 : const Rational& l = left.getConst<Rational>();
196 [ + + ]: 830185 : if (right.isConst())
197 : : {
198 : 595464 : const Rational& r = right.getConst<Rational>();
199 : 595464 : return evaluateRelation(rel, l, r);
200 : : }
201 [ + + ]: 234721 : else if (right.getKind() == Kind::REAL_ALGEBRAIC_NUMBER)
202 : : {
203 : : const RealAlgebraicNumber& r =
204 : 1 : right.getOperator().getConst<RealAlgebraicNumber>();
205 : 1 : return evaluateRelation(rel, RealAlgebraicNumber(l), r);
206 : : }
207 : : }
208 [ + + ]: 10112972 : else if (left.getKind() == Kind::REAL_ALGEBRAIC_NUMBER)
209 : : {
210 : : const RealAlgebraicNumber& l =
211 : 223 : left.getOperator().getConst<RealAlgebraicNumber>();
212 [ + + ]: 223 : if (right.isConst())
213 : : {
214 : 220 : const Rational& r = right.getConst<Rational>();
215 : 220 : return evaluateRelation(rel, l, RealAlgebraicNumber(r));
216 : : }
217 [ - + ]: 3 : else if (right.getKind() == Kind::REAL_ALGEBRAIC_NUMBER)
218 : : {
219 : : const RealAlgebraicNumber& r =
220 : 0 : right.getOperator().getConst<RealAlgebraicNumber>();
221 : 0 : return evaluateRelation(rel, l, r);
222 : : }
223 : : }
224 : 10347472 : return {};
225 : : }
226 : :
227 : 12449964 : std::optional<bool> tryEvaluateRelationReflexive(Kind rel,
228 : : TNode left,
229 : : TNode right)
230 : : {
231 [ + + ]: 12449964 : if (left == right)
232 : : {
233 [ + + ][ + - ]: 271887 : switch (rel)
[ + + ][ - ]
234 : : {
235 : 453 : case Kind::LT: return false;
236 : 9434 : case Kind::LEQ: return true;
237 : 180194 : case Kind::EQUAL: return true;
238 : 0 : case Kind::DISTINCT: return false;
239 : 81282 : case Kind::GEQ: return true;
240 : 524 : case Kind::GT: return false;
241 : 0 : default:;
242 : : }
243 : : }
244 : 12178077 : return {};
245 : : }
246 : :
247 : 5430382 : Node buildRelation(Kind kind, Node left, Node right, bool negate)
248 : : {
249 [ + + ]: 5430382 : if (auto response = tryEvaluateRelation(kind, left, right); response)
250 : : {
251 : 51980 : return mkConst(left.getNodeManager(), *response != negate);
252 : : }
253 [ + + ]: 5378402 : if (negate)
254 : : {
255 : 1410704 : return NodeManager::mkNode(kind, left, right).notNode();
256 : : }
257 : 4673050 : return NodeManager::mkNode(kind, left, right);
258 : : }
259 : :
260 : 1909061 : Node buildIntegerEquality(NodeManager* nm, Sum&& sum)
261 : : {
262 [ + - ]: 3818122 : Trace("arith-rewriter") << "building integer equality from " << sum
263 : 1909061 : << std::endl;
264 : 1909061 : normalizeGCDLCM(sum);
265 : :
266 [ + - ]: 1909061 : Trace("arith-rewriter::debug") << "\tnormalized to " << sum << std::endl;
267 : :
268 : 1909061 : const auto& constant = *sum.begin();
269 [ + + ]: 1909061 : if (constant.first.isConst())
270 : : {
271 [ - + ][ - + ]: 739467 : Assert(constant.second.isRational());
[ - - ]
272 [ + + ]: 739467 : if (!constant.second.toRational().isIntegral())
273 : : {
274 [ + - ]: 3944 : Trace("arith-rewriter::debug")
275 : 1972 : << "\thas non-integer constant, thus false" << std::endl;
276 : 1972 : return mkConst(nm, false);
277 : : }
278 : : }
279 : :
280 : 1907089 : auto minabscoeff = removeMinAbsCoeff(nm, sum);
281 [ + - ]: 3814178 : Trace("arith-rewriter::debug") << "\tremoved min abs coeff " << minabscoeff
282 : 1907089 : << ", left with " << sum << std::endl;
283 [ + + ]: 1907089 : if (minabscoeff.second.sgn() < 0)
284 : : {
285 : : // move minabscoeff goes to the right and switch lhs and rhs
286 : 324065 : minabscoeff.second = -minabscoeff.second;
287 : : }
288 : : else
289 : : {
290 : : // move the sum to the right
291 [ + + ]: 3300309 : for (auto& s : sum) s.second = -s.second;
292 : : }
293 : 1907089 : Node left = mkMultTerm(minabscoeff.second, minabscoeff.first);
294 : :
295 [ + - ]: 3814178 : Trace("arith-rewriter::debug")
296 : 1907089 : << "\tbuilding " << left << " = " << sum << std::endl;
297 : :
298 : 1907089 : Node rhs = collectSum(nm, sum);
299 [ - + ][ - + ]: 1907089 : Assert(left.getType().isInteger());
[ - - ]
300 [ - + ][ - + ]: 1907089 : Assert(rhs.getType().isInteger());
[ - - ]
301 : 1907089 : return buildRelation(Kind::EQUAL, left, rhs);
302 : 1907089 : }
303 : :
304 : 305311 : Node buildRealEquality(NodeManager* nm, Sum&& sum)
305 : : {
306 [ + - ]: 305311 : Trace("arith-rewriter") << "building real equality from " << sum << std::endl;
307 : 305311 : auto lterm = removeLTerm(nm, sum);
308 [ - + ]: 305311 : if (lterm.second.isZero())
309 : : {
310 : : // Use zero to ensure deterministic node ID assignments
311 : 0 : Node zero = mkConst(nm, Integer(0));
312 : 0 : return buildRelation(Kind::EQUAL, zero, collectSum(nm, sum));
313 : 0 : }
314 : 305311 : RealAlgebraicNumber lcoeff = -lterm.second;
315 [ + + ]: 658998 : for (auto& s : sum)
316 : : {
317 : 353687 : s.second = s.second / lcoeff;
318 : : }
319 : : // Ensure real for both sides.
320 : 305311 : Node lhs = lterm.first;
321 : 305311 : Node rhs = collectSum(nm, sum);
322 : 305311 : Node lhsr = ensureReal(lhs);
323 : 305311 : Node rhsr = ensureReal(rhs);
324 [ + + ][ + - ]: 305311 : if (lhsr != lhs && rhsr != rhs)
[ + + ]
325 : : {
326 : : // if both were changed, then this implies we could make an integer equality
327 : : // instead.
328 [ - + ][ - + ]: 3 : Assert(lhs.getType().isInteger());
[ - - ]
329 [ - + ][ - + ]: 3 : Assert(rhs.getType().isInteger());
[ - - ]
330 : 3 : return buildRelation(Kind::EQUAL, lhs, rhs);
331 : : }
332 : 305308 : Assert(lhsr.getType().isReal() || lhsr.getType().isFullyAbstract());
333 : 305308 : Assert(rhsr.getType().isReal() || rhsr.getType().isFullyAbstract());
334 : 305308 : return buildRelation(Kind::EQUAL, lhsr, rhsr);
335 : 305311 : }
336 : :
337 : 1809210 : Node buildIntegerInequality(NodeManager* nm, Sum&& sum, Kind k)
338 : : {
339 [ + - ]: 3618420 : Trace("arith-rewriter") << "building integer inequality from " << sum
340 : 1809210 : << std::endl;
341 : 1809210 : bool negate = normalizeGCDLCM(sum, true);
342 : :
343 [ + + ]: 1809210 : if (negate)
344 : : {
345 [ + - ]: 284350 : k = (k == Kind::GEQ) ? Kind::GT : Kind::GEQ;
346 : : }
347 : :
348 : 1809210 : RealAlgebraicNumber constant = removeConstant(sum);
349 [ - + ][ - + ]: 1809210 : Assert(constant.isRational());
[ - - ]
350 : 1809210 : Rational rhs = -constant.toRational();
351 : :
352 [ + + ][ + + ]: 1809210 : if (rhs.isIntegral() && k == Kind::GT)
[ + + ]
353 : : {
354 : 282854 : rhs += 1;
355 : : }
356 : : else
357 : : {
358 : 1526356 : rhs = rhs.ceiling();
359 : : }
360 : : // Use rhsNode to ensure deterministic node ID assignments
361 : 1809210 : Node rhsNode = nm->mkConstInt(rhs);
362 : 5427630 : return buildRelation(Kind::GEQ, collectSum(nm, sum), rhsNode, negate);
363 : 1809210 : }
364 : :
365 : 945488 : Node buildRealInequality(NodeManager* nm, Sum&& sum, Kind k)
366 : : {
367 [ + - ]: 1890976 : Trace("arith-rewriter") << "building real inequality from " << sum
368 : 945488 : << std::endl;
369 : 945488 : normalizeLCoeffAbsOne(sum);
370 : 1890976 : Node rhs = mkConst(nm, -removeConstant(sum));
371 : 2836464 : return buildRelation(k, collectSum(nm, sum), rhs);
372 : 945488 : }
373 : :
374 : 245740 : std::pair<Node, Node> decomposeSum(NodeManager* nm,
375 : : Sum&& sum,
376 : : bool& negated,
377 : : bool followLCoeffSign)
378 : : {
379 : 245740 : negated = normalizeGCDLCM(sum, followLCoeffSign);
380 : 245740 : RealAlgebraicNumber constant = removeConstant(sum);
381 [ - + ][ - + ]: 245740 : Assert(constant.isRational());
[ - - ]
382 : 245740 : Node c = nm->mkConstReal(constant.toRational());
383 : 245740 : Node t = collectSum(nm, sum);
384 : 491480 : return std::pair<Node, Node>(t, c);
385 : 245740 : }
386 : :
387 : 77325 : std::pair<Node, Node> decomposeSum(NodeManager* nm, Sum&& sum)
388 : : {
389 : 77325 : bool negated = false;
390 : 154650 : return decomposeSum(nm, std::move(sum), negated, false);
391 : : }
392 : :
393 : 170 : std::pair<Node, Node> decomposeRelation(NodeManager* nm,
394 : : const Node& a,
395 : : const Node& b)
396 : : {
397 [ + + ]: 170 : Node ar = a.getKind() == Kind::TO_REAL ? a[0] : a;
398 [ + + ]: 170 : Node br = b.getKind() == Kind::TO_REAL ? b[0] : b;
399 : 170 : rewriter::Sum sum;
400 : 170 : rewriter::addToSum(sum, ar, false);
401 : 170 : rewriter::addToSum(sum, br, true);
402 : : // decompose the sum into a non-constant and constant part
403 : 170 : normalizeGCDLCM(sum);
404 : 170 : RealAlgebraicNumber constant = removeConstant(sum);
405 [ - + ][ - + ]: 170 : Assert(constant.isRational());
[ - - ]
406 : : // negate the constant
407 : 340 : Node c = nm->mkConstReal(-constant.toRational());
408 : 170 : Node t = collectSum(nm, sum);
409 : 340 : return std::pair<Node, Node>(t, c);
410 : 170 : }
411 : :
412 : : } // namespace rewriter
413 : : } // namespace arith
414 : : } // namespace theory
415 : : } // namespace cvc5::internal
|
