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 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : :
16 : : #include "theory/arith/arith_rewriter.h"
17 : :
18 : : #include <optional>
19 : : #include <set>
20 : : #include <sstream>
21 : : #include <stack>
22 : : #include <vector>
23 : :
24 : : #include "expr/algorithm/flatten.h"
25 : : #include "expr/node_algorithm.h"
26 : : #include "smt/logic_exception.h"
27 : : #include "theory/arith/arith_msum.h"
28 : : #include "theory/arith/arith_utilities.h"
29 : : #include "theory/arith/operator_elim.h"
30 : : #include "theory/arith/rewriter/addition.h"
31 : : #include "theory/arith/rewriter/node_utils.h"
32 : : #include "theory/arith/rewriter/ordering.h"
33 : : #include "theory/arith/rewriter/rewrite_atom.h"
34 : : #include "theory/evaluator.h"
35 : : #include "theory/rewriter.h"
36 : : #include "theory/strings/arith_entail.h"
37 : : #include "theory/theory.h"
38 : : #include "util/bitvector.h"
39 : : #include "util/divisible.h"
40 : : #include "util/iand.h"
41 : : #include "util/real_algebraic_number.h"
42 : :
43 : : using namespace cvc5::internal::kind;
44 : :
45 : : namespace cvc5::internal {
46 : : namespace theory {
47 : : namespace arith {
48 : :
49 : : /**
50 : : * Flatten a node into a vector of its (direct or indirect) children, collecting
51 : : * how many times each child occurs in the sum.
52 : : * A sequence of kinds is given that indicate which kinds to traverse over.
53 : : * This method is similar to expr::algorithm::flatten but does not use a tree
54 : : * traversal. Instead it merges subterms, based on counting the number of
55 : : * occurrences, as a Rational.
56 : : * @param t The node to be flattened
57 : : * @param children The resulting list of children
58 : : * @param kinds A sequence of kinds to consider for flattening
59 : : */
60 : : template <typename... Kinds>
61 : 5402135 : bool flattenAndCollectSum(TNode t,
62 : : std::vector<std::pair<TNode, Rational>>& children,
63 : : Kinds... kinds)
64 : : {
65 [ + + ]: 5402135 : if (!expr::algorithm::canFlatten(t, kinds...))
66 : : {
67 : 4891519 : return false;
68 : : }
69 : : // Note we use an *ordered* map, where we assume that nodes are ordered by
70 : : // their id, where nodes constructed later have a larger id. This ensures
71 : : // we process nodes in the (reverse) order in which they constructed, newest
72 : : // nodes processed first, thus ensuring we process each node only once while
73 : : // flattening.
74 : 510616 : std::map<TNode, Rational> countMap;
75 : 510616 : countMap[t] = Rational(1);
76 : 510616 : std::map<TNode, Rational>::iterator it;
77 : 510616 : Kind tk = t.getKind();
78 [ + + ]: 7353120 : while (!countMap.empty())
79 : : {
80 : : // Go off of end first. This is important for efficiency since later terms
81 : : // in the map may contain subterms that are earlier terms in the map.
82 : 3421252 : std::map<TNode, Rational>::iterator cur = std::prev(countMap.end());
83 : 3421252 : bool recurse = false;
84 : 3421252 : TNode tc = cur->first;
85 : 3421252 : Kind k = tc.getKind();
86 : 3421252 : Rational coeff = cur->second;
87 : 3421252 : countMap.erase(cur);
88 : : // Additionally collect coefficient
89 [ + + ][ + - ]: 4296184 : while (k == Kind::MULT && tc.getNumChildren() == 2 && tc[0].isConst())
[ + + ][ + + ]
[ + + ][ - - ]
90 : : {
91 : 874932 : coeff *= tc[0].getConst<Rational>();
92 : 874932 : tc = tc[1];
93 : 874932 : k = tc.getKind();
94 : : }
95 : : // figure out whether to recurse into cur
96 : : if constexpr (sizeof...(kinds) == 0)
97 : : {
98 : : recurse = tk == k;
99 : : }
100 : : else
101 : : {
102 [ + + ][ + + ]: 3421252 : recurse = ((kinds == k) || ...);
103 : : }
104 [ + + ]: 3421252 : if (recurse)
105 : : {
106 [ + + ]: 6309258 : for (TNode cc : tc)
107 : : {
108 : 3320336 : countMap[cc] += coeff;
109 : : }
110 : : }
111 : : else
112 : : {
113 : 1926791 : children.emplace_back(tc, coeff);
114 : : }
115 : : }
116 : 510616 : return true;
117 : 510616 : }
118 : :
119 : 28698 : ArithRewriter::ArithRewriter(NodeManager* nm,
120 : : OperatorElim& oe,
121 : 28698 : bool expertEnabled)
122 : 28698 : : TheoryRewriter(nm), d_opElim(oe), d_expertEnabled(expertEnabled)
123 : : {
124 : 28698 : registerProofRewriteRule(ProofRewriteRule::ARITH_POW_ELIM,
125 : : TheoryRewriteCtx::PRE_DSL);
126 : 28698 : registerProofRewriteRule(ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL,
127 : : TheoryRewriteCtx::DSL_SUBCALL);
128 : 28698 : registerProofRewriteRule(ProofRewriteRule::MACRO_ARITH_INT_EQ_CONFLICT,
129 : : TheoryRewriteCtx::DSL_SUBCALL);
130 : 28698 : registerProofRewriteRule(ProofRewriteRule::MACRO_ARITH_INT_GEQ_TIGHTEN,
131 : : TheoryRewriteCtx::DSL_SUBCALL);
132 : : // we don't register ARITH_STRING_PRED_ENTAIL or
133 : : // ARITH_STRING_PRED_SAFE_APPROX, as these are subsumed by
134 : : // MACRO_ARITH_STRING_PRED_ENTAIL.
135 : 28698 : }
136 : :
137 : 2035267 : Node ArithRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
138 : : {
139 [ + + ][ + + ]: 2035267 : switch (id)
[ + + ]
140 : : {
141 : 223210 : case ProofRewriteRule::ARITH_POW_ELIM:
142 : : {
143 [ + + ]: 223210 : if (n.getKind() == Kind::POW)
144 : : {
145 : 7 : Node nx = expandPowConst(nodeManager(), n);
146 [ + - ]: 7 : if (!nx.isNull())
147 : : {
148 : 7 : return nx;
149 : : }
150 [ - + ]: 7 : }
151 : : }
152 : 223203 : break;
153 : 605270 : case ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL:
154 : : {
155 : : // only matters if n contains integer string operators
156 : 1120114 : if (!n.getType().isBoolean() || n.getNumChildren() != 2 || n[0] == n[1]
157 : 1120114 : || !expr::hasSubtermKinds(
158 : : {Kind::STRING_LENGTH, Kind::STRING_INDEXOF, Kind::STRING_STOI},
159 : : n))
160 : : {
161 : 487140 : return Node::null();
162 : : }
163 [ + - ]: 118130 : Trace("macro-arith-str-pred") << "Check entailment " << n << std::endl;
164 : : // Note that we do *not* pass a rewriter here, since the proof rule
165 : : // cannot depend on the rewriter. This makes this rule capture most
166 : : // but not all cases of this kind of reasoning.
167 : 118130 : theory::strings::ArithEntail ae(d_nm, nullptr);
168 : 118130 : Node tgt;
169 [ + + ]: 118130 : if (n.getKind() == Kind::EQUAL)
170 : : {
171 : 21932 : tgt = n;
172 : : }
173 : : else
174 : : {
175 : 96198 : tgt = ae.normalizeGeq(n);
176 : : }
177 : 118130 : if (tgt.isNull() || !tgt[0].getType().isInteger())
178 : : {
179 : 93 : return Node::null();
180 : : }
181 : : // first do basic length intro, which rewrites (str.len (str.++ x y))
182 : : // to (+ (str.len x) (str.len y))
183 : 118037 : Node nexp = ae.rewriteLengthIntro(tgt);
184 [ + - ]: 118037 : Trace("macro-arith-str-pred") << "...setup to " << nexp << std::endl;
185 : : // Also must make this a "simple" check (isSimple = true).
186 : 118037 : Node ret = ae.rewritePredViaEntailment(nexp, true);
187 [ + - ]: 118037 : Trace("macro-arith-str-pred") << "...result = " << ret << std::endl;
188 : 118037 : return ret;
189 : 118130 : }
190 : : break;
191 : 215 : case ProofRewriteRule::ARITH_STRING_PRED_ENTAIL:
192 : : case ProofRewriteRule::ARITH_STRING_PRED_SAFE_APPROX:
193 : : {
194 [ + - ][ - + ]: 430 : if (n.getKind() != Kind::GEQ || !n[1].isConst()
[ - - ]
195 [ + - ][ - + ]: 430 : || n[1].getConst<Rational>().sgn() != 0)
[ + - ][ + - ]
[ - - ]
196 : : {
197 : 0 : return Node::null();
198 : : }
199 [ + + ]: 215 : if (id == ProofRewriteRule::ARITH_STRING_PRED_ENTAIL)
200 : : {
201 [ + - ]: 138 : if (theory::strings::ArithEntail::checkSimple(n[0]))
202 : : {
203 : 276 : return nodeManager()->mkConst(true);
204 : : }
205 : : }
206 [ + - ]: 77 : else if (id == ProofRewriteRule::ARITH_STRING_PRED_SAFE_APPROX)
207 : : {
208 : : // Note that we do *not* pass a rewriter here, since the proof rule
209 : : // cannot depend on the rewriter.
210 : 77 : theory::strings::ArithEntail ae(nodeManager(), nullptr);
211 : : // must only use simple checks when computing the approximations
212 : 77 : Node approx = ae.findApprox(n[0], true);
213 [ + - ]: 77 : if (approx != n[0])
214 : : {
215 [ + - ]: 154 : Trace("arith-rewriter-proof")
216 [ - + ][ - - ]: 77 : << n[0] << " --> " << approx << " by safe approx" << std::endl;
217 : 77 : return nodeManager()->mkNode(Kind::GEQ, approx, n[1]);
218 : : }
219 [ - + ][ - + ]: 154 : }
220 : : }
221 : 0 : break;
222 : 603334 : case ProofRewriteRule::MACRO_ARITH_INT_EQ_CONFLICT:
223 : : {
224 : 603334 : if (n.getKind() == Kind::EQUAL && n[0] != n[1])
225 : : {
226 [ + + ][ + + ]: 100317 : Node a = n[0].getKind() == Kind::TO_REAL ? n[0][0] : n[0];
[ - - ]
227 [ + + ][ + + ]: 100222 : Node b = n[1].getKind() == Kind::TO_REAL ? n[1][0] : n[1];
[ - - ]
228 : 99956 : rewriter::Sum sum;
229 : : // allow dropping TO_REAL
230 : 99956 : rewriter::addToSumNoMixed(sum, a, false);
231 : 99956 : rewriter::addToSumNoMixed(sum, b, true);
232 [ + + ]: 99956 : if (rewriter::isIntegral(sum))
233 : : {
234 : 77487 : std::pair<Node, Node> p = decomposeSum(d_nm, std::move(sum));
235 : 77487 : Rational c = p.second.getConst<Rational>();
236 [ + + ]: 77487 : if (!c.isIntegral())
237 : : {
238 : 336 : return d_nm->mkConst(false);
239 : : }
240 [ + + ][ + + ]: 77655 : }
241 [ + + ][ + + ]: 100292 : }
[ + + ]
242 : : }
243 : 603166 : break;
244 : 603233 : case ProofRewriteRule::MACRO_ARITH_INT_GEQ_TIGHTEN:
245 : : {
246 [ + - ]: 603233 : Trace("arith-rewriter-proof") << "Rewrite " << n << "?" << std::endl;
247 : 603233 : if (n.getKind() == Kind::GEQ && n[0] != n[1])
248 : : {
249 [ + + ][ + + ]: 206129 : Node a = n[0].getKind() == Kind::TO_REAL ? n[0][0] : n[0];
[ - - ]
250 [ + + ][ + + ]: 206090 : Node b = n[1].getKind() == Kind::TO_REAL ? n[1][0] : n[1];
[ - - ]
251 : 205869 : rewriter::Sum sum;
252 : : // allow dropping TO_REAL
253 : 205869 : rewriter::addToSumNoMixed(sum, a, false);
254 : 205869 : rewriter::addToSumNoMixed(sum, b, true);
255 [ + + ]: 205869 : if (rewriter::isIntegral(sum))
256 : : {
257 : : // decompose the sum into a non-constant and constant part
258 : 168542 : bool negated = false;
259 : : std::pair<Node, Node> p =
260 : 168542 : decomposeSum(d_nm, std::move(sum), negated, true);
261 : 168542 : Rational c = p.second.getConst<Rational>();
262 [ + - ]: 337084 : Trace("arith-rewriter-proof")
263 : 168542 : << "Decomposed to " << p.first << " + " << p.second << std::endl;
264 [ + + ]: 168542 : if (!c.isIntegral())
265 : : {
266 : 180 : c = -c;
267 : 180 : c = c.ceiling();
268 : 360 : Node ret = d_nm->mkNode(Kind::GEQ, p.first, d_nm->mkConstInt(c));
269 [ + + ]: 180 : if (negated)
270 : : {
271 : 83 : ret = ret.notNode();
272 : : }
273 : 180 : return ret;
274 : 180 : }
275 [ + + ][ + + ]: 168722 : }
276 [ + + ][ + + ]: 206229 : }
[ + + ]
277 : : }
278 : 603053 : break;
279 : 5 : default: break;
280 : : }
281 : 1429427 : return Node::null();
282 : : }
283 : :
284 : 12702724 : RewriteResponse ArithRewriter::preRewrite(TNode t)
285 : : {
286 [ + - ]: 12702724 : Trace("arith-rewriter") << "preRewrite(" << t << ")" << std::endl;
287 [ + + ]: 12702724 : if (rewriter::isAtom(t))
288 : : {
289 : 6769978 : auto res = preRewriteAtom(t);
290 [ + - ]: 13539956 : Trace("arith-rewriter")
291 : 6769978 : << res.d_status << " -> " << res.d_node << std::endl;
292 : 6769978 : return res;
293 : 6769978 : }
294 : 5932746 : auto res = preRewriteTerm(t);
295 [ + - ]: 5932746 : Trace("arith-rewriter") << res.d_status << " -> " << res.d_node << std::endl;
296 : 5932746 : return res;
297 : 5932746 : }
298 : :
299 : 10876384 : RewriteResponse ArithRewriter::postRewrite(TNode t)
300 : : {
301 [ + - ]: 10876384 : Trace("arith-rewriter") << "postRewrite(" << t << ")" << std::endl;
302 [ + + ]: 10876384 : if (rewriter::isAtom(t))
303 : : {
304 : 5689389 : auto res = postRewriteAtom(t);
305 [ + - ]: 11378778 : Trace("arith-rewriter")
306 : 5689389 : << res.d_status << " -> " << res.d_node << std::endl;
307 : 5689389 : return res;
308 : 5689389 : }
309 : 5186995 : auto res = postRewriteTerm(t);
310 [ + - ]: 5186995 : Trace("arith-rewriter") << res.d_status << " -> " << res.d_node << std::endl;
311 : 5186995 : return res;
312 : 5186995 : }
313 : :
314 : 6769978 : RewriteResponse ArithRewriter::preRewriteAtom(TNode atom)
315 : : {
316 [ - + ][ - + ]: 6769978 : Assert(rewriter::isAtom(atom));
[ - - ]
317 : :
318 : 6769978 : Kind kind = atom.getKind();
319 [ + + ]: 6769978 : if (atom.getNumChildren() == 2)
320 : : {
321 [ + + ]: 6769023 : if (auto response =
322 : 6769023 : rewriter::tryEvaluateRelationReflexive(kind, atom[0], atom[1]);
323 : 6769023 : response)
324 : : {
325 : 197124 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, *response));
326 : : }
327 : : }
328 : :
329 [ + + ][ + + ]: 6671416 : switch (kind)
[ + ]
330 : : {
331 : 245058 : case Kind::GT:
332 : : return RewriteResponse(
333 : : REWRITE_DONE,
334 : 490116 : rewriter::buildRelation(Kind::LEQ, atom[0], atom[1], true));
335 : 218803 : case Kind::LT:
336 : : return RewriteResponse(
337 : : REWRITE_DONE,
338 : 437606 : rewriter::buildRelation(Kind::GEQ, atom[0], atom[1], true));
339 : 877 : case Kind::IS_INTEGER:
340 [ + + ]: 877 : if (atom[0].getType().isInteger())
341 : : {
342 : 10 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, true));
343 : : }
344 : 872 : break;
345 : 78 : case Kind::DIVISIBLE:
346 [ - + ]: 78 : if (atom.getOperator().getConst<Divisible>().k.isOne())
347 : : {
348 : 0 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, true));
349 : : }
350 : 78 : break;
351 : 6207550 : default:;
352 : : }
353 : :
354 : 6207550 : return RewriteResponse(REWRITE_DONE, atom);
355 : : }
356 : :
357 : 5689389 : RewriteResponse ArithRewriter::postRewriteAtom(TNode atom)
358 : : {
359 [ - + ][ - + ]: 5689389 : Assert(rewriter::isAtom(atom));
[ - - ]
360 [ + - ]: 5689389 : Trace("arith-rewriter") << "postRewriteAtom: " << atom << std::endl;
361 : :
362 [ + + ]: 5689389 : if (atom.getKind() == Kind::IS_INTEGER)
363 : : {
364 : 838 : return rewriteExtIntegerOp(atom);
365 : : }
366 [ + + ]: 5688551 : else if (atom.getKind() == Kind::DIVISIBLE)
367 : : {
368 : 39 : const Integer& k = atom.getOperator().getConst<Divisible>().k;
369 [ - + ]: 39 : if (atom[0].isConst())
370 : : {
371 : 0 : const Rational& num = atom[0].getConst<Rational>();
372 : : return RewriteResponse(REWRITE_DONE,
373 : 0 : rewriter::mkConst(d_nm, (num / k).isIntegral()));
374 : : }
375 [ - + ]: 39 : if (k.isOne())
376 : : {
377 : 0 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, true));
378 : : }
379 : 39 : NodeManager* nm = nodeManager();
380 : : return RewriteResponse(REWRITE_AGAIN_FULL,
381 [ + + ][ - - ]: 195 : nm->mkNode(Kind::EQUAL,
382 : 78 : {nm->mkNode(Kind::INTS_MODULUS_TOTAL,
383 : : atom[0],
384 : 78 : rewriter::mkConst(d_nm, k)),
385 : 117 : rewriter::mkConst(d_nm, Integer(0))}));
386 : : }
387 : : // left |><| right
388 : 5688512 : Kind kind = atom.getKind();
389 : 11377024 : Node left = rewriter::removeToReal(atom[0]);
390 : 11377024 : Node right = rewriter::removeToReal(atom[1]);
391 : :
392 [ + + ]: 11377024 : if (auto response = rewriter::tryEvaluateRelationReflexive(kind, left, right);
393 : 5688512 : response)
394 : : {
395 : 347576 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, *response));
396 : : }
397 : :
398 [ - + ][ - + ]: 5514724 : Assert(isRelationOperator(kind));
[ - - ]
399 : :
400 [ + + ]: 11029448 : if (auto response = rewriter::tryEvaluateRelation(kind, left, right);
401 : 5514724 : response)
402 : : {
403 : 1087572 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, *response));
404 : : }
405 : :
406 : 4970938 : bool negate = false;
407 : :
408 [ + - ][ + ]: 4970938 : switch (atom.getKind())
409 : : {
410 : 304898 : case Kind::LEQ:
411 : 304898 : kind = Kind::GEQ;
412 : 304898 : negate = true;
413 : 304898 : break;
414 : 0 : case Kind::LT:
415 : 0 : kind = Kind::GT;
416 : 0 : negate = true;
417 : 0 : break;
418 : 4666040 : default: break;
419 : : }
420 : :
421 : 9941876 : rewriter::Sum sum;
422 : 4970938 : rewriter::addToSum(sum, left, negate);
423 : 4970938 : rewriter::addToSum(sum, right, !negate);
424 : :
425 : : // Now we have (sum <kind> 0)
426 [ + + ]: 4970938 : if (rewriter::isIntegral(sum))
427 : : {
428 [ + - ]: 3720139 : Trace("arith-rewriter") << "...sum is integral" << std::endl;
429 [ + + ]: 3720139 : if (kind == Kind::EQUAL)
430 : : {
431 : : return RewriteResponse(
432 : 3820854 : REWRITE_DONE, rewriter::buildIntegerEquality(d_nm, std::move(sum)));
433 : : }
434 : : return RewriteResponse(
435 : : REWRITE_DONE,
436 : 3619424 : rewriter::buildIntegerInequality(d_nm, std::move(sum), kind));
437 : : }
438 : : else
439 : : {
440 [ + - ]: 1250799 : Trace("arith-rewriter") << "...sum is not integral" << std::endl;
441 [ + + ]: 1250799 : if (kind == Kind::EQUAL)
442 : : {
443 : : return RewriteResponse(REWRITE_DONE,
444 : 610622 : rewriter::buildRealEquality(d_nm, std::move(sum)));
445 : : }
446 : : return RewriteResponse(
447 : : REWRITE_DONE,
448 : 1890976 : rewriter::buildRealInequality(d_nm, std::move(sum), kind));
449 : : }
450 : 5688512 : }
451 : :
452 : 5932746 : RewriteResponse ArithRewriter::preRewriteTerm(TNode t)
453 : : {
454 [ + + ]: 5932746 : if (t.isConst())
455 : : {
456 : 794962 : return RewriteResponse(REWRITE_DONE, t);
457 : : }
458 [ - + ]: 5137784 : else if (t.isVar())
459 : : {
460 : 0 : return rewriteVariable(t);
461 : : }
462 : : else
463 : : {
464 [ + + ][ + + ]: 5137784 : switch (Kind k = t.getKind())
[ + + ][ + + ]
[ + + ][ - ]
465 : : {
466 : 274 : case Kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
467 : 557726 : case Kind::SUB: return rewriteSub(t);
468 : 23556 : case Kind::NEG: return rewriteNeg(t, true);
469 : 10937 : case Kind::DIVISION:
470 : 10937 : case Kind::DIVISION_TOTAL: return rewriteDiv(t, true);
471 : 3155228 : case Kind::ADD: return preRewritePlus(t);
472 : 1312179 : case Kind::MULT:
473 : 1312179 : case Kind::NONLINEAR_MULT: return preRewriteMult(t);
474 : 8432 : case Kind::INTS_DIVISION:
475 : 8432 : case Kind::INTS_MODULUS: return rewriteIntsDivMod(t);
476 : 25908 : case Kind::INTS_DIVISION_TOTAL:
477 : 25908 : case Kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, true);
478 : 6604 : case Kind::ABS: return rewriteAbs(t);
479 : 36940 : case Kind::IAND:
480 : : case Kind::PIAND:
481 : : case Kind::POW2:
482 : : case Kind::INTS_ISPOW2:
483 : : case Kind::INTS_LOG2:
484 : : case Kind::EXPONENTIAL:
485 : : case Kind::SINE:
486 : : case Kind::COSINE:
487 : : case Kind::TANGENT:
488 : : case Kind::COSECANT:
489 : : case Kind::SECANT:
490 : : case Kind::COTANGENT:
491 : : case Kind::ARCSINE:
492 : : case Kind::ARCCOSINE:
493 : : case Kind::ARCTANGENT:
494 : : case Kind::ARCCOSECANT:
495 : : case Kind::ARCSECANT:
496 : : case Kind::ARCCOTANGENT:
497 : : case Kind::SQRT:
498 : : case Kind::IS_INTEGER:
499 : : case Kind::TO_INTEGER:
500 : : case Kind::TO_REAL:
501 : : case Kind::POW:
502 : 36940 : case Kind::PI: return RewriteResponse(REWRITE_DONE, t);
503 : 0 : default: Unhandled() << k;
504 : : }
505 : : }
506 : : }
507 : :
508 : 5186995 : RewriteResponse ArithRewriter::postRewriteTerm(TNode t)
509 : : {
510 [ + + ]: 5186995 : if (t.isConst())
511 : : {
512 : 1780221 : return RewriteResponse(REWRITE_DONE, t);
513 : : }
514 [ - + ]: 3406774 : else if (t.isVar())
515 : : {
516 : 0 : return rewriteVariable(t);
517 : : }
518 : : else
519 : : {
520 [ + - ]: 3406774 : Trace("arith-rewriter") << "postRewriteTerm: " << t << std::endl;
521 [ + - ][ - + ]: 3406774 : switch (t.getKind())
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ]
522 : : {
523 : 397 : case Kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
524 : 0 : case Kind::SUB: return rewriteSub(t);
525 : 0 : case Kind::NEG: return rewriteNeg(t, false);
526 : 5492 : case Kind::DIVISION:
527 : 5492 : case Kind::DIVISION_TOTAL: return rewriteDiv(t, false);
528 : 2246907 : case Kind::ADD: return postRewritePlus(t);
529 : 1080012 : case Kind::MULT:
530 : 1080012 : case Kind::NONLINEAR_MULT: return postRewriteMult(t);
531 : 142 : case Kind::INTS_ISPOW2: return postRewriteIntsIsPow2(t);
532 : 215 : case Kind::INTS_LOG2: return postRewriteIntsLog2(t);
533 : 6620 : case Kind::INTS_DIVISION:
534 : 6620 : case Kind::INTS_MODULUS: return rewriteIntsDivMod(t);
535 : 20477 : case Kind::INTS_DIVISION_TOTAL:
536 : 20477 : case Kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, false);
537 : 6266 : case Kind::ABS: return rewriteAbs(t);
538 : 23058 : case Kind::TO_REAL: return rewriteToReal(t);
539 : 3477 : case Kind::TO_INTEGER: return rewriteExtIntegerOp(t);
540 : 888 : case Kind::PI: return RewriteResponse(REWRITE_DONE, t);
541 : 1949 : case Kind::POW2: return postRewritePow2(t);
542 : 775 : case Kind::PIAND: return postRewritePIAnd(t);
543 : : // expert cases
544 : 10099 : case Kind::POW:
545 : : case Kind::EXPONENTIAL:
546 : : case Kind::SINE:
547 : : case Kind::COSINE:
548 : : case Kind::TANGENT:
549 : : case Kind::COSECANT:
550 : : case Kind::SECANT:
551 : : case Kind::COTANGENT:
552 : : case Kind::ARCSINE:
553 : : case Kind::ARCCOSINE:
554 : : case Kind::ARCTANGENT:
555 : : case Kind::ARCCOSECANT:
556 : : case Kind::ARCSECANT:
557 : : case Kind::ARCCOTANGENT:
558 : : case Kind::SQRT:
559 : 10099 : case Kind::IAND: return postRewriteExpert(t);
560 : 0 : default: Unreachable();
561 : : }
562 : : }
563 : : }
564 : 10099 : RewriteResponse ArithRewriter::postRewriteExpert(TNode t)
565 : : {
566 [ - + ]: 10099 : if (!d_expertEnabled)
567 : : {
568 : 0 : return RewriteResponse(REWRITE_DONE, t);
569 : : }
570 [ + + ][ + - ]: 10099 : switch (t.getKind())
571 : : {
572 : 214 : case Kind::POW:
573 : : {
574 : 214 : Node tx = expandPowConst(nodeManager(), t);
575 [ + + ]: 214 : if (!tx.isNull())
576 : : {
577 : 202 : return RewriteResponse(REWRITE_AGAIN_FULL, tx);
578 : : }
579 : 12 : return RewriteResponse(REWRITE_DONE, t);
580 : 214 : }
581 : 7881 : case Kind::EXPONENTIAL:
582 : : case Kind::SINE:
583 : : case Kind::COSINE:
584 : : case Kind::TANGENT:
585 : : case Kind::COSECANT:
586 : : case Kind::SECANT:
587 : : case Kind::COTANGENT:
588 : : case Kind::ARCSINE:
589 : : case Kind::ARCCOSINE:
590 : : case Kind::ARCTANGENT:
591 : : case Kind::ARCCOSECANT:
592 : : case Kind::ARCSECANT:
593 : : case Kind::ARCCOTANGENT:
594 : 7881 : case Kind::SQRT: return postRewriteTranscendental(t);
595 : 2004 : case Kind::IAND: return postRewriteIAnd(t);
596 : 0 : default: Unreachable();
597 : : }
598 : : }
599 : :
600 : 671 : RewriteResponse ArithRewriter::rewriteRAN(TNode t)
601 : : {
602 [ - + ][ - + ]: 671 : Assert(rewriter::isRAN(t));
[ - - ]
603 [ - + ][ - + ]: 671 : Assert(t.getType().isReal());
[ - - ]
604 : 671 : const RealAlgebraicNumber& r = rewriter::getRAN(t);
605 [ - + ]: 671 : if (r.isRational())
606 : : {
607 : : return RewriteResponse(REWRITE_DONE,
608 : 0 : rewriter::mkConst(d_nm, r.toRational()));
609 : : }
610 : 671 : return RewriteResponse(REWRITE_DONE, t);
611 : : }
612 : :
613 : 0 : RewriteResponse ArithRewriter::rewriteVariable(TNode t)
614 : : {
615 : 0 : Assert(t.isVar());
616 : :
617 : 0 : return RewriteResponse(REWRITE_DONE, t);
618 : : }
619 : :
620 : 23556 : RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
621 : : {
622 [ - + ][ - + ]: 23556 : Assert(t.getKind() == Kind::NEG);
[ - - ]
623 : :
624 : 23556 : NodeManager* nm = nodeManager();
625 [ + + ]: 23556 : if (t[0].isConst())
626 : : {
627 : 10949 : Rational neg = -(t[0].getConst<Rational>());
628 : : return RewriteResponse(REWRITE_DONE,
629 : 21898 : nm->mkConstRealOrInt(t.getType(), neg));
630 : 10949 : }
631 [ + + ]: 12607 : if (rewriter::isRAN(t[0]))
632 : : {
633 : : return RewriteResponse(REWRITE_DONE,
634 : 4 : rewriter::mkConst(d_nm, -rewriter::getRAN(t[0])));
635 : : }
636 : :
637 : : Node noUminus =
638 : 25210 : nm->mkNode(Kind::MULT, rewriter::mkConst(d_nm, Rational(-1)), t[0]);
639 [ + - ]: 12605 : if (pre)
640 : : {
641 : 12605 : return RewriteResponse(REWRITE_DONE, noUminus);
642 : : }
643 : : else
644 : : {
645 : 0 : return RewriteResponse(REWRITE_AGAIN, noUminus);
646 : : }
647 : 12605 : }
648 : :
649 : 557726 : RewriteResponse ArithRewriter::rewriteSub(TNode t)
650 : : {
651 [ - + ][ - + ]: 557726 : Assert(t.getKind() == Kind::SUB);
[ - - ]
652 [ - + ][ - + ]: 557726 : Assert(t.getNumChildren() == 2);
[ - - ]
653 : :
654 : 557726 : NodeManager* nm = nodeManager();
655 [ + + ]: 557726 : if (t[0] == t[1])
656 : : {
657 : : return RewriteResponse(REWRITE_DONE,
658 : 3140 : nm->mkConstRealOrInt(t.getType(), Rational(0)));
659 : : }
660 : : return RewriteResponse(
661 : : REWRITE_AGAIN_FULL,
662 : 1112312 : nm->mkNode(Kind::ADD,
663 : : t[0],
664 : 2224624 : nm->mkNode(Kind::MULT,
665 : 1112312 : nm->mkConstRealOrInt(t[1].getType(), Rational(-1)),
666 : 556156 : t[1])));
667 : : }
668 : :
669 : 3155228 : RewriteResponse ArithRewriter::preRewritePlus(TNode t)
670 : : {
671 [ - + ][ - + ]: 3155228 : Assert(t.getKind() == Kind::ADD);
[ - - ]
672 : 3155228 : std::vector<std::pair<TNode, Rational>> children;
673 [ + + ]: 3155228 : if (!flattenAndCollectSum(t, children, Kind::ADD))
674 : : {
675 : 2787591 : return RewriteResponse(REWRITE_DONE, t);
676 : : }
677 : 367637 : NodeManager* nm = nodeManager();
678 : 367637 : NodeBuilder nb(nm, Kind::ADD);
679 : 367637 : Rational coeff(0);
680 [ + + ]: 1757538 : for (const std::pair<TNode, Rational>& c : children)
681 : : {
682 [ + + ]: 1389901 : if (c.first.isConst())
683 : : {
684 : 578185 : coeff += c.first.getConst<Rational>() * c.second;
685 : : }
686 [ + + ]: 811716 : else if (c.second.isOne())
687 : : {
688 : 209692 : nb << c.first;
689 : : }
690 : : else
691 : : {
692 : 602024 : nb << nm->mkNode(Kind::MULT, nm->mkConstRealOrInt(c.second), c.first);
693 : : }
694 : : }
695 [ + + ][ + + ]: 367637 : if (!coeff.isZero() || nb.getNumChildren() == 0)
[ + + ]
696 : : {
697 : 289631 : nb << nm->mkConstRealOrInt(t.getType(), coeff);
698 : : }
699 [ + + ]: 367637 : Node ret = nb.getNumChildren() == 1 ? nb.getChild(0) : nb;
700 : 367637 : ret = rewriter::maybeEnsureReal(t.getType(), ret);
701 : 367637 : return RewriteResponse(REWRITE_DONE, ret);
702 : 3155228 : }
703 : :
704 : 2246907 : RewriteResponse ArithRewriter::postRewritePlus(TNode t)
705 : : {
706 [ - + ][ - + ]: 2246907 : Assert(t.getKind() == Kind::ADD);
[ - - ]
707 [ - + ][ - + ]: 2246907 : Assert(t.getNumChildren() > 1);
[ - - ]
708 : :
709 : 2246907 : rewriter::Sum sum;
710 : 2246907 : std::vector<std::pair<TNode, Rational>> children;
711 [ + + ]: 2246907 : if (!flattenAndCollectSum(t, children, Kind::ADD, Kind::TO_REAL))
712 : : {
713 : 2103928 : rewriter::addToSum(sum, t);
714 : : }
715 : : else
716 : : {
717 : 142979 : Rational coeff(0);
718 [ + + ]: 679869 : for (const std::pair<TNode, Rational>& c : children)
719 : : {
720 [ + + ]: 536890 : if (c.first.isConst())
721 : : {
722 : 190758 : coeff += c.first.getConst<Rational>() * c.second;
723 : : }
724 [ + + ]: 346132 : else if (c.second.isOne())
725 : : {
726 : 131757 : rewriter::addToSum(sum, c.first);
727 : : }
728 : : else
729 : : {
730 : 214375 : RealAlgebraicNumber mul = RealAlgebraicNumber(c.second);
731 : 214375 : rewriter::addMonomialToSum(sum, c.first, mul);
732 : 214375 : }
733 : : }
734 [ + + ]: 142979 : if (!coeff.isZero())
735 : : {
736 : 89563 : rewriter::addToSum(sum, nodeManager()->mkConstRealOrInt(coeff));
737 : : }
738 : 142979 : }
739 : 2246907 : Node retSum = rewriter::collectSum(d_nm, sum);
740 : 2246907 : retSum = rewriter::maybeEnsureReal(t.getType(), retSum);
741 : 4493814 : return RewriteResponse(REWRITE_DONE, retSum);
742 : 2246907 : }
743 : :
744 : 1312179 : RewriteResponse ArithRewriter::preRewriteMult(TNode node)
745 : : {
746 [ + + ][ + - ]: 1312179 : Assert(node.getKind() == Kind::MULT
[ - + ][ - + ]
[ - - ]
747 : : || node.getKind() == Kind::NONLINEAR_MULT);
748 : :
749 [ + + ]: 1312179 : if (auto res = rewriter::getZeroChild(node); res)
750 : : {
751 : : return RewriteResponse(REWRITE_DONE,
752 : 229818 : rewriter::maybeEnsureReal(node.getType(), *res));
753 [ + + ]: 1312179 : }
754 : 1197270 : return RewriteResponse(REWRITE_DONE, node);
755 : : }
756 : :
757 : 1080012 : RewriteResponse ArithRewriter::postRewriteMult(TNode t)
758 : : {
759 [ + + ][ + - ]: 1080012 : Assert(t.getKind() == Kind::MULT || t.getKind() == Kind::NONLINEAR_MULT);
[ - + ][ - + ]
[ - - ]
760 [ - + ][ - + ]: 1080012 : Assert(t.getNumChildren() >= 2);
[ - - ]
761 : :
762 : 1080012 : std::vector<TNode> children;
763 : 1080012 : expr::algorithm::flatten(
764 : : t, children, Kind::MULT, Kind::NONLINEAR_MULT, Kind::TO_REAL);
765 : :
766 [ + + ]: 1080012 : if (auto res = rewriter::getZeroChild(children); res)
767 : : {
768 : : return RewriteResponse(REWRITE_DONE,
769 : 11190 : rewriter::maybeEnsureReal(t.getType(), *res));
770 [ + + ]: 1080012 : }
771 : :
772 : 1074417 : RewriteStatus rs = REWRITE_DONE;
773 : 1074417 : Node ret;
774 : : // Distribute over addition
775 [ + + ]: 1074417 : if (std::any_of(children.begin(), children.end(), [](TNode child) {
776 : 2389863 : return child.getKind() == Kind::ADD;
777 : : }))
778 : : {
779 : : // if we distribute multiplication, we rewrite again to ensure the
780 : : // sum is sorted.
781 : 68448 : rs = REWRITE_AGAIN_FULL;
782 : 68448 : ret = rewriter::distributeMultiplication(d_nm, children);
783 : : }
784 : : else
785 : : {
786 : 1005969 : RealAlgebraicNumber ran = RealAlgebraicNumber(Integer(1));
787 : 1005969 : std::vector<Node> leafs;
788 : :
789 [ + + ]: 3262746 : for (const auto& child : children)
790 : : {
791 [ + + ]: 2256777 : if (child.isConst())
792 : : {
793 [ - + ]: 1104622 : if (child.getConst<Rational>().isZero())
794 : : {
795 : : return RewriteResponse(REWRITE_DONE,
796 : 0 : rewriter::maybeEnsureReal(t.getType(), child));
797 : : }
798 : 1104622 : ran *= child.getConst<Rational>();
799 : : }
800 [ + + ]: 1152155 : else if (rewriter::isRAN(child))
801 : : {
802 : 164 : ran *= rewriter::getRAN(child);
803 : : }
804 : : else
805 : : {
806 : 1151991 : leafs.emplace_back(child);
807 : : }
808 : : }
809 : 1005969 : ret = rewriter::mkMultTerm(d_nm, ran, std::move(leafs));
810 [ + - ][ + - ]: 1005969 : }
811 : 1074417 : ret = rewriter::maybeEnsureReal(t.getType(), ret);
812 : 1074417 : return RewriteResponse(rs, ret);
813 : 1080012 : }
814 : :
815 : 16429 : RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
816 : : {
817 [ + + ][ + - ]: 16429 : Assert(t.getKind() == Kind::DIVISION_TOTAL || t.getKind() == Kind::DIVISION);
[ - + ][ - + ]
[ - - ]
818 [ - + ][ - + ]: 16429 : Assert(t.getNumChildren() == 2);
[ - - ]
819 : :
820 : 32858 : Node left = rewriter::removeToReal(t[0]);
821 : 32858 : Node right = rewriter::removeToReal(t[1]);
822 : 16429 : NodeManager* nm = nodeManager();
823 [ + + ]: 16429 : if (right.isConst())
824 : : {
825 : 6518 : const Rational& den = right.getConst<Rational>();
826 : :
827 [ + + ]: 6518 : if (den.isZero())
828 : : {
829 [ + + ]: 1141 : if (t.getKind() == Kind::DIVISION_TOTAL)
830 : : {
831 : 171 : Node ret = nm->mkConstReal(0);
832 : 171 : return RewriteResponse(REWRITE_DONE, ret);
833 : 171 : }
834 : : else
835 : : {
836 : 1940 : Node ret = nm->mkNode(t.getKind(), left, right);
837 : 970 : return RewriteResponse(REWRITE_DONE, ret);
838 : 970 : }
839 : : }
840 [ - + ][ - + ]: 5377 : Assert(den != Rational(0));
[ - - ]
841 : :
842 [ + + ]: 5377 : if (left.isConst())
843 : : {
844 : 2154 : const Rational& num = left.getConst<Rational>();
845 : 4308 : return RewriteResponse(REWRITE_DONE, nm->mkConstReal(num / den));
846 : : }
847 [ - + ]: 3223 : if (rewriter::isRAN(left))
848 : : {
849 : : return RewriteResponse(REWRITE_DONE,
850 : 0 : rewriter::ensureReal(nm->mkRealAlgebraicNumber(
851 : 0 : rewriter::getRAN(left) / den)));
852 : : }
853 : :
854 : 3223 : Node result = nm->mkConstReal(den.inverse());
855 : : Node mult =
856 : 6446 : rewriter::ensureReal(nodeManager()->mkNode(Kind::MULT, left, result));
857 [ + + ]: 3223 : if (pre)
858 : : {
859 : 3195 : return RewriteResponse(REWRITE_DONE, mult);
860 : : }
861 : : // requires again full since ensureReal may have added a to_real
862 : 28 : return RewriteResponse(REWRITE_AGAIN_FULL, mult);
863 : 3223 : }
864 [ + + ]: 9911 : if (rewriter::isRAN(right))
865 : : {
866 : 4 : const RealAlgebraicNumber& den = rewriter::getRAN(right);
867 : : // mkConst is applied to RAN in this block, which are always Real
868 [ + + ]: 4 : if (left.isConst())
869 : : {
870 : : return RewriteResponse(
871 : : REWRITE_DONE,
872 : 4 : rewriter::ensureReal(rewriter::mkConst(
873 : 6 : d_nm, RealAlgebraicNumber(left.getConst<Rational>()) / den)));
874 : : }
875 [ + - ]: 2 : if (rewriter::isRAN(left))
876 : : {
877 : : return RewriteResponse(REWRITE_DONE,
878 : 4 : rewriter::ensureReal(rewriter::mkConst(
879 : 6 : d_nm, rewriter::getRAN(left) / den)));
880 : : }
881 : :
882 : 0 : Node result = rewriter::mkConst(d_nm, den.inverse());
883 : : Node mult =
884 : 0 : rewriter::ensureReal(nodeManager()->mkNode(Kind::MULT, left, result));
885 [ - - ]: 0 : if (pre)
886 : : {
887 : 0 : return RewriteResponse(REWRITE_DONE, mult);
888 : : }
889 : : // requires again full since ensureReal may have added a to_real
890 : 0 : return RewriteResponse(REWRITE_AGAIN_FULL, mult);
891 : 0 : }
892 : : // We also convert integral rationals in the numerator to integers,
893 : : // e.g. (/ 1 x) ---> (/ 1.0 x).
894 [ + + ]: 9907 : if (left.getKind() == Kind::CONST_INTEGER)
895 : : {
896 : 47 : left = nm->mkConstReal(left.getConst<Rational>());
897 : : }
898 : : // may have changed due to removing to_real
899 : 9907 : if (left != t[0] || right != t[1])
900 : : {
901 : 296 : Node ret = nm->mkNode(t.getKind(), left, right);
902 : 148 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
903 : 148 : }
904 : 9759 : return RewriteResponse(REWRITE_DONE, t);
905 : 16429 : }
906 : :
907 : 23058 : RewriteResponse ArithRewriter::rewriteToReal(TNode t)
908 : : {
909 [ - + ][ - + ]: 23058 : Assert(t.getKind() == Kind::TO_REAL);
[ - - ]
910 [ + + ]: 23058 : if (!t[0].getType().isInteger())
911 : : {
912 : : // if it is already real type, then just return the argument
913 : 18 : return RewriteResponse(REWRITE_DONE, t[0]);
914 : : }
915 : 23040 : NodeManager* nm = nodeManager();
916 [ + + ]: 23040 : if (t[0].isConst())
917 : : {
918 : : // If the argument is constant, return a real constant.
919 : 3625 : const Rational& rat = t[0].getConst<Rational>();
920 : 7250 : return RewriteResponse(REWRITE_DONE, nm->mkConstReal(rat));
921 : : }
922 [ - + ]: 19415 : if (t[0].getKind() == Kind::TO_REAL)
923 : : {
924 : : // (to_real (to_real t)) ---> (to_real t)
925 : 0 : return RewriteResponse(REWRITE_DONE, t[0]);
926 : : }
927 : 19415 : return RewriteResponse(REWRITE_DONE, t);
928 : : }
929 : :
930 : 12870 : RewriteResponse ArithRewriter::rewriteAbs(TNode t)
931 : : {
932 [ - + ][ - + ]: 12870 : Assert(t.getKind() == Kind::ABS);
[ - - ]
933 [ - + ][ - + ]: 12870 : Assert(t.getNumChildren() == 1);
[ - - ]
934 : :
935 [ + + ]: 12870 : if (t[0].isConst())
936 : : {
937 : 366 : const Rational& rat = t[0].getConst<Rational>();
938 [ + + ]: 366 : if (rat >= 0)
939 : : {
940 : 361 : return RewriteResponse(REWRITE_DONE, t[0]);
941 : : }
942 : : return RewriteResponse(
943 : 5 : REWRITE_DONE, nodeManager()->mkConstRealOrInt(t[0].getType(), -rat));
944 : : }
945 [ + + ]: 12504 : if (rewriter::isRAN(t[0]))
946 : : {
947 : 2 : const RealAlgebraicNumber& ran = rewriter::getRAN(t[0]);
948 [ + + ]: 2 : if (ran >= RealAlgebraicNumber())
949 : : {
950 : 1 : return RewriteResponse(REWRITE_DONE, t[0]);
951 : : }
952 : : return RewriteResponse(REWRITE_DONE,
953 : 2 : nodeManager()->mkRealAlgebraicNumber(-ran));
954 : : }
955 : 12502 : return RewriteResponse(REWRITE_DONE, t);
956 : : }
957 : :
958 : 15052 : RewriteResponse ArithRewriter::rewriteIntsDivMod(TNode t)
959 : : {
960 : 15052 : NodeManager* nm = nodeManager();
961 : 15052 : Kind k = t.getKind();
962 [ + + ]: 15052 : if (k == Kind::INTS_MODULUS)
963 : : {
964 : 11223 : if (t[1].isConst() && !t[1].getConst<Rational>().isZero())
965 : : {
966 : : // can immediately replace by INTS_MODULUS_TOTAL
967 : 4850 : Node ret = nm->mkNode(Kind::INTS_MODULUS_TOTAL, t[0], t[1]);
968 : 2425 : return returnRewrite(t, ret, Rewrite::MOD_TOTAL_BY_CONST);
969 : 2425 : }
970 : : }
971 [ + + ]: 12627 : if (k == Kind::INTS_DIVISION)
972 : : {
973 : 3829 : if (t[1].isConst() && !t[1].getConst<Rational>().isZero())
974 : : {
975 : : // can immediately replace by INTS_DIVISION_TOTAL
976 : 880 : Node ret = nm->mkNode(Kind::INTS_DIVISION_TOTAL, t[0], t[1]);
977 : 440 : return returnRewrite(t, ret, Rewrite::DIV_TOTAL_BY_CONST);
978 : 440 : }
979 : : }
980 : 12187 : return RewriteResponse(REWRITE_DONE, t);
981 : : }
982 : :
983 : 46385 : RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre)
984 : : {
985 [ + + ]: 46385 : if (pre)
986 : : {
987 : : // do not rewrite at prewrite.
988 : 25908 : return RewriteResponse(REWRITE_DONE, t);
989 : : }
990 : 20477 : NodeManager* nm = nodeManager();
991 : 20477 : Kind k = t.getKind();
992 [ + + ][ + - ]: 20477 : Assert(k == Kind::INTS_MODULUS_TOTAL || k == Kind::INTS_DIVISION_TOTAL);
[ - + ][ - + ]
[ - - ]
993 : 20477 : TNode n = t[0];
994 : 20477 : TNode d = t[1];
995 : 20477 : bool dIsConstant = d.isConst();
996 [ + + ][ + + ]: 20477 : if (dIsConstant && d.getConst<Rational>().isZero())
[ + + ]
997 : : {
998 : : // (div_total x 0) ---> 0 or (mod_total x 0) ---> x
999 : 340 : Node ret = k == Kind::INTS_MODULUS_TOTAL ? Node(t[0]) : nm->mkConstInt(0);
1000 : 210 : return returnRewrite(t, ret, Rewrite::DIV_MOD_BY_ZERO);
1001 : 210 : }
1002 [ + + ][ + + ]: 20267 : else if (dIsConstant && d.getConst<Rational>().isOne())
[ + + ]
1003 : : {
1004 [ + + ]: 562 : if (k == Kind::INTS_MODULUS_TOTAL)
1005 : : {
1006 : : // (mod_total x 1) --> 0
1007 : 98 : return returnRewrite(t, nm->mkConstInt(0), Rewrite::MOD_BY_ONE);
1008 : : }
1009 [ - + ][ - + ]: 464 : Assert(k == Kind::INTS_DIVISION_TOTAL);
[ - - ]
1010 : : // (div_total x 1) --> x
1011 : 464 : return returnRewrite(t, n, Rewrite::DIV_BY_ONE);
1012 : : }
1013 [ + + ][ + + ]: 19705 : else if (dIsConstant && d.getConst<Rational>().sgn() < 0)
[ + + ]
1014 : : {
1015 : : // pull negation
1016 : : // (div_total x (- c)) ---> (- (div_total x c))
1017 : : // (mod_total x (- c)) ---> (mod_total x c)
1018 : 360 : Node nn = nm->mkNode(k, t[0], nm->mkConstInt(-t[1].getConst<Rational>()));
1019 [ + + ][ + + ]: 180 : Node ret = k == Kind::INTS_DIVISION_TOTAL ? nm->mkNode(Kind::NEG, nn) : nn;
[ - - ]
1020 : 180 : return returnRewrite(t, ret, Rewrite::DIV_MOD_PULL_NEG_DEN);
1021 : 180 : }
1022 [ + + ][ + + ]: 19525 : else if (dIsConstant && n.isConst())
[ + + ]
1023 : : {
1024 [ - + ][ - + ]: 3426 : Assert(d.getConst<Rational>().isIntegral());
[ - - ]
1025 [ - + ][ - + ]: 3426 : Assert(n.getConst<Rational>().isIntegral());
[ - - ]
1026 [ - + ][ - + ]: 3426 : Assert(!d.getConst<Rational>().isZero());
[ - - ]
1027 : 3426 : Integer di = d.getConst<Rational>().getNumerator();
1028 : 3426 : Integer ni = n.getConst<Rational>().getNumerator();
1029 : :
1030 : 3426 : bool isDiv = (k == Kind::INTS_DIVISION_TOTAL);
1031 : :
1032 : : Integer result = isDiv ? ni.euclidianDivideQuotient(di)
1033 [ + + ]: 3426 : : ni.euclidianDivideRemainder(di);
1034 : :
1035 : : // constant evaluation
1036 : : // (mod_total c1 c2) ---> c3 or (div_total c1 c2) ---> c3
1037 : 3426 : Node resultNode = nm->mkConstInt(Rational(result));
1038 : 3426 : return returnRewrite(t, resultNode, Rewrite::CONST_EVAL);
1039 : 3426 : }
1040 [ + + ]: 16099 : if (k == Kind::INTS_MODULUS_TOTAL)
1041 : : {
1042 : : // Note these rewrites do not need to account for modulus by zero as being
1043 : : // a UF, which is handled by the reduction of INTS_MODULUS.
1044 : 9589 : Kind k0 = t[0].getKind();
1045 : 9589 : if (k0 == Kind::INTS_MODULUS_TOTAL && t[0][1] == t[1])
1046 : : {
1047 : : // (mod_total (mod_total x c) c) --> (mod x c)
1048 : 41 : return returnRewrite(t, t[0], Rewrite::MOD_OVER_MOD);
1049 : : }
1050 [ + + ][ + + ]: 9548 : else if (k0 == Kind::NONLINEAR_MULT || k0 == Kind::MULT || k0 == Kind::ADD)
[ + + ]
1051 : : {
1052 : : // can drop all
1053 : 3500 : std::vector<Node> newChildren;
1054 : 3500 : bool childChanged = false;
1055 [ + + ]: 11694 : for (const Node& tc : t[0])
1056 : : {
1057 : 8194 : if (tc.getKind() == Kind::INTS_MODULUS_TOTAL && tc[1] == t[1])
1058 : : {
1059 : 52 : newChildren.push_back(tc[0]);
1060 : 52 : childChanged = true;
1061 : 52 : continue;
1062 : : }
1063 : 8142 : newChildren.push_back(tc);
1064 [ + + ]: 11694 : }
1065 [ + + ]: 3500 : if (childChanged)
1066 : : {
1067 : : // (mod_total (op ... (mod_total x c) ...) c) --->
1068 : : // (mod_total (op ... x ...) c) where
1069 : : // op is one of { NONLINEAR_MULT, MULT, ADD }.
1070 : 52 : Node ret = nm->mkNode(k0, newChildren);
1071 : 52 : ret = nm->mkNode(Kind::INTS_MODULUS_TOTAL, ret, t[1]);
1072 : 52 : return returnRewrite(t, ret, Rewrite::MOD_CHILD_MOD);
1073 : 52 : }
1074 [ + + ]: 3500 : }
1075 : : }
1076 : : else
1077 : : {
1078 [ - + ][ - + ]: 6510 : Assert(k == Kind::INTS_DIVISION_TOTAL);
[ - - ]
1079 : : // Note these rewrites do not need to account for division by zero as being
1080 : : // a UF, which is handled by the reduction of INTS_DIVISION.
1081 : 6510 : if (t[0].getKind() == Kind::INTS_MODULUS_TOTAL && t[0][1] == t[1])
1082 : : {
1083 : : // (div_total (mod_total x c) c) --> 0
1084 : 0 : Node ret = nm->mkConstInt(0);
1085 : 0 : return returnRewrite(t, ret, Rewrite::DIV_OVER_MOD);
1086 : 0 : }
1087 : : }
1088 : 16006 : return RewriteResponse(REWRITE_DONE, t);
1089 : 20477 : }
1090 : :
1091 : 4315 : RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t)
1092 : : {
1093 [ + + ][ + - ]: 4315 : Assert(t.getKind() == Kind::TO_INTEGER || t.getKind() == Kind::IS_INTEGER);
[ - + ][ - + ]
[ - - ]
1094 : 4315 : bool isPred = t.getKind() == Kind::IS_INTEGER;
1095 : 4315 : NodeManager* nm = nodeManager();
1096 [ + + ]: 4315 : if (t[0].isConst())
1097 : : {
1098 : 500 : Node ret;
1099 [ + + ]: 500 : if (isPred)
1100 : : {
1101 : 20 : ret = nm->mkConst(t[0].getConst<Rational>().isIntegral());
1102 : : }
1103 : : else
1104 : : {
1105 : 480 : ret = nm->mkConstInt(Rational(t[0].getConst<Rational>().floor()));
1106 : : }
1107 : 500 : return returnRewrite(t, ret, Rewrite::INT_EXT_CONST);
1108 : 500 : }
1109 [ + + ]: 3815 : if (t[0].getType().isInteger())
1110 : : {
1111 [ - + ][ + - ]: 230 : Node ret = isPred ? nm->mkConst(true) : Node(t[0]);
[ - - ]
1112 : 115 : return returnRewrite(t, ret, Rewrite::INT_EXT_INT);
1113 : 115 : }
1114 [ + + ]: 3700 : if (t[0].getKind() == Kind::TO_REAL)
1115 : : {
1116 : 238 : Node ret = nm->mkNode(t.getKind(), t[0][0]);
1117 : 119 : return returnRewrite(t, ret, Rewrite::INT_EXT_TO_REAL);
1118 : 119 : }
1119 [ + - ]: 3581 : if (d_expertEnabled)
1120 : : {
1121 [ + + ]: 3581 : if (t[0].getKind() == Kind::PI)
1122 : : {
1123 [ + + ][ + + ]: 14 : Node ret = isPred ? nm->mkConst(false) : nm->mkConstInt(Rational(3));
[ - - ]
1124 : 12 : return returnRewrite(t, ret, Rewrite::INT_EXT_PI);
1125 : 12 : }
1126 : : }
1127 : 3569 : return RewriteResponse(REWRITE_DONE, t);
1128 : : }
1129 : :
1130 : 2004 : RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
1131 : : {
1132 [ - + ][ - + ]: 2004 : Assert(t.getKind() == Kind::IAND);
[ - - ]
1133 : 2004 : uint32_t bsize = t.getOperator().getConst<IntAnd>().d_size;
1134 : 2004 : NodeManager* nm = nodeManager();
1135 : : // if constant, we eliminate
1136 : 2004 : if (t[0].isConst() && t[1].isConst())
1137 : : {
1138 : 940 : Node iToBvop = nm->mkConst(IntToBitVector(bsize));
1139 : 1880 : Node arg1 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[0]);
1140 : 1880 : Node arg2 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[1]);
1141 : 1880 : Node bvand = nm->mkNode(Kind::BITVECTOR_AND, arg1, arg2);
1142 : 940 : Node ret = nm->mkNode(Kind::BITVECTOR_UBV_TO_INT, bvand);
1143 : 940 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1144 : 940 : }
1145 [ + + ]: 1064 : else if (t[0] > t[1])
1146 : : {
1147 : : // ((_ iand k) x y) ---> ((_ iand k) y x) if x > y by node ordering
1148 : 174 : Node ret = nm->mkNode(Kind::IAND, t.getOperator(), t[1], t[0]);
1149 : 87 : return RewriteResponse(REWRITE_AGAIN, ret);
1150 : 87 : }
1151 [ + + ]: 977 : else if (t[0] == t[1])
1152 : : {
1153 : : // ((_ iand k) x x) ---> (mod x 2^k)
1154 : 24 : Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
1155 : 24 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[0], twok);
1156 : 12 : return RewriteResponse(REWRITE_AGAIN, ret);
1157 : 12 : }
1158 : : // simplifications involving constants
1159 [ + + ]: 2868 : for (unsigned i = 0; i < 2; i++)
1160 : : {
1161 [ + + ]: 1929 : if (!t[i].isConst())
1162 : : {
1163 : 1684 : continue;
1164 : : }
1165 [ + + ]: 245 : if (t[i].getConst<Rational>().sgn() == 0)
1166 : : {
1167 : : // ((_ iand k) 0 y) ---> 0
1168 : 1 : return RewriteResponse(REWRITE_DONE, t[i]);
1169 : : }
1170 [ + + ]: 244 : if (t[i].getConst<Rational>().getNumerator() == Integer(2).pow(bsize) - 1)
1171 : : {
1172 : : // ((_ iand k) 111...1 y) ---> (mod y 2^k)
1173 : 50 : Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
1174 : 50 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[1 - i], twok);
1175 : 25 : return RewriteResponse(REWRITE_AGAIN, ret);
1176 : 25 : }
1177 : : }
1178 : 939 : return RewriteResponse(REWRITE_DONE, t);
1179 : : }
1180 : :
1181 : 775 : RewriteResponse ArithRewriter::postRewritePIAnd(TNode t)
1182 : : {
1183 [ - + ][ - + ]: 775 : Assert(t.getKind() == Kind::PIAND);
[ - - ]
1184 : 775 : NodeManager* nm = nodeManager();
1185 : : // simplifications involving constants
1186 [ + + ][ - - ]: 775 : if (t[0].isConst()
1187 [ + + ][ + + ]: 1570 : && (t[0].getConst<Rational>().sgn() == 0
[ + - ][ - - ]
1188 [ + + ][ + + ]: 795 : || t[0].getConst<Rational>().sgn() == -1))
[ + + ][ - - ]
1189 : : {
1190 : 80 : return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(0)));
1191 : : }
1192 [ + + ]: 2161 : for (unsigned i = 1; i < 3; i++)
1193 : : {
1194 [ + + ]: 1454 : if (!t[i].isConst())
1195 : : {
1196 : 1426 : continue;
1197 : : }
1198 [ + + ]: 108 : if (t[i].getConst<Rational>().sgn() == 0)
1199 : : {
1200 : : // (piand k 0 y) ---> 0
1201 : 44 : return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(0)));
1202 : : }
1203 [ + + ]: 86 : if (!t[0].isConst())
1204 : : {
1205 : 80 : continue;
1206 : : }
1207 : 6 : size_t bsize = t[0].getConst<Rational>().getNumerator().toUnsignedInt();
1208 : 6 : Node twok = nm->mkNode(Kind::POW2, t[0]);
1209 : 12 : Node maxsign = nm->mkConstInt(Rational(Integer(2).pow(bsize) - 1));
1210 : 12 : if (t[i].getConst<Rational>().getNumerator()
1211 [ + - ]: 18 : == maxsign.getConst<Rational>().getNumerator())
1212 : : {
1213 : : // (piand k 111...1 y) ---> (mod y 2^k)
1214 [ + - ]: 6 : if (i == 1)
1215 : : {
1216 : 12 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[2], twok);
1217 : 6 : return RewriteResponse(REWRITE_AGAIN, ret);
1218 : 6 : }
1219 [ - - ]: 0 : else if (i == 2)
1220 : : {
1221 : 0 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[1], twok);
1222 : 0 : return RewriteResponse(REWRITE_AGAIN, ret);
1223 : 0 : }
1224 : : }
1225 [ - + ][ - + ]: 12 : }
1226 : : // if constant, we eliminate
1227 : 707 : if (t[0].isConst() && t[1].isConst() && t[2].isConst())
1228 : : {
1229 : 0 : size_t bsize = t[0].getConst<Rational>().getNumerator().toUnsignedInt();
1230 : 0 : Node iToBvop = nm->mkConst(IntToBitVector(bsize));
1231 : 0 : Node arg1 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[1]);
1232 : 0 : Node arg2 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[2]);
1233 : 0 : Node bvand = nm->mkNode(Kind::BITVECTOR_AND, arg1, arg2);
1234 : 0 : Node ret = nm->mkNode(Kind::BITVECTOR_UBV_TO_INT, bvand);
1235 : 0 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1236 : 0 : }
1237 [ + + ]: 707 : else if (t[1] > t[2])
1238 : : {
1239 : : // (piand k x y) ---> (piand k y x) if x > y by node ordering
1240 : 184 : Node ret = nm->mkNode(Kind::PIAND, t[0], t[2], t[1]);
1241 : 92 : return RewriteResponse(REWRITE_AGAIN, ret);
1242 : 92 : }
1243 [ + + ]: 615 : else if (t[1] == t[2])
1244 : : {
1245 : : // (piand k x x) ---> (mod x 2^k)
1246 : 20 : Node twok = nm->mkNode(Kind::POW2, t[0]);
1247 : 40 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[1], twok);
1248 : 20 : return RewriteResponse(REWRITE_AGAIN, ret);
1249 : 20 : }
1250 : 595 : return RewriteResponse(REWRITE_DONE, t);
1251 : : }
1252 : :
1253 : 1949 : RewriteResponse ArithRewriter::postRewritePow2(TNode t)
1254 : : {
1255 [ - + ][ - + ]: 1949 : Assert(t.getKind() == Kind::POW2);
[ - - ]
1256 : : // if constant, we eliminate
1257 [ + + ]: 1949 : if (t[0].isConst())
1258 : : {
1259 : : // pow2 is only supported for integers
1260 [ + - ]: 1908 : Trace("arith-rewriter")
1261 : 954 : << "ArithRewriter::postRewritePow2, t:" << t << std::endl;
1262 [ - + ][ - + ]: 954 : Assert(t[0].getType().isInteger());
[ - - ]
1263 : : // use the evaluator definition for rewriting this
1264 : 954 : Evaluator eval(nullptr);
1265 : 1908 : Node ret = eval.eval(t, {}, {});
1266 [ + + ]: 954 : if (!ret.isNull())
1267 : : {
1268 : 938 : return RewriteResponse(REWRITE_DONE, ret);
1269 : : }
1270 [ + + ]: 954 : }
1271 : 1011 : return RewriteResponse(REWRITE_DONE, t);
1272 : : }
1273 : :
1274 : 142 : RewriteResponse ArithRewriter::postRewriteIntsIsPow2(TNode t)
1275 : : {
1276 [ - + ][ - + ]: 142 : Assert(t.getKind() == Kind::INTS_ISPOW2);
[ - - ]
1277 : : // if constant, we eliminate
1278 [ + - ]: 142 : if (t[0].isConst())
1279 : : {
1280 : : // pow2 is only supported for integers
1281 [ - + ][ - + ]: 142 : Assert(t[0].getType().isInteger());
[ - - ]
1282 : 142 : Integer i = t[0].getConst<Rational>().getNumerator();
1283 : :
1284 : 284 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, i.isPow2()));
1285 : 142 : }
1286 : 0 : return RewriteResponse(REWRITE_DONE, t);
1287 : : }
1288 : 215 : RewriteResponse ArithRewriter::postRewriteIntsLog2(TNode t)
1289 : : {
1290 [ - + ][ - + ]: 215 : Assert(t.getKind() == Kind::INTS_LOG2);
[ - - ]
1291 : : // if constant, we eliminate
1292 [ + + ]: 215 : if (t[0].isConst())
1293 : : {
1294 : : // log2 is only supported for integers
1295 [ - + ][ - + ]: 159 : Assert(t[0].getType().isInteger());
[ - - ]
1296 : 159 : const Rational& r = t[0].getConst<Rational>();
1297 : : // default to 0 for negative inputs
1298 [ + + ]: 159 : if (r.sgn() < 0)
1299 : : {
1300 : 2 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, Integer(0)));
1301 : : }
1302 : : // for non-negative inputs, this
1303 : : // is captured by `length()` of `Integer`.
1304 : 158 : Integer i = r.getNumerator();
1305 : 158 : size_t const length = i.length();
1306 : : return RewriteResponse(REWRITE_DONE,
1307 : 316 : rewriter::mkConst(d_nm, Integer(length - 1)));
1308 : 158 : }
1309 : 56 : return RewriteResponse(REWRITE_DONE, t);
1310 : : }
1311 : :
1312 : 7881 : RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t)
1313 : : {
1314 [ + - ]: 15762 : Trace("arith-tf-rewrite")
1315 : 7881 : << "Rewrite transcendental function : " << t << std::endl;
1316 [ - + ][ - + ]: 7881 : Assert(t.getTypeOrNull(true).isReal());
[ - - ]
1317 : 7881 : NodeManager* nm = nodeManager();
1318 [ + + ][ + + ]: 7881 : switch (t.getKind())
[ + + ][ + + ]
1319 : : {
1320 : 1365 : case Kind::EXPONENTIAL:
1321 : : {
1322 [ + + ]: 1365 : if (t[0].isConst())
1323 : : {
1324 : 779 : Rational r = t[0].getConst<Rational>();
1325 [ + + ]: 779 : if (r.sgn() == 0)
1326 : : {
1327 : 50 : Node one = nm->mkConstReal(Rational(1));
1328 : : // (= (exp 0.0) 1.0)
1329 : 50 : return RewriteResponse(REWRITE_DONE, one);
1330 : 50 : }
1331 : : else
1332 : : {
1333 : 729 : return RewriteResponse(REWRITE_DONE, t);
1334 : : }
1335 : 779 : }
1336 [ + + ]: 586 : else if (t[0].getKind() == Kind::ADD)
1337 : : {
1338 : 61 : std::vector<Node> product;
1339 [ + + ]: 183 : for (const Node tc : t[0])
1340 : : {
1341 : 122 : Node tcr = rewriter::ensureReal(tc);
1342 : 122 : product.push_back(nm->mkNode(Kind::EXPONENTIAL, tcr));
1343 : 183 : }
1344 : : // We need to do a full rewrite here, since we can get exponentials of
1345 : : // constants, e.g. when we are rewriting exp(2 + x)
1346 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1347 : 122 : nm->mkNode(Kind::MULT, product));
1348 : 61 : }
1349 : : }
1350 : 525 : break;
1351 : 5788 : case Kind::SINE:
1352 [ + + ]: 5788 : if (t[0].isConst())
1353 : : {
1354 : 2249 : const Rational& rat = t[0].getConst<Rational>();
1355 [ + + ]: 2249 : if (rat.sgn() == 0)
1356 : : {
1357 : 116 : return RewriteResponse(REWRITE_DONE, nm->mkConstReal(Rational(0)));
1358 : : }
1359 [ + + ]: 2191 : else if (rat.sgn() == -1)
1360 : : {
1361 : : Node ret = nm->mkNode(Kind::NEG,
1362 : 394 : nm->mkNode(Kind::SINE, nm->mkConstReal(-rat)));
1363 : 197 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1364 : 197 : }
1365 : : }
1366 [ + + ][ - - ]: 3539 : else if ((t[0].getKind() == Kind::MULT
1367 [ - + ][ + - ]: 6988 : || t[0].getKind() == Kind::NONLINEAR_MULT)
[ - - ]
1368 : 6988 : && t[0][0].isConst() && t[0][0].getConst<Rational>().sgn() == -1)
1369 : : {
1370 : : // sin(-n*x) ---> -sin(n*x)
1371 : 30 : std::vector<Node> mchildren(t[0].begin(), t[0].end());
1372 : 15 : mchildren[0] = nm->mkConstReal(-t[0][0].getConst<Rational>());
1373 : : Node ret = nm->mkNode(
1374 : : Kind::NEG,
1375 : 30 : nm->mkNode(Kind::SINE, nm->mkNode(t[0].getKind(), mchildren)));
1376 : 15 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1377 : 15 : }
1378 : : else
1379 : : {
1380 : : // get the factor of PI in the argument
1381 : 3524 : Node pi_factor;
1382 : 3524 : Node pi;
1383 : 3524 : Node rem;
1384 : 3524 : std::map<Node, Node> msum;
1385 [ + - ]: 3524 : if (ArithMSum::getMonomialSum(t[0], msum))
1386 : : {
1387 : 3524 : pi = mkPi(nm);
1388 : 3524 : std::map<Node, Node>::iterator itm = msum.find(pi);
1389 [ + + ]: 3524 : if (itm != msum.end())
1390 : : {
1391 [ + + ]: 2083 : if (itm->second.isNull())
1392 : : {
1393 : 12 : pi_factor = rewriter::mkConst(d_nm, Integer(1));
1394 : : }
1395 : : else
1396 : : {
1397 : 2071 : pi_factor = itm->second;
1398 : : }
1399 : 2083 : msum.erase(pi);
1400 [ + + ]: 2083 : if (!msum.empty())
1401 : : {
1402 : 2006 : rem = ArithMSum::mkNode(nm, msum);
1403 : : }
1404 : : }
1405 : : }
1406 : : else
1407 : : {
1408 : 0 : DebugUnhandled();
1409 : : }
1410 : :
1411 : : // if there is a factor of PI
1412 [ + + ]: 3524 : if (!pi_factor.isNull())
1413 : : {
1414 [ + - ]: 4166 : Trace("arith-tf-rewrite-debug")
1415 : 2083 : << "Process pi factor = " << pi_factor << std::endl;
1416 : 2083 : Rational r = pi_factor.getConst<Rational>();
1417 : 2083 : Rational r_abs = r.abs();
1418 : 2083 : Rational rone = Rational(1);
1419 : 2083 : Rational rtwo = Rational(2);
1420 [ + + ]: 2083 : if (r_abs > rone)
1421 : : {
1422 : : // add/substract 2*pi beyond scope
1423 : 1 : Rational ra_div_two = (r_abs + rone) / rtwo;
1424 : 1 : Node new_pi_factor;
1425 [ + - ]: 1 : if (r.sgn() == 1)
1426 : : {
1427 : 1 : new_pi_factor = nm->mkConstReal(r - rtwo * ra_div_two.floor());
1428 : : }
1429 : : else
1430 : : {
1431 : 0 : Assert(r.sgn() == -1);
1432 : 0 : new_pi_factor = nm->mkConstReal(r + rtwo * ra_div_two.floor());
1433 : : }
1434 : 2 : Node new_arg = nm->mkNode(Kind::MULT, new_pi_factor, pi);
1435 [ + - ]: 1 : if (!rem.isNull())
1436 : : {
1437 : 1 : new_arg = nm->mkNode(Kind::ADD, new_arg, rem);
1438 : : }
1439 : 1 : new_arg = rewriter::ensureReal(new_arg);
1440 : : // sin( 2*n*PI + x ) = sin( x )
1441 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1442 : 2 : nm->mkNode(Kind::SINE, new_arg));
1443 : 1 : }
1444 [ + + ]: 2082 : else if (r_abs == rone)
1445 : : {
1446 : : // sin( PI + x ) = -sin( x )
1447 [ + + ]: 12 : if (rem.isNull())
1448 : : {
1449 : : return RewriteResponse(REWRITE_DONE,
1450 : 4 : nm->mkConstReal(Rational(0)));
1451 : : }
1452 : : else
1453 : : {
1454 : 10 : rem = rewriter::ensureReal(rem);
1455 : : return RewriteResponse(
1456 : : REWRITE_AGAIN_FULL,
1457 : 20 : nm->mkNode(Kind::NEG, nm->mkNode(Kind::SINE, rem)));
1458 : : }
1459 : : }
1460 [ + + ]: 2070 : else if (rem.isNull())
1461 : : {
1462 : : // other rational cases based on Niven's theorem
1463 : : // (https://en.wikipedia.org/wiki/Niven%27s_theorem)
1464 : 75 : Integer one = Integer(1);
1465 : 75 : Integer two = Integer(2);
1466 : 75 : Integer six = Integer(6);
1467 [ + - ]: 75 : if (r_abs.getDenominator() == two)
1468 : : {
1469 [ - + ][ - + ]: 75 : Assert(r_abs.getNumerator() == one);
[ - - ]
1470 : : return RewriteResponse(REWRITE_DONE,
1471 : 150 : nm->mkConstReal(Rational(r.sgn())));
1472 : : }
1473 [ - - ]: 0 : else if (r_abs.getDenominator() == six)
1474 : : {
1475 : 0 : Integer five = Integer(5);
1476 : 0 : if (r_abs.getNumerator() == one || r_abs.getNumerator() == five)
1477 : : {
1478 : : return RewriteResponse(
1479 : : REWRITE_DONE,
1480 : 0 : nm->mkConstReal(Rational(r.sgn()) / Rational(2)));
1481 : : }
1482 [ - - ]: 0 : }
1483 [ - + ][ - + ]: 225 : }
[ - + ]
1484 [ + + ][ + + ]: 2347 : }
[ + + ][ + + ]
1485 [ + + ][ + + ]: 3788 : }
[ + + ][ + + ]
1486 : 5430 : break;
1487 : 258 : case Kind::COSINE:
1488 : : {
1489 : : return RewriteResponse(
1490 : : REWRITE_AGAIN_FULL,
1491 : 516 : nm->mkNode(
1492 : : Kind::SINE,
1493 : 1032 : nm->mkNode(Kind::SUB,
1494 [ + + ][ - - ]: 1290 : nm->mkNode(Kind::MULT,
1495 : 516 : {nm->mkConstReal(Rational(1) / Rational(2)),
1496 : 516 : mkPi(nm)}),
1497 : 258 : t[0])));
1498 : : }
1499 : : break;
1500 : 57 : case Kind::TANGENT:
1501 : : {
1502 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1503 [ + + ][ - - ]: 285 : nm->mkNode(Kind::DIVISION,
1504 : 114 : {nm->mkNode(Kind::SINE, t[0]),
1505 : 171 : nm->mkNode(Kind::COSINE, t[0])}));
1506 : : }
1507 : : break;
1508 : 20 : case Kind::COSECANT:
1509 : : {
1510 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1511 [ + + ][ - - ]: 100 : nm->mkNode(Kind::DIVISION,
1512 : 40 : {nm->mkConstReal(Rational(1)),
1513 : 60 : nm->mkNode(Kind::SINE, t[0])}));
1514 : : }
1515 : : break;
1516 : 33 : case Kind::SECANT:
1517 : : {
1518 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1519 [ + + ][ - - ]: 165 : nm->mkNode(Kind::DIVISION,
1520 : 66 : {nm->mkConstReal(Rational(1)),
1521 : 99 : nm->mkNode(Kind::COSINE, t[0])}));
1522 : : }
1523 : : break;
1524 : 22 : case Kind::COTANGENT:
1525 : : {
1526 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1527 [ + + ][ - - ]: 110 : nm->mkNode(Kind::DIVISION,
1528 : 44 : {nm->mkNode(Kind::COSINE, t[0]),
1529 : 66 : nm->mkNode(Kind::SINE, t[0])}));
1530 : : }
1531 : : break;
1532 : 338 : default: break;
1533 : : }
1534 : 6293 : return RewriteResponse(REWRITE_DONE, t);
1535 : : }
1536 : :
1537 : 46125 : Node ArithRewriter::expandDefinition(Node node)
1538 : : {
1539 : : // call eliminate operators, to eliminate partial operators only
1540 : 46125 : std::vector<SkolemLemma> lems;
1541 : 46125 : TrustNode ret = d_opElim.eliminate(node, lems, true);
1542 [ - + ][ - + ]: 46125 : Assert(lems.empty());
[ - - ]
1543 [ + + ]: 46125 : if (ret.isNull())
1544 : : {
1545 : 45926 : return Node::null();
1546 : : }
1547 : 199 : return ret.getNode();
1548 : 46125 : }
1549 : :
1550 : 8082 : RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r)
1551 : : {
1552 [ + - ]: 16164 : Trace("arith-rewriter") << "ArithRewriter : " << t << " == " << ret << " by "
1553 : 8082 : << r << std::endl;
1554 : 8082 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1555 : : }
1556 : :
1557 : 223456 : Node ArithRewriter::rewriteIneqToBv(const Node& ineq)
1558 : : {
1559 [ - + ][ - + ]: 223456 : Assert(ineq.getKind() == Kind::GEQ);
[ - - ]
1560 : :
1561 : 446912 : Node left = rewriter::removeToReal(ineq[0]);
1562 : 446912 : Node right = rewriter::removeToReal(ineq[1]);
1563 : :
1564 : 223456 : rewriter::Sum sum;
1565 : 223456 : rewriter::addToSum(sum, left, false);
1566 : 223456 : rewriter::addToSum(sum, right, true);
1567 : :
1568 : 446912 : return rewriteIneqToBv(Kind::GEQ, sum, ineq);
1569 : 223456 : }
1570 : :
1571 : 223456 : Node ArithRewriter::rewriteIneqToBv(Kind kind,
1572 : : const rewriter::Sum& sum,
1573 : : const Node& ineq)
1574 : : {
1575 : 223456 : bool convertible = true;
1576 : : // the (single) bv2nat term in the sum
1577 : 223456 : Node bv2natTerm;
1578 : : // whether the bv2nat term is positive in the sum
1579 : 223456 : bool bv2natPol = false;
1580 : : // the remaining sum (constant)
1581 : 223456 : std::vector<Node> otherSum;
1582 : 223456 : NodeManager* nm = nodeManager();
1583 [ + + ]: 361981 : for (const std::pair<const Node, RealAlgebraicNumber>& m : sum)
1584 : : {
1585 [ + - ]: 361940 : if (m.second.isRational())
1586 : : {
1587 : 361940 : const Rational& r = m.second.toRational();
1588 : 361940 : Kind mk = m.first.getKind();
1589 [ + + ]: 361940 : if (mk == Kind::BITVECTOR_UBV_TO_INT)
1590 : : {
1591 : : // We currently only eliminate sums involving exactly one
1592 : : // (bv2nat x) monomial whose coefficient is +- 1, although more
1593 : : // cases could be handled here.
1594 [ + + ]: 47 : if (bv2natTerm.isNull())
1595 : : {
1596 [ + + ]: 45 : if (r.abs().isOne())
1597 : : {
1598 : 43 : bv2natPol = (r.sgn() == 1);
1599 : 43 : bv2natTerm = m.first;
1600 : 43 : continue;
1601 : : }
1602 : : }
1603 : : else
1604 : : {
1605 : 2 : convertible = false;
1606 : 2 : break;
1607 : : }
1608 : : }
1609 [ + + ][ + - ]: 361893 : else if (mk == Kind::CONST_INTEGER && m.second.isRational())
[ + + ]
1610 : : {
1611 [ + + ]: 148641 : if (r.isIntegral())
1612 : : {
1613 : 138482 : otherSum.push_back(nm->mkConstInt(r));
1614 : 138482 : continue;
1615 : : }
1616 : : }
1617 : : // if a non-constant, non-bv2nat term is in the sum, we fail
1618 [ + + ][ + ]: 361940 : }
1619 : 223413 : convertible = false;
1620 : 223413 : break;
1621 : : }
1622 [ + + ][ + - ]: 223456 : if (convertible && !bv2natTerm.isNull())
[ + + ]
1623 : : {
1624 : 41 : Node zero = nm->mkConstInt(Rational(0));
1625 : 41 : Kind bvKind =
1626 : : (kind == Kind::GT
1627 [ - + ][ - - ]: 82 : ? (bv2natPol ? Kind::BITVECTOR_UGT : Kind::BITVECTOR_ULT)
1628 [ + - ]: 41 : : (bv2natPol ? Kind::BITVECTOR_UGE : Kind::BITVECTOR_ULE));
1629 : 41 : Node bvt = bv2natTerm[0];
1630 : 41 : size_t bvsize = bvt.getType().getBitVectorSize();
1631 : 82 : Node w = nm->mkConstInt(Rational(Integer(2).pow(bvsize)));
1632 : 41 : Node osum = otherSum.empty()
1633 : : ? zero
1634 : 40 : : (otherSum.size() == 1 ? otherSum[0]
1635 [ + + ][ + - ]: 81 : : nm->mkNode(Kind::ADD, otherSum));
1636 : : // possibly negate the sum
1637 : : Node o = bv2natPol
1638 : 41 : ? (osum.getKind() == Kind::NEG ? osum[0]
1639 : : : nm->mkNode(Kind::NEG, osum))
1640 [ + - ][ - + ]: 82 : : osum;
[ + - ][ - - ]
1641 : 82 : Node ub = nm->mkNode(Kind::GEQ, o, w);
1642 : 82 : Node lb = nm->mkNode(Kind::LT, o, zero);
1643 : 41 : Node iToBvop = nm->mkConst(IntToBitVector(bvsize));
1644 : 164 : Node ret = nm->mkNode(
1645 : : Kind::ITE,
1646 : : {ub,
1647 : 41 : nm->mkConst(!bv2natPol),
1648 : 328 : nm->mkNode(
1649 : : Kind::ITE,
1650 : : {lb,
1651 : 82 : nm->mkConst(bv2natPol),
1652 : 82 : nm->mkNode(bvKind,
1653 : : bvt,
1654 : 246 : nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, o))})});
1655 : : // E.g. (<= (bv2nat x) N) -->
1656 : : // (ite (>= N 2^w) true (ite (< N 0) false (bvule x ((_ int2bv w) N))
1657 : : // or (<= N (bv2nat x)) -->
1658 : : // (ite (>= N 2^w) false (ite (< N 0) true (bvuge x ((_ int2bv w) N))
1659 : : // where N is a constant. Note that ((_ int2bv w) N) will subsequently
1660 : : // be rewritten to the appropriate bitvector constant.
1661 : 41 : return ret;
1662 : 41 : }
1663 : 223415 : return ineq;
1664 : 223456 : }
1665 : :
1666 : 221 : Node ArithRewriter::expandPowConst(NodeManager* nm, const Node& t)
1667 : : {
1668 [ + + ]: 221 : if (t[1].isConst())
1669 : : {
1670 : 213 : const Rational& exp = t[1].getConst<Rational>();
1671 [ - + ]: 213 : if (!exp.isIntegral())
1672 : : {
1673 : 209 : return Node::null();
1674 : : }
1675 : 213 : TNode base = t[0];
1676 [ + + ]: 213 : if (exp.sgn() == 0)
1677 : : {
1678 : 40 : return nm->mkConstRealOrInt(t.getType(), Rational(1));
1679 : : }
1680 [ + + ]: 193 : else if (exp.sgn() > 0)
1681 : : {
1682 : 191 : Rational r(expr::NodeValue::MAX_CHILDREN);
1683 [ + + ]: 191 : if (exp <= r)
1684 : : {
1685 : 189 : unsigned num = exp.getNumerator().toUnsignedInt();
1686 : 189 : Node ret;
1687 [ + + ]: 189 : if (num == 1)
1688 : : {
1689 : 22 : ret = base;
1690 : : }
1691 : : else
1692 : : {
1693 : 167 : NodeBuilder nb(nm, Kind::MULT);
1694 [ + + ]: 910 : for (unsigned i = 0; i < num; ++i)
1695 : : {
1696 : 743 : nb << base;
1697 : : }
1698 [ - + ][ - + ]: 167 : Assert(nb.getNumChildren() > 0);
[ - - ]
1699 : 167 : ret = nb;
1700 : 167 : }
1701 : 189 : return ret;
1702 : 189 : }
1703 [ + + ]: 191 : }
1704 [ + + ]: 213 : }
1705 : 12 : return Node::null();
1706 : : }
1707 : :
1708 : : } // namespace arith
1709 : : } // namespace theory
1710 : : } // namespace cvc5::internal
|
