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 : 5404197 : bool flattenAndCollectSum(TNode t,
62 : : std::vector<std::pair<TNode, Rational>>& children,
63 : : Kinds... kinds)
64 : : {
65 [ + + ]: 5404197 : if (!expr::algorithm::canFlatten(t, kinds...))
66 : : {
67 : 4854790 : 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 : 549407 : std::map<TNode, Rational> countMap;
75 : 549407 : countMap[t] = Rational(1);
76 : 549407 : std::map<TNode, Rational>::iterator it;
77 : 549407 : Kind tk = t.getKind();
78 [ + + ]: 7999301 : 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 : 3724947 : std::map<TNode, Rational>::iterator cur = std::prev(countMap.end());
83 : 3724947 : bool recurse = false;
84 : 3724947 : TNode tc = cur->first;
85 : 3724947 : Kind k = tc.getKind();
86 : 3724947 : Rational coeff = cur->second;
87 : 3724947 : countMap.erase(cur);
88 : : // Additionally collect coefficient
89 [ + + ][ + - ]: 4728147 : while (k == Kind::MULT && tc.getNumChildren() == 2 && tc[0].isConst())
[ + + ][ + + ]
[ + + ][ - - ]
90 : : {
91 : 1003200 : coeff *= tc[0].getConst<Rational>();
92 : 1003200 : tc = tc[1];
93 : 1003200 : 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 [ + + ][ + + ]: 3724947 : recurse = ((kinds == k) || ...);
103 : : }
104 [ + + ]: 3724947 : if (recurse)
105 : : {
106 [ + + ]: 6830531 : for (TNode cc : tc)
107 : : {
108 : 3604583 : countMap[cc] += coeff;
109 : : }
110 : : }
111 : : else
112 : : {
113 : 2111973 : children.emplace_back(tc, coeff);
114 : : }
115 : : }
116 : 549407 : return true;
117 : 549407 : }
118 : :
119 : 28852 : ArithRewriter::ArithRewriter(NodeManager* nm,
120 : : OperatorElim& oe,
121 : 28852 : bool expertEnabled)
122 : 28852 : : TheoryRewriter(nm), d_opElim(oe), d_expertEnabled(expertEnabled)
123 : : {
124 : 28852 : registerProofRewriteRule(ProofRewriteRule::ARITH_POW_ELIM,
125 : : TheoryRewriteCtx::PRE_DSL);
126 : 28852 : registerProofRewriteRule(ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL,
127 : : TheoryRewriteCtx::DSL_SUBCALL);
128 : 28852 : registerProofRewriteRule(ProofRewriteRule::MACRO_ARITH_INT_EQ_CONFLICT,
129 : : TheoryRewriteCtx::DSL_SUBCALL);
130 : 28852 : 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 : 28852 : }
136 : :
137 : 2054639 : Node ArithRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
138 : : {
139 [ + + ][ + + ]: 2054639 : switch (id)
[ + + ]
140 : : {
141 : 217998 : case ProofRewriteRule::ARITH_POW_ELIM:
142 : : {
143 [ + + ]: 217998 : if (n.getKind() == Kind::POW)
144 : : {
145 : 28 : Node nx = expandPowConst(nodeManager(), n);
146 [ + - ]: 28 : if (!nx.isNull())
147 : : {
148 : 28 : return nx;
149 : : }
150 [ - + ]: 28 : }
151 : : }
152 : 217970 : break;
153 : 613437 : case ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL:
154 : : {
155 : : // only matters if n contains integer string operators
156 : 1134000 : if (!n.getType().isBoolean() || n.getNumChildren() != 2 || n[0] == n[1]
157 : 1134000 : || !expr::hasSubtermKinds(
158 : : {Kind::STRING_LENGTH, Kind::STRING_INDEXOF, Kind::STRING_STOI},
159 : : n))
160 : : {
161 : 501491 : return Node::null();
162 : : }
163 [ + - ]: 111946 : 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 : 111946 : theory::strings::ArithEntail ae(d_nm, nullptr);
168 : 111946 : Node tgt;
169 [ + + ]: 111946 : if (n.getKind() == Kind::EQUAL)
170 : : {
171 : 17859 : tgt = n;
172 : : }
173 : : else
174 : : {
175 : 94087 : tgt = ae.normalizeGeq(n);
176 : : }
177 : 111946 : if (tgt.isNull() || !tgt[0].getType().isInteger())
178 : : {
179 : 99 : 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 : 111847 : Node nexp = ae.rewriteLengthIntro(tgt);
184 [ + - ]: 111847 : Trace("macro-arith-str-pred") << "...setup to " << nexp << std::endl;
185 : : // Also must make this a "simple" check (isSimple = true).
186 : 111847 : Node ret = ae.rewritePredViaEntailment(nexp, true);
187 [ + - ]: 111847 : Trace("macro-arith-str-pred") << "...result = " << ret << std::endl;
188 : 111847 : return ret;
189 : 111946 : }
190 : : break;
191 : 218 : case ProofRewriteRule::ARITH_STRING_PRED_ENTAIL:
192 : : case ProofRewriteRule::ARITH_STRING_PRED_SAFE_APPROX:
193 : : {
194 [ + - ][ - + ]: 436 : if (n.getKind() != Kind::GEQ || !n[1].isConst()
[ - - ]
195 [ + - ][ - + ]: 436 : || n[1].getConst<Rational>().sgn() != 0)
[ + - ][ + - ]
[ - - ]
196 : : {
197 : 0 : return Node::null();
198 : : }
199 [ + + ]: 218 : if (id == ProofRewriteRule::ARITH_STRING_PRED_ENTAIL)
200 : : {
201 [ + - ]: 142 : if (theory::strings::ArithEntail::checkSimple(n[0]))
202 : : {
203 : 284 : return nodeManager()->mkConst(true);
204 : : }
205 : : }
206 [ + - ]: 76 : 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 : 76 : theory::strings::ArithEntail ae(nodeManager(), nullptr);
211 : : // must only use simple checks when computing the approximations
212 : 76 : Node approx = ae.findApprox(n[0], true);
213 [ + - ]: 76 : if (approx != n[0])
214 : : {
215 [ + - ]: 152 : Trace("arith-rewriter-proof")
216 [ - + ][ - - ]: 76 : << n[0] << " --> " << approx << " by safe approx" << std::endl;
217 : 76 : return nodeManager()->mkNode(Kind::GEQ, approx, n[1]);
218 : : }
219 [ - + ][ - + ]: 152 : }
220 : : }
221 : 0 : break;
222 : 611577 : case ProofRewriteRule::MACRO_ARITH_INT_EQ_CONFLICT:
223 : : {
224 : 611577 : if (n.getKind() == Kind::EQUAL && n[0] != n[1])
225 : : {
226 [ + + ][ + + ]: 91123 : Node a = n[0].getKind() == Kind::TO_REAL ? n[0][0] : n[0];
[ - - ]
227 [ + + ][ + + ]: 91056 : Node b = n[1].getKind() == Kind::TO_REAL ? n[1][0] : n[1];
[ - - ]
228 : 90825 : rewriter::Sum sum;
229 : : // allow dropping TO_REAL
230 : 90825 : rewriter::addToSumNoMixed(sum, a, false);
231 : 90825 : rewriter::addToSumNoMixed(sum, b, true);
232 [ + + ]: 90825 : if (rewriter::isIntegral(sum))
233 : : {
234 : 70483 : std::pair<Node, Node> p = decomposeSum(d_nm, std::move(sum));
235 : 70483 : Rational c = p.second.getConst<Rational>();
236 [ + + ]: 70483 : if (!c.isIntegral())
237 : : {
238 : 468 : return d_nm->mkConst(false);
239 : : }
240 [ + + ][ + + ]: 70717 : }
241 [ + + ][ + + ]: 91293 : }
[ + + ]
242 : : }
243 : 611343 : break;
244 : 611404 : case ProofRewriteRule::MACRO_ARITH_INT_GEQ_TIGHTEN:
245 : : {
246 [ + - ]: 611404 : Trace("arith-rewriter-proof") << "Rewrite " << n << "?" << std::endl;
247 : 611404 : if (n.getKind() == Kind::GEQ && n[0] != n[1])
248 : : {
249 [ + + ][ + + ]: 210844 : Node a = n[0].getKind() == Kind::TO_REAL ? n[0][0] : n[0];
[ - - ]
250 [ + + ][ + + ]: 210727 : Node b = n[1].getKind() == Kind::TO_REAL ? n[1][0] : n[1];
[ - - ]
251 : 210560 : rewriter::Sum sum;
252 : : // allow dropping TO_REAL
253 : 210560 : rewriter::addToSumNoMixed(sum, a, false);
254 : 210560 : rewriter::addToSumNoMixed(sum, b, true);
255 [ + + ]: 210560 : if (rewriter::isIntegral(sum))
256 : : {
257 : : // decompose the sum into a non-constant and constant part
258 : 171541 : bool negated = false;
259 : : std::pair<Node, Node> p =
260 : 171541 : decomposeSum(d_nm, std::move(sum), negated, true);
261 : 171541 : Rational c = p.second.getConst<Rational>();
262 [ + - ]: 343082 : Trace("arith-rewriter-proof")
263 : 171541 : << "Decomposed to " << p.first << " + " << p.second << std::endl;
264 [ + + ]: 171541 : if (!c.isIntegral())
265 : : {
266 : 177 : c = -c;
267 : 177 : c = c.ceiling();
268 : 354 : Node ret = d_nm->mkNode(Kind::GEQ, p.first, d_nm->mkConstInt(c));
269 [ + + ]: 177 : if (negated)
270 : : {
271 : 83 : ret = ret.notNode();
272 : : }
273 : 177 : return ret;
274 : 177 : }
275 [ + + ][ + + ]: 171718 : }
276 [ + + ][ + + ]: 210914 : }
[ + + ]
277 : : }
278 : 611227 : break;
279 : 5 : default: break;
280 : : }
281 : 1440545 : return Node::null();
282 : : }
283 : :
284 : 12879952 : RewriteResponse ArithRewriter::preRewrite(TNode t)
285 : : {
286 [ + - ]: 12879952 : Trace("arith-rewriter") << "preRewrite(" << t << ")" << std::endl;
287 [ + + ]: 12879952 : if (rewriter::isAtom(t))
288 : : {
289 : 6813970 : auto res = preRewriteAtom(t);
290 [ + - ]: 13627940 : Trace("arith-rewriter")
291 : 6813970 : << res.d_status << " -> " << res.d_node << std::endl;
292 : 6813970 : return res;
293 : 6813970 : }
294 : 6065982 : auto res = preRewriteTerm(t);
295 [ + - ]: 6065982 : Trace("arith-rewriter") << res.d_status << " -> " << res.d_node << std::endl;
296 : 6065982 : return res;
297 : 6065982 : }
298 : :
299 : 10978223 : RewriteResponse ArithRewriter::postRewrite(TNode t)
300 : : {
301 [ + - ]: 10978223 : Trace("arith-rewriter") << "postRewrite(" << t << ")" << std::endl;
302 [ + + ]: 10978223 : if (rewriter::isAtom(t))
303 : : {
304 : 5728765 : auto res = postRewriteAtom(t);
305 [ + - ]: 11457530 : Trace("arith-rewriter")
306 : 5728765 : << res.d_status << " -> " << res.d_node << std::endl;
307 : 5728765 : return res;
308 : 5728765 : }
309 : 5249458 : auto res = postRewriteTerm(t);
310 [ + - ]: 5249458 : Trace("arith-rewriter") << res.d_status << " -> " << res.d_node << std::endl;
311 : 5249458 : return res;
312 : 5249458 : }
313 : :
314 : 6813970 : RewriteResponse ArithRewriter::preRewriteAtom(TNode atom)
315 : : {
316 [ - + ][ - + ]: 6813970 : Assert(rewriter::isAtom(atom));
[ - - ]
317 : :
318 : 6813970 : Kind kind = atom.getKind();
319 [ + + ]: 6813970 : if (atom.getNumChildren() == 2)
320 : : {
321 [ + + ]: 6813021 : if (auto response =
322 : 6813021 : rewriter::tryEvaluateRelationReflexive(kind, atom[0], atom[1]);
323 : 6813021 : response)
324 : : {
325 : 198850 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, *response));
326 : : }
327 : : }
328 : :
329 [ + + ][ + + ]: 6714545 : switch (kind)
[ + ]
330 : : {
331 : 252077 : case Kind::GT:
332 : : return RewriteResponse(
333 : : REWRITE_DONE,
334 : 504154 : rewriter::buildRelation(Kind::LEQ, atom[0], atom[1], true));
335 : 249757 : case Kind::LT:
336 : : return RewriteResponse(
337 : : REWRITE_DONE,
338 : 499514 : rewriter::buildRelation(Kind::GEQ, atom[0], atom[1], true));
339 : 871 : case Kind::IS_INTEGER:
340 [ + + ]: 871 : if (atom[0].getType().isInteger())
341 : : {
342 : 10 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, true));
343 : : }
344 : 866 : 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 : 6212706 : default:;
352 : : }
353 : :
354 : 6212706 : return RewriteResponse(REWRITE_DONE, atom);
355 : : }
356 : :
357 : 5728765 : RewriteResponse ArithRewriter::postRewriteAtom(TNode atom)
358 : : {
359 [ - + ][ - + ]: 5728765 : Assert(rewriter::isAtom(atom));
[ - - ]
360 [ + - ]: 5728765 : Trace("arith-rewriter") << "postRewriteAtom: " << atom << std::endl;
361 : :
362 [ + + ]: 5728765 : if (atom.getKind() == Kind::IS_INTEGER)
363 : : {
364 : 832 : return rewriteExtIntegerOp(atom);
365 : : }
366 [ + + ]: 5727933 : 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 : 5727894 : Kind kind = atom.getKind();
389 : 11455788 : Node left = rewriter::removeToReal(atom[0]);
390 : 11455788 : Node right = rewriter::removeToReal(atom[1]);
391 : :
392 [ + + ]: 11455788 : if (auto response = rewriter::tryEvaluateRelationReflexive(kind, left, right);
393 : 5727894 : response)
394 : : {
395 : 369266 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, *response));
396 : : }
397 : :
398 [ - + ][ - + ]: 5543261 : Assert(isRelationOperator(kind));
[ - - ]
399 : :
400 [ + + ]: 11086522 : if (auto response = rewriter::tryEvaluateRelation(kind, left, right);
401 : 5543261 : response)
402 : : {
403 : 1050314 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, *response));
404 : : }
405 : :
406 [ + + ]: 5018104 : if (kind == Kind::EQUAL)
407 : : {
408 : : // We do not normalize equalities here, since this does not preserve their
409 : : // terms, see rewriter::normalizeEquality. However, if the normal form of
410 : : // the equality is a Boolean constant, we return that constant, which e.g.
411 : : // is the case for (= (* 2 x) 1) for integer x. This ensures that the
412 : : // rewritten form of an equality is a Boolean constant whenever it is
413 : : // equivalent to one, which is relied upon e.g. when setting up atoms in
414 : : // the linear solver.
415 : 2144068 : bool negated = false;
416 : 2144068 : Node norm = rewriter::normalizeEquality(d_nm, atom, &negated);
417 [ + + ]: 2144068 : if (norm.isConst())
418 : : {
419 : 7132 : return RewriteResponse(REWRITE_DONE, norm);
420 : : }
421 : : // Otherwise, we only orient the equality, which we do so that it points in
422 : : // the same direction as its normal form, i.e. so that the difference of
423 : : // its sides is a positive multiple of the difference of the sides of norm.
424 : : // Note this makes the normal form of an equality itself in rewritten form,
425 : : // which ensures that the linear solver does not have to introduce a second
426 : : // atom for an equality that is already in normal form, see
427 : : // TheoryArithPrivate::setupAtom.
428 [ + + ]: 2136936 : if (negated)
429 : : {
430 : : return RewriteResponse(REWRITE_DONE,
431 : 727012 : d_nm->mkNode(Kind::EQUAL, atom[1], atom[0]));
432 : : }
433 : 1773430 : return RewriteResponse(REWRITE_DONE, atom);
434 : 2144068 : }
435 : :
436 : : // Equalities were handled above, hence the atom is an inequality here.
437 [ - + ][ - + ]: 2874036 : Assert(kind != Kind::EQUAL);
[ - - ]
438 : 2874036 : bool negate = false;
439 : :
440 [ + - ][ + ]: 2874036 : switch (atom.getKind())
441 : : {
442 : 326145 : case Kind::LEQ:
443 : 326145 : kind = Kind::GEQ;
444 : 326145 : negate = true;
445 : 326145 : break;
446 : 0 : case Kind::LT:
447 : 0 : kind = Kind::GT;
448 : 0 : negate = true;
449 : 0 : break;
450 : 2547891 : default: break;
451 : : }
452 : :
453 : 5748072 : rewriter::Sum sum;
454 : 2874036 : rewriter::addToSum(sum, left, negate);
455 : 2874036 : rewriter::addToSum(sum, right, !negate);
456 : :
457 : : // Now we have (sum <kind> 0)
458 [ + + ]: 2874036 : if (rewriter::isIntegral(sum))
459 : : {
460 [ + - ]: 1781982 : Trace("arith-rewriter") << "...sum is integral" << std::endl;
461 : : return RewriteResponse(
462 : : REWRITE_DONE,
463 : 3563964 : rewriter::buildIntegerInequality(d_nm, std::move(sum), kind));
464 : : }
465 : : else
466 : : {
467 [ + - ]: 1092054 : Trace("arith-rewriter") << "...sum is not integral" << std::endl;
468 : : return RewriteResponse(
469 : : REWRITE_DONE,
470 : 2184108 : rewriter::buildRealInequality(d_nm, std::move(sum), kind));
471 : : }
472 : 5727894 : }
473 : :
474 : 43773 : Node ArithRewriter::rewriteEqualityExt(Node node)
475 : : {
476 [ - + ][ - + ]: 43773 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
477 [ - + ]: 43773 : if (!node[0].getType().isRealOrInt())
478 : : {
479 : 0 : return node;
480 : : }
481 : 43773 : return rewriter::normalizeEquality(d_nm, node);
482 : : }
483 : :
484 : 6065982 : RewriteResponse ArithRewriter::preRewriteTerm(TNode t)
485 : : {
486 [ + + ]: 6065982 : if (t.isConst())
487 : : {
488 : 828056 : return RewriteResponse(REWRITE_DONE, t);
489 : : }
490 [ - + ]: 5237926 : else if (t.isVar())
491 : : {
492 : 0 : return rewriteVariable(t);
493 : : }
494 : : else
495 : : {
496 [ + + ][ + + ]: 5237926 : switch (Kind k = t.getKind())
[ + + ][ + + ]
[ + + ][ - ]
497 : : {
498 : 229 : case Kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
499 : 600816 : case Kind::SUB: return rewriteSub(t);
500 : 23679 : case Kind::NEG: return rewriteNeg(t, true);
501 : 11004 : case Kind::DIVISION:
502 : 11004 : case Kind::DIVISION_TOTAL: return rewriteDiv(t, true);
503 : 3150732 : case Kind::ADD: return preRewritePlus(t);
504 : 1367065 : case Kind::MULT:
505 : 1367065 : case Kind::NONLINEAR_MULT: return preRewriteMult(t);
506 : 8518 : case Kind::INTS_DIVISION:
507 : 8518 : case Kind::INTS_MODULUS: return rewriteIntsDivMod(t);
508 : 28504 : case Kind::INTS_DIVISION_TOTAL:
509 : 28504 : case Kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, true);
510 : 6939 : case Kind::ABS: return rewriteAbs(t);
511 : 40440 : case Kind::IAND:
512 : : case Kind::PIAND:
513 : : case Kind::POW2:
514 : : case Kind::INTS_ISPOW2:
515 : : case Kind::INTS_LOG2:
516 : : case Kind::EXPONENTIAL:
517 : : case Kind::SINE:
518 : : case Kind::COSINE:
519 : : case Kind::TANGENT:
520 : : case Kind::COSECANT:
521 : : case Kind::SECANT:
522 : : case Kind::COTANGENT:
523 : : case Kind::ARCSINE:
524 : : case Kind::ARCCOSINE:
525 : : case Kind::ARCTANGENT:
526 : : case Kind::ARCCOSECANT:
527 : : case Kind::ARCSECANT:
528 : : case Kind::ARCCOTANGENT:
529 : : case Kind::SQRT:
530 : : case Kind::IS_INTEGER:
531 : : case Kind::TO_INTEGER:
532 : : case Kind::TO_REAL:
533 : : case Kind::POW:
534 : 40440 : case Kind::PI: return RewriteResponse(REWRITE_DONE, t);
535 : 0 : default: Unhandled() << k;
536 : : }
537 : : }
538 : : }
539 : :
540 : 5249458 : RewriteResponse ArithRewriter::postRewriteTerm(TNode t)
541 : : {
542 [ + + ]: 5249458 : if (t.isConst())
543 : : {
544 : 1792019 : return RewriteResponse(REWRITE_DONE, t);
545 : : }
546 [ - + ]: 3457439 : else if (t.isVar())
547 : : {
548 : 0 : return rewriteVariable(t);
549 : : }
550 : : else
551 : : {
552 [ + - ]: 3457439 : Trace("arith-rewriter") << "postRewriteTerm: " << t << std::endl;
553 [ + - ][ - + ]: 3457439 : switch (t.getKind())
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ]
554 : : {
555 : 350 : case Kind::REAL_ALGEBRAIC_NUMBER: return rewriteRAN(t);
556 : 0 : case Kind::SUB: return rewriteSub(t);
557 : 0 : case Kind::NEG: return rewriteNeg(t, false);
558 : 5589 : case Kind::DIVISION:
559 : 5589 : case Kind::DIVISION_TOTAL: return rewriteDiv(t, false);
560 : 2253465 : case Kind::ADD: return postRewritePlus(t);
561 : 1118645 : case Kind::MULT:
562 : 1118645 : case Kind::NONLINEAR_MULT: return postRewriteMult(t);
563 : 136 : case Kind::INTS_ISPOW2: return postRewriteIntsIsPow2(t);
564 : 209 : case Kind::INTS_LOG2: return postRewriteIntsLog2(t);
565 : 6843 : case Kind::INTS_DIVISION:
566 : 6843 : case Kind::INTS_MODULUS: return rewriteIntsDivMod(t);
567 : 23236 : case Kind::INTS_DIVISION_TOTAL:
568 : 23236 : case Kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t, false);
569 : 6620 : case Kind::ABS: return rewriteAbs(t);
570 : 24346 : case Kind::TO_REAL: return rewriteToReal(t);
571 : 4396 : case Kind::TO_INTEGER: return rewriteExtIntegerOp(t);
572 : 915 : case Kind::PI: return RewriteResponse(REWRITE_DONE, t);
573 : 1982 : case Kind::POW2: return postRewritePow2(t);
574 : 775 : case Kind::PIAND: return postRewritePIAnd(t);
575 : : // expert cases
576 : 9932 : case Kind::POW:
577 : : case Kind::EXPONENTIAL:
578 : : case Kind::SINE:
579 : : case Kind::COSINE:
580 : : case Kind::TANGENT:
581 : : case Kind::COSECANT:
582 : : case Kind::SECANT:
583 : : case Kind::COTANGENT:
584 : : case Kind::ARCSINE:
585 : : case Kind::ARCCOSINE:
586 : : case Kind::ARCTANGENT:
587 : : case Kind::ARCCOSECANT:
588 : : case Kind::ARCSECANT:
589 : : case Kind::ARCCOTANGENT:
590 : : case Kind::SQRT:
591 : 9932 : case Kind::IAND: return postRewriteExpert(t);
592 : 0 : default: Unreachable();
593 : : }
594 : : }
595 : : }
596 : 9932 : RewriteResponse ArithRewriter::postRewriteExpert(TNode t)
597 : : {
598 [ - + ]: 9932 : if (!d_expertEnabled)
599 : : {
600 : 0 : return RewriteResponse(REWRITE_DONE, t);
601 : : }
602 [ + + ][ + - ]: 9932 : switch (t.getKind())
603 : : {
604 : 222 : case Kind::POW:
605 : : {
606 : 222 : Node tx = expandPowConst(nodeManager(), t);
607 [ + + ]: 222 : if (!tx.isNull())
608 : : {
609 : 210 : return RewriteResponse(REWRITE_AGAIN_FULL, tx);
610 : : }
611 : 12 : return RewriteResponse(REWRITE_DONE, t);
612 : 222 : }
613 : 7960 : case Kind::EXPONENTIAL:
614 : : case Kind::SINE:
615 : : case Kind::COSINE:
616 : : case Kind::TANGENT:
617 : : case Kind::COSECANT:
618 : : case Kind::SECANT:
619 : : case Kind::COTANGENT:
620 : : case Kind::ARCSINE:
621 : : case Kind::ARCCOSINE:
622 : : case Kind::ARCTANGENT:
623 : : case Kind::ARCCOSECANT:
624 : : case Kind::ARCSECANT:
625 : : case Kind::ARCCOTANGENT:
626 : 7960 : case Kind::SQRT: return postRewriteTranscendental(t);
627 : 1750 : case Kind::IAND: return postRewriteIAnd(t);
628 : 0 : default: Unreachable();
629 : : }
630 : : }
631 : :
632 : 579 : RewriteResponse ArithRewriter::rewriteRAN(TNode t)
633 : : {
634 [ - + ][ - + ]: 579 : Assert(rewriter::isRAN(t));
[ - - ]
635 [ - + ][ - + ]: 579 : Assert(t.getType().isReal());
[ - - ]
636 : 579 : const RealAlgebraicNumber& r = rewriter::getRAN(t);
637 [ - + ]: 579 : if (r.isRational())
638 : : {
639 : : return RewriteResponse(REWRITE_DONE,
640 : 0 : rewriter::mkConst(d_nm, r.toRational()));
641 : : }
642 : 579 : return RewriteResponse(REWRITE_DONE, t);
643 : : }
644 : :
645 : 0 : RewriteResponse ArithRewriter::rewriteVariable(TNode t)
646 : : {
647 : 0 : Assert(t.isVar());
648 : :
649 : 0 : return RewriteResponse(REWRITE_DONE, t);
650 : : }
651 : :
652 : 23679 : RewriteResponse ArithRewriter::rewriteNeg(TNode t, bool pre)
653 : : {
654 [ - + ][ - + ]: 23679 : Assert(t.getKind() == Kind::NEG);
[ - - ]
655 : :
656 : 23679 : NodeManager* nm = nodeManager();
657 [ + + ]: 23679 : if (t[0].isConst())
658 : : {
659 : 11018 : Rational neg = -(t[0].getConst<Rational>());
660 : : return RewriteResponse(REWRITE_DONE,
661 : 22036 : nm->mkConstRealOrInt(t.getType(), neg));
662 : 11018 : }
663 [ + + ]: 12661 : if (rewriter::isRAN(t[0]))
664 : : {
665 : : return RewriteResponse(REWRITE_DONE,
666 : 4 : rewriter::mkConst(d_nm, -rewriter::getRAN(t[0])));
667 : : }
668 : :
669 : : Node noUminus =
670 : 25318 : nm->mkNode(Kind::MULT, rewriter::mkConst(d_nm, Rational(-1)), t[0]);
671 [ + - ]: 12659 : if (pre)
672 : : {
673 : 12659 : return RewriteResponse(REWRITE_DONE, noUminus);
674 : : }
675 : : else
676 : : {
677 : 0 : return RewriteResponse(REWRITE_AGAIN, noUminus);
678 : : }
679 : 12659 : }
680 : :
681 : 600816 : RewriteResponse ArithRewriter::rewriteSub(TNode t)
682 : : {
683 [ - + ][ - + ]: 600816 : Assert(t.getKind() == Kind::SUB);
[ - - ]
684 [ - + ][ - + ]: 600816 : Assert(t.getNumChildren() == 2);
[ - - ]
685 : :
686 : 600816 : NodeManager* nm = nodeManager();
687 [ + + ]: 600816 : if (t[0] == t[1])
688 : : {
689 : : return RewriteResponse(REWRITE_DONE,
690 : 3330 : nm->mkConstRealOrInt(t.getType(), Rational(0)));
691 : : }
692 : : return RewriteResponse(
693 : : REWRITE_AGAIN_FULL,
694 : 1198302 : nm->mkNode(Kind::ADD,
695 : : t[0],
696 : 2396604 : nm->mkNode(Kind::MULT,
697 : 1198302 : nm->mkConstRealOrInt(t[1].getType(), Rational(-1)),
698 : 599151 : t[1])));
699 : : }
700 : :
701 : 3150732 : RewriteResponse ArithRewriter::preRewritePlus(TNode t)
702 : : {
703 [ - + ][ - + ]: 3150732 : Assert(t.getKind() == Kind::ADD);
[ - - ]
704 : 3150732 : std::vector<std::pair<TNode, Rational>> children;
705 [ + + ]: 3150732 : if (!flattenAndCollectSum(t, children, Kind::ADD))
706 : : {
707 : 2769875 : return RewriteResponse(REWRITE_DONE, t);
708 : : }
709 : 380857 : NodeManager* nm = nodeManager();
710 : 380857 : NodeBuilder nb(nm, Kind::ADD);
711 : 380857 : Rational coeff(0);
712 [ + + ]: 1864038 : for (const std::pair<TNode, Rational>& c : children)
713 : : {
714 [ + + ]: 1483181 : if (c.first.isConst())
715 : : {
716 : 572416 : coeff += c.first.getConst<Rational>() * c.second;
717 : : }
718 [ + + ]: 910765 : else if (c.second.isOne())
719 : : {
720 : 233443 : nb << c.first;
721 : : }
722 : : else
723 : : {
724 : 677322 : nb << nm->mkNode(Kind::MULT, nm->mkConstRealOrInt(c.second), c.first);
725 : : }
726 : : }
727 [ + + ][ + + ]: 380857 : if (!coeff.isZero() || nb.getNumChildren() == 0)
[ + + ]
728 : : {
729 : 286437 : nb << nm->mkConstRealOrInt(t.getType(), coeff);
730 : : }
731 [ + + ]: 380857 : Node ret = nb.getNumChildren() == 1 ? nb.getChild(0) : nb;
732 : 380857 : ret = rewriter::maybeEnsureReal(t.getType(), ret);
733 : 380857 : return RewriteResponse(REWRITE_DONE, ret);
734 : 3150732 : }
735 : :
736 : 2253465 : RewriteResponse ArithRewriter::postRewritePlus(TNode t)
737 : : {
738 [ - + ][ - + ]: 2253465 : Assert(t.getKind() == Kind::ADD);
[ - - ]
739 [ - + ][ - + ]: 2253465 : Assert(t.getNumChildren() > 1);
[ - - ]
740 : :
741 : 2253465 : rewriter::Sum sum;
742 : 2253465 : std::vector<std::pair<TNode, Rational>> children;
743 [ + + ]: 2253465 : if (!flattenAndCollectSum(t, children, Kind::ADD, Kind::TO_REAL))
744 : : {
745 : 2084915 : rewriter::addToSum(sum, t);
746 : : }
747 : : else
748 : : {
749 : 168550 : Rational coeff(0);
750 [ + + ]: 797342 : for (const std::pair<TNode, Rational>& c : children)
751 : : {
752 [ + + ]: 628792 : if (c.first.isConst())
753 : : {
754 : 237304 : coeff += c.first.getConst<Rational>() * c.second;
755 : : }
756 [ + + ]: 391488 : else if (c.second.isOne())
757 : : {
758 : 143150 : rewriter::addToSum(sum, c.first);
759 : : }
760 : : else
761 : : {
762 : 248338 : RealAlgebraicNumber mul = RealAlgebraicNumber(c.second);
763 : 248338 : rewriter::addMonomialToSum(sum, c.first, mul);
764 : 248338 : }
765 : : }
766 [ + + ]: 168550 : if (!coeff.isZero())
767 : : {
768 : 115462 : rewriter::addToSum(sum, nodeManager()->mkConstRealOrInt(coeff));
769 : : }
770 : 168550 : }
771 : 2253465 : Node retSum = rewriter::collectSum(d_nm, sum);
772 : 2253465 : retSum = rewriter::maybeEnsureReal(t.getType(), retSum);
773 : 4506930 : return RewriteResponse(REWRITE_DONE, retSum);
774 : 2253465 : }
775 : :
776 : 1367065 : RewriteResponse ArithRewriter::preRewriteMult(TNode node)
777 : : {
778 [ + + ][ + - ]: 1367065 : Assert(node.getKind() == Kind::MULT
[ - + ][ - + ]
[ - - ]
779 : : || node.getKind() == Kind::NONLINEAR_MULT);
780 : :
781 [ + + ]: 1367065 : if (auto res = rewriter::getZeroChild(node); res)
782 : : {
783 : : return RewriteResponse(REWRITE_DONE,
784 : 257002 : rewriter::maybeEnsureReal(node.getType(), *res));
785 [ + + ]: 1367065 : }
786 : 1238564 : return RewriteResponse(REWRITE_DONE, node);
787 : : }
788 : :
789 : 1118645 : RewriteResponse ArithRewriter::postRewriteMult(TNode t)
790 : : {
791 [ + + ][ + - ]: 1118645 : Assert(t.getKind() == Kind::MULT || t.getKind() == Kind::NONLINEAR_MULT);
[ - + ][ - + ]
[ - - ]
792 [ - + ][ - + ]: 1118645 : Assert(t.getNumChildren() >= 2);
[ - - ]
793 : :
794 : 1118645 : std::vector<TNode> children;
795 : 1118645 : expr::algorithm::flatten(
796 : : t, children, Kind::MULT, Kind::NONLINEAR_MULT, Kind::TO_REAL);
797 : :
798 [ + + ]: 1118645 : if (auto res = rewriter::getZeroChild(children); res)
799 : : {
800 : : return RewriteResponse(REWRITE_DONE,
801 : 14560 : rewriter::maybeEnsureReal(t.getType(), *res));
802 [ + + ]: 1118645 : }
803 : :
804 : 1111365 : RewriteStatus rs = REWRITE_DONE;
805 : 1111365 : Node ret;
806 : : // Distribute over addition
807 [ + + ]: 1111365 : if (std::any_of(children.begin(), children.end(), [](TNode child) {
808 : 2506496 : return child.getKind() == Kind::ADD;
809 : : }))
810 : : {
811 : : // if we distribute multiplication, we rewrite again to ensure the
812 : : // sum is sorted.
813 : 72927 : rs = REWRITE_AGAIN_FULL;
814 : 72927 : ret = rewriter::distributeMultiplication(d_nm, children);
815 : : }
816 : : else
817 : : {
818 : 1038438 : RealAlgebraicNumber ran = RealAlgebraicNumber(Integer(1));
819 : 1038438 : std::vector<Node> leafs;
820 : :
821 [ + + ]: 3401393 : for (const auto& child : children)
822 : : {
823 [ + + ]: 2362955 : if (child.isConst())
824 : : {
825 [ - + ]: 1122444 : if (child.getConst<Rational>().isZero())
826 : : {
827 : : return RewriteResponse(REWRITE_DONE,
828 : 0 : rewriter::maybeEnsureReal(t.getType(), child));
829 : : }
830 : 1122444 : ran *= child.getConst<Rational>();
831 : : }
832 [ + + ]: 1240511 : else if (rewriter::isRAN(child))
833 : : {
834 : 127 : ran *= rewriter::getRAN(child);
835 : : }
836 : : else
837 : : {
838 : 1240384 : leafs.emplace_back(child);
839 : : }
840 : : }
841 : 1038438 : ret = rewriter::mkMultTerm(d_nm, ran, std::move(leafs));
842 [ + - ][ + - ]: 1038438 : }
843 : 1111365 : ret = rewriter::maybeEnsureReal(t.getType(), ret);
844 : 1111365 : return RewriteResponse(rs, ret);
845 : 1118645 : }
846 : :
847 : 16593 : RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
848 : : {
849 [ + + ][ + - ]: 16593 : Assert(t.getKind() == Kind::DIVISION_TOTAL || t.getKind() == Kind::DIVISION);
[ - + ][ - + ]
[ - - ]
850 [ - + ][ - + ]: 16593 : Assert(t.getNumChildren() == 2);
[ - - ]
851 : :
852 : 33186 : Node left = rewriter::removeToReal(t[0]);
853 : 33186 : Node right = rewriter::removeToReal(t[1]);
854 : 16593 : NodeManager* nm = nodeManager();
855 [ + + ]: 16593 : if (right.isConst())
856 : : {
857 : 6577 : const Rational& den = right.getConst<Rational>();
858 : :
859 [ + + ]: 6577 : if (den.isZero())
860 : : {
861 [ + + ]: 1185 : if (t.getKind() == Kind::DIVISION_TOTAL)
862 : : {
863 : 169 : Node ret = nm->mkConstReal(0);
864 : 169 : return RewriteResponse(REWRITE_DONE, ret);
865 : 169 : }
866 : : else
867 : : {
868 : 2032 : Node ret = nm->mkNode(t.getKind(), left, right);
869 : 1016 : return RewriteResponse(REWRITE_DONE, ret);
870 : 1016 : }
871 : : }
872 [ - + ][ - + ]: 5392 : Assert(den != Rational(0));
[ - - ]
873 : :
874 [ + + ]: 5392 : if (left.isConst())
875 : : {
876 : 2122 : const Rational& num = left.getConst<Rational>();
877 : 4244 : return RewriteResponse(REWRITE_DONE, nm->mkConstReal(num / den));
878 : : }
879 [ - + ]: 3270 : if (rewriter::isRAN(left))
880 : : {
881 : : return RewriteResponse(REWRITE_DONE,
882 : 0 : rewriter::ensureReal(nm->mkRealAlgebraicNumber(
883 : 0 : rewriter::getRAN(left) / den)));
884 : : }
885 : :
886 : 3270 : Node result = nm->mkConstReal(den.inverse());
887 : : Node mult =
888 : 6540 : rewriter::ensureReal(nodeManager()->mkNode(Kind::MULT, left, result));
889 [ + + ]: 3270 : if (pre)
890 : : {
891 : 3244 : return RewriteResponse(REWRITE_DONE, mult);
892 : : }
893 : : // requires again full since ensureReal may have added a to_real
894 : 26 : return RewriteResponse(REWRITE_AGAIN_FULL, mult);
895 : 3270 : }
896 [ + + ]: 10016 : if (rewriter::isRAN(right))
897 : : {
898 : 4 : const RealAlgebraicNumber& den = rewriter::getRAN(right);
899 : : // mkConst is applied to RAN in this block, which are always Real
900 [ + + ]: 4 : if (left.isConst())
901 : : {
902 : : return RewriteResponse(
903 : : REWRITE_DONE,
904 : 4 : rewriter::ensureReal(rewriter::mkConst(
905 : 6 : d_nm, RealAlgebraicNumber(left.getConst<Rational>()) / den)));
906 : : }
907 [ + - ]: 2 : if (rewriter::isRAN(left))
908 : : {
909 : : return RewriteResponse(REWRITE_DONE,
910 : 4 : rewriter::ensureReal(rewriter::mkConst(
911 : 6 : d_nm, rewriter::getRAN(left) / den)));
912 : : }
913 : :
914 : 0 : Node result = rewriter::mkConst(d_nm, den.inverse());
915 : : Node mult =
916 : 0 : rewriter::ensureReal(nodeManager()->mkNode(Kind::MULT, left, result));
917 [ - - ]: 0 : if (pre)
918 : : {
919 : 0 : return RewriteResponse(REWRITE_DONE, mult);
920 : : }
921 : : // requires again full since ensureReal may have added a to_real
922 : 0 : return RewriteResponse(REWRITE_AGAIN_FULL, mult);
923 : 0 : }
924 : : // We also convert integral rationals in the numerator to integers,
925 : : // e.g. (/ 1 x) ---> (/ 1.0 x).
926 [ + + ]: 10012 : if (left.getKind() == Kind::CONST_INTEGER)
927 : : {
928 : 43 : left = nm->mkConstReal(left.getConst<Rational>());
929 : : }
930 : : // may have changed due to removing to_real
931 : 10012 : if (left != t[0] || right != t[1])
932 : : {
933 : 290 : Node ret = nm->mkNode(t.getKind(), left, right);
934 : 145 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
935 : 145 : }
936 : 9867 : return RewriteResponse(REWRITE_DONE, t);
937 : 16593 : }
938 : :
939 : 24346 : RewriteResponse ArithRewriter::rewriteToReal(TNode t)
940 : : {
941 [ - + ][ - + ]: 24346 : Assert(t.getKind() == Kind::TO_REAL);
[ - - ]
942 [ + + ]: 24346 : if (!t[0].getType().isInteger())
943 : : {
944 : : // if it is already real type, then just return the argument
945 : 2 : return RewriteResponse(REWRITE_DONE, t[0]);
946 : : }
947 : 24344 : NodeManager* nm = nodeManager();
948 [ + + ]: 24344 : if (t[0].isConst())
949 : : {
950 : : // If the argument is constant, return a real constant.
951 : 4564 : const Rational& rat = t[0].getConst<Rational>();
952 : 9128 : return RewriteResponse(REWRITE_DONE, nm->mkConstReal(rat));
953 : : }
954 [ - + ]: 19780 : if (t[0].getKind() == Kind::TO_REAL)
955 : : {
956 : : // (to_real (to_real t)) ---> (to_real t)
957 : 0 : return RewriteResponse(REWRITE_DONE, t[0]);
958 : : }
959 : 19780 : return RewriteResponse(REWRITE_DONE, t);
960 : : }
961 : :
962 : 13559 : RewriteResponse ArithRewriter::rewriteAbs(TNode t)
963 : : {
964 [ - + ][ - + ]: 13559 : Assert(t.getKind() == Kind::ABS);
[ - - ]
965 [ - + ][ - + ]: 13559 : Assert(t.getNumChildren() == 1);
[ - - ]
966 : :
967 [ + + ]: 13559 : if (t[0].isConst())
968 : : {
969 : 347 : const Rational& rat = t[0].getConst<Rational>();
970 [ + + ]: 347 : if (rat >= 0)
971 : : {
972 : 342 : return RewriteResponse(REWRITE_DONE, t[0]);
973 : : }
974 : : return RewriteResponse(
975 : 5 : REWRITE_DONE, nodeManager()->mkConstRealOrInt(t[0].getType(), -rat));
976 : : }
977 [ + + ]: 13212 : if (rewriter::isRAN(t[0]))
978 : : {
979 : 2 : const RealAlgebraicNumber& ran = rewriter::getRAN(t[0]);
980 [ + + ]: 2 : if (ran >= RealAlgebraicNumber())
981 : : {
982 : 1 : return RewriteResponse(REWRITE_DONE, t[0]);
983 : : }
984 : : return RewriteResponse(REWRITE_DONE,
985 : 2 : nodeManager()->mkRealAlgebraicNumber(-ran));
986 : : }
987 : 13210 : return RewriteResponse(REWRITE_DONE, t);
988 : : }
989 : :
990 : 15361 : RewriteResponse ArithRewriter::rewriteIntsDivMod(TNode t)
991 : : {
992 : 15361 : NodeManager* nm = nodeManager();
993 : 15361 : Kind k = t.getKind();
994 [ + + ]: 15361 : if (k == Kind::INTS_MODULUS)
995 : : {
996 : 11553 : if (t[1].isConst() && !t[1].getConst<Rational>().isZero())
997 : : {
998 : : // can immediately replace by INTS_MODULUS_TOTAL
999 : 4898 : Node ret = nm->mkNode(Kind::INTS_MODULUS_TOTAL, t[0], t[1]);
1000 : 2449 : return returnRewrite(t, ret, Rewrite::MOD_TOTAL_BY_CONST);
1001 : 2449 : }
1002 : : }
1003 [ + + ]: 12912 : if (k == Kind::INTS_DIVISION)
1004 : : {
1005 : 3808 : if (t[1].isConst() && !t[1].getConst<Rational>().isZero())
1006 : : {
1007 : : // can immediately replace by INTS_DIVISION_TOTAL
1008 : 846 : Node ret = nm->mkNode(Kind::INTS_DIVISION_TOTAL, t[0], t[1]);
1009 : 423 : return returnRewrite(t, ret, Rewrite::DIV_TOTAL_BY_CONST);
1010 : 423 : }
1011 : : }
1012 : 12489 : return RewriteResponse(REWRITE_DONE, t);
1013 : : }
1014 : :
1015 : 51740 : RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre)
1016 : : {
1017 [ + + ]: 51740 : if (pre)
1018 : : {
1019 : : // do not rewrite at prewrite.
1020 : 28504 : return RewriteResponse(REWRITE_DONE, t);
1021 : : }
1022 : 23236 : NodeManager* nm = nodeManager();
1023 : 23236 : Kind k = t.getKind();
1024 [ + + ][ + - ]: 23236 : Assert(k == Kind::INTS_MODULUS_TOTAL || k == Kind::INTS_DIVISION_TOTAL);
[ - + ][ - + ]
[ - - ]
1025 : 23236 : TNode n = t[0];
1026 : 23236 : TNode d = t[1];
1027 : 23236 : bool dIsConstant = d.isConst();
1028 [ + + ][ + + ]: 23236 : if (dIsConstant && d.getConst<Rational>().isZero())
[ + + ]
1029 : : {
1030 : : // (div_total x 0) ---> 0 or (mod_total x 0) ---> x
1031 : 333 : Node ret = k == Kind::INTS_MODULUS_TOTAL ? Node(t[0]) : nm->mkConstInt(0);
1032 : 206 : return returnRewrite(t, ret, Rewrite::DIV_MOD_BY_ZERO);
1033 : 206 : }
1034 [ + + ][ + + ]: 23030 : else if (dIsConstant && d.getConst<Rational>().isOne())
[ + + ]
1035 : : {
1036 [ + + ]: 583 : if (k == Kind::INTS_MODULUS_TOTAL)
1037 : : {
1038 : : // (mod_total x 1) --> 0
1039 : 98 : return returnRewrite(t, nm->mkConstInt(0), Rewrite::MOD_BY_ONE);
1040 : : }
1041 [ - + ][ - + ]: 485 : Assert(k == Kind::INTS_DIVISION_TOTAL);
[ - - ]
1042 : : // (div_total x 1) --> x
1043 : 485 : return returnRewrite(t, n, Rewrite::DIV_BY_ONE);
1044 : : }
1045 [ + + ][ + + ]: 22447 : else if (dIsConstant && d.getConst<Rational>().sgn() < 0)
[ + + ]
1046 : : {
1047 : : // pull negation
1048 : : // (div_total x (- c)) ---> (- (div_total x c))
1049 : : // (mod_total x (- c)) ---> (mod_total x c)
1050 : 428 : Node nn = nm->mkNode(k, t[0], nm->mkConstInt(-t[1].getConst<Rational>()));
1051 [ + + ][ + + ]: 214 : Node ret = k == Kind::INTS_DIVISION_TOTAL ? nm->mkNode(Kind::NEG, nn) : nn;
[ - - ]
1052 : 214 : return returnRewrite(t, ret, Rewrite::DIV_MOD_PULL_NEG_DEN);
1053 : 214 : }
1054 [ + + ][ + + ]: 22233 : else if (dIsConstant && n.isConst())
[ + + ]
1055 : : {
1056 [ - + ][ - + ]: 3598 : Assert(d.getConst<Rational>().isIntegral());
[ - - ]
1057 [ - + ][ - + ]: 3598 : Assert(n.getConst<Rational>().isIntegral());
[ - - ]
1058 [ - + ][ - + ]: 3598 : Assert(!d.getConst<Rational>().isZero());
[ - - ]
1059 : 3598 : Integer di = d.getConst<Rational>().getNumerator();
1060 : 3598 : Integer ni = n.getConst<Rational>().getNumerator();
1061 : :
1062 : 3598 : bool isDiv = (k == Kind::INTS_DIVISION_TOTAL);
1063 : :
1064 : : Integer result = isDiv ? ni.euclidianDivideQuotient(di)
1065 [ + + ]: 3598 : : ni.euclidianDivideRemainder(di);
1066 : :
1067 : : // constant evaluation
1068 : : // (mod_total c1 c2) ---> c3 or (div_total c1 c2) ---> c3
1069 : 3598 : Node resultNode = nm->mkConstInt(Rational(result));
1070 : 3598 : return returnRewrite(t, resultNode, Rewrite::CONST_EVAL);
1071 : 3598 : }
1072 [ + + ]: 18635 : if (k == Kind::INTS_MODULUS_TOTAL)
1073 : : {
1074 : : // Note these rewrites do not need to account for modulus by zero as being
1075 : : // a UF, which is handled by the reduction of INTS_MODULUS.
1076 : 10909 : Kind k0 = t[0].getKind();
1077 : 10909 : if (k0 == Kind::INTS_MODULUS_TOTAL && t[0][1] == t[1])
1078 : : {
1079 : : // (mod_total (mod_total x c) c) --> (mod x c)
1080 : 41 : return returnRewrite(t, t[0], Rewrite::MOD_OVER_MOD);
1081 : : }
1082 [ + + ][ + + ]: 10868 : else if (k0 == Kind::NONLINEAR_MULT || k0 == Kind::MULT || k0 == Kind::ADD)
[ + + ]
1083 : : {
1084 : : // can drop all
1085 : 4230 : std::vector<Node> newChildren;
1086 : 4230 : bool childChanged = false;
1087 [ + + ]: 14526 : for (const Node& tc : t[0])
1088 : : {
1089 : 10296 : if (tc.getKind() == Kind::INTS_MODULUS_TOTAL && tc[1] == t[1])
1090 : : {
1091 : 100 : newChildren.push_back(tc[0]);
1092 : 100 : childChanged = true;
1093 : 100 : continue;
1094 : : }
1095 : 10196 : newChildren.push_back(tc);
1096 [ + + ]: 14526 : }
1097 [ + + ]: 4230 : if (childChanged)
1098 : : {
1099 : : // (mod_total (op ... (mod_total x c) ...) c) --->
1100 : : // (mod_total (op ... x ...) c) where
1101 : : // op is one of { NONLINEAR_MULT, MULT, ADD }.
1102 : 100 : Node ret = nm->mkNode(k0, newChildren);
1103 : 100 : ret = nm->mkNode(Kind::INTS_MODULUS_TOTAL, ret, t[1]);
1104 : 100 : return returnRewrite(t, ret, Rewrite::MOD_CHILD_MOD);
1105 : 100 : }
1106 [ + + ]: 4230 : }
1107 : : }
1108 : : else
1109 : : {
1110 [ - + ][ - + ]: 7726 : Assert(k == Kind::INTS_DIVISION_TOTAL);
[ - - ]
1111 : : // Note these rewrites do not need to account for division by zero as being
1112 : : // a UF, which is handled by the reduction of INTS_DIVISION.
1113 : 7726 : if (t[0].getKind() == Kind::INTS_MODULUS_TOTAL && t[0][1] == t[1])
1114 : : {
1115 : : // (div_total (mod_total x c) c) --> 0
1116 : 0 : Node ret = nm->mkConstInt(0);
1117 : 0 : return returnRewrite(t, ret, Rewrite::DIV_OVER_MOD);
1118 : 0 : }
1119 : : }
1120 : 18494 : return RewriteResponse(REWRITE_DONE, t);
1121 : 23236 : }
1122 : :
1123 : 5228 : RewriteResponse ArithRewriter::rewriteExtIntegerOp(TNode t)
1124 : : {
1125 [ + + ][ + - ]: 5228 : Assert(t.getKind() == Kind::TO_INTEGER || t.getKind() == Kind::IS_INTEGER);
[ - + ][ - + ]
[ - - ]
1126 : 5228 : bool isPred = t.getKind() == Kind::IS_INTEGER;
1127 : 5228 : NodeManager* nm = nodeManager();
1128 [ + + ]: 5228 : if (t[0].isConst())
1129 : : {
1130 : 589 : Node ret;
1131 [ + + ]: 589 : if (isPred)
1132 : : {
1133 : 20 : ret = nm->mkConst(t[0].getConst<Rational>().isIntegral());
1134 : : }
1135 : : else
1136 : : {
1137 : 569 : ret = nm->mkConstInt(Rational(t[0].getConst<Rational>().floor()));
1138 : : }
1139 : 589 : return returnRewrite(t, ret, Rewrite::INT_EXT_CONST);
1140 : 589 : }
1141 [ + + ]: 4639 : if (t[0].getType().isInteger())
1142 : : {
1143 [ - + ][ + - ]: 216 : Node ret = isPred ? nm->mkConst(true) : Node(t[0]);
[ - - ]
1144 : 108 : return returnRewrite(t, ret, Rewrite::INT_EXT_INT);
1145 : 108 : }
1146 [ + + ]: 4531 : if (t[0].getKind() == Kind::TO_REAL)
1147 : : {
1148 : 228 : Node ret = nm->mkNode(t.getKind(), t[0][0]);
1149 : 114 : return returnRewrite(t, ret, Rewrite::INT_EXT_TO_REAL);
1150 : 114 : }
1151 [ + - ]: 4417 : if (d_expertEnabled)
1152 : : {
1153 [ + + ]: 4417 : if (t[0].getKind() == Kind::PI)
1154 : : {
1155 [ + + ][ + + ]: 14 : Node ret = isPred ? nm->mkConst(false) : nm->mkConstInt(Rational(3));
[ - - ]
1156 : 12 : return returnRewrite(t, ret, Rewrite::INT_EXT_PI);
1157 : 12 : }
1158 : : }
1159 : 4405 : return RewriteResponse(REWRITE_DONE, t);
1160 : : }
1161 : :
1162 : 1750 : RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
1163 : : {
1164 [ - + ][ - + ]: 1750 : Assert(t.getKind() == Kind::IAND);
[ - - ]
1165 : 1750 : uint32_t bsize = t.getOperator().getConst<IntAnd>().d_size;
1166 : 1750 : NodeManager* nm = nodeManager();
1167 : : // if constant, we eliminate
1168 : 1750 : if (t[0].isConst() && t[1].isConst())
1169 : : {
1170 : 550 : Node iToBvop = nm->mkConst(IntToBitVector(bsize));
1171 : 1100 : Node arg1 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[0]);
1172 : 1100 : Node arg2 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[1]);
1173 : 1100 : Node bvand = nm->mkNode(Kind::BITVECTOR_AND, arg1, arg2);
1174 : 550 : Node ret = nm->mkNode(Kind::BITVECTOR_UBV_TO_INT, bvand);
1175 : 550 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1176 : 550 : }
1177 [ + + ]: 1200 : else if (t[0] > t[1])
1178 : : {
1179 : : // ((_ iand k) x y) ---> ((_ iand k) y x) if x > y by node ordering
1180 : 218 : Node ret = nm->mkNode(Kind::IAND, t.getOperator(), t[1], t[0]);
1181 : 109 : return RewriteResponse(REWRITE_AGAIN, ret);
1182 : 109 : }
1183 [ + + ]: 1091 : else if (t[0] == t[1])
1184 : : {
1185 : : // ((_ iand k) x x) ---> (mod x 2^k)
1186 : 64 : Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
1187 : 64 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[0], twok);
1188 : 32 : return RewriteResponse(REWRITE_AGAIN, ret);
1189 : 32 : }
1190 : : // simplifications involving constants
1191 [ + + ]: 3150 : for (unsigned i = 0; i < 2; i++)
1192 : : {
1193 [ + + ]: 2117 : if (!t[i].isConst())
1194 : : {
1195 : 1882 : continue;
1196 : : }
1197 [ + + ]: 235 : if (t[i].getConst<Rational>().sgn() == 0)
1198 : : {
1199 : : // ((_ iand k) 0 y) ---> 0
1200 : 1 : return RewriteResponse(REWRITE_DONE, t[i]);
1201 : : }
1202 [ + + ]: 234 : if (t[i].getConst<Rational>().getNumerator() == Integer(2).pow(bsize) - 1)
1203 : : {
1204 : : // ((_ iand k) 111...1 y) ---> (mod y 2^k)
1205 : 50 : Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize)));
1206 : 50 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[1 - i], twok);
1207 : 25 : return RewriteResponse(REWRITE_AGAIN, ret);
1208 : 25 : }
1209 : : }
1210 : 1033 : return RewriteResponse(REWRITE_DONE, t);
1211 : : }
1212 : :
1213 : 775 : RewriteResponse ArithRewriter::postRewritePIAnd(TNode t)
1214 : : {
1215 [ - + ][ - + ]: 775 : Assert(t.getKind() == Kind::PIAND);
[ - - ]
1216 : 775 : NodeManager* nm = nodeManager();
1217 : : // simplifications involving constants
1218 [ + + ][ - - ]: 775 : if (t[0].isConst()
1219 [ + + ][ + + ]: 1570 : && (t[0].getConst<Rational>().sgn() == 0
[ + - ][ - - ]
1220 [ + + ][ + + ]: 795 : || t[0].getConst<Rational>().sgn() == -1))
[ + + ][ - - ]
1221 : : {
1222 : 80 : return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(0)));
1223 : : }
1224 [ + + ]: 2161 : for (unsigned i = 1; i < 3; i++)
1225 : : {
1226 [ + + ]: 1454 : if (!t[i].isConst())
1227 : : {
1228 : 1426 : continue;
1229 : : }
1230 [ + + ]: 108 : if (t[i].getConst<Rational>().sgn() == 0)
1231 : : {
1232 : : // (piand k 0 y) ---> 0
1233 : 44 : return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(0)));
1234 : : }
1235 [ + + ]: 86 : if (!t[0].isConst())
1236 : : {
1237 : 80 : continue;
1238 : : }
1239 : 6 : size_t bsize = t[0].getConst<Rational>().getNumerator().toUnsignedInt();
1240 : 6 : Node twok = nm->mkNode(Kind::POW2, t[0]);
1241 : 12 : Node maxsign = nm->mkConstInt(Rational(Integer(2).pow(bsize) - 1));
1242 : 12 : if (t[i].getConst<Rational>().getNumerator()
1243 [ + - ]: 18 : == maxsign.getConst<Rational>().getNumerator())
1244 : : {
1245 : : // (piand k 111...1 y) ---> (mod y 2^k)
1246 [ + - ]: 6 : if (i == 1)
1247 : : {
1248 : 12 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[2], twok);
1249 : 6 : return RewriteResponse(REWRITE_AGAIN, ret);
1250 : 6 : }
1251 [ - - ]: 0 : else if (i == 2)
1252 : : {
1253 : 0 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[1], twok);
1254 : 0 : return RewriteResponse(REWRITE_AGAIN, ret);
1255 : 0 : }
1256 : : }
1257 [ - + ][ - + ]: 12 : }
1258 : : // if constant, we eliminate
1259 : 707 : if (t[0].isConst() && t[1].isConst() && t[2].isConst())
1260 : : {
1261 : 0 : size_t bsize = t[0].getConst<Rational>().getNumerator().toUnsignedInt();
1262 : 0 : Node iToBvop = nm->mkConst(IntToBitVector(bsize));
1263 : 0 : Node arg1 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[1]);
1264 : 0 : Node arg2 = nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, t[2]);
1265 : 0 : Node bvand = nm->mkNode(Kind::BITVECTOR_AND, arg1, arg2);
1266 : 0 : Node ret = nm->mkNode(Kind::BITVECTOR_UBV_TO_INT, bvand);
1267 : 0 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1268 : 0 : }
1269 [ + + ]: 707 : else if (t[1] > t[2])
1270 : : {
1271 : : // (piand k x y) ---> (piand k y x) if x > y by node ordering
1272 : 184 : Node ret = nm->mkNode(Kind::PIAND, t[0], t[2], t[1]);
1273 : 92 : return RewriteResponse(REWRITE_AGAIN, ret);
1274 : 92 : }
1275 [ + + ]: 615 : else if (t[1] == t[2])
1276 : : {
1277 : : // (piand k x x) ---> (mod x 2^k)
1278 : 20 : Node twok = nm->mkNode(Kind::POW2, t[0]);
1279 : 40 : Node ret = nm->mkNode(Kind::INTS_MODULUS, t[1], twok);
1280 : 20 : return RewriteResponse(REWRITE_AGAIN, ret);
1281 : 20 : }
1282 : 595 : return RewriteResponse(REWRITE_DONE, t);
1283 : : }
1284 : :
1285 : 1982 : RewriteResponse ArithRewriter::postRewritePow2(TNode t)
1286 : : {
1287 [ - + ][ - + ]: 1982 : Assert(t.getKind() == Kind::POW2);
[ - - ]
1288 : : // if constant, we eliminate
1289 [ + + ]: 1982 : if (t[0].isConst())
1290 : : {
1291 : : // pow2 is only supported for integers
1292 [ + - ]: 1924 : Trace("arith-rewriter")
1293 : 962 : << "ArithRewriter::postRewritePow2, t:" << t << std::endl;
1294 [ - + ][ - + ]: 962 : Assert(t[0].getType().isInteger());
[ - - ]
1295 : : // use the evaluator definition for rewriting this
1296 : 962 : Evaluator eval(nullptr);
1297 : 1924 : Node ret = eval.eval(t, {}, {});
1298 [ + + ]: 962 : if (!ret.isNull())
1299 : : {
1300 : 946 : return RewriteResponse(REWRITE_DONE, ret);
1301 : : }
1302 [ + + ]: 962 : }
1303 : 1036 : return RewriteResponse(REWRITE_DONE, t);
1304 : : }
1305 : :
1306 : 136 : RewriteResponse ArithRewriter::postRewriteIntsIsPow2(TNode t)
1307 : : {
1308 [ - + ][ - + ]: 136 : Assert(t.getKind() == Kind::INTS_ISPOW2);
[ - - ]
1309 : : // if constant, we eliminate
1310 [ + - ]: 136 : if (t[0].isConst())
1311 : : {
1312 : : // pow2 is only supported for integers
1313 [ - + ][ - + ]: 136 : Assert(t[0].getType().isInteger());
[ - - ]
1314 : 136 : Integer i = t[0].getConst<Rational>().getNumerator();
1315 : :
1316 : 272 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, i.isPow2()));
1317 : 136 : }
1318 : 0 : return RewriteResponse(REWRITE_DONE, t);
1319 : : }
1320 : 209 : RewriteResponse ArithRewriter::postRewriteIntsLog2(TNode t)
1321 : : {
1322 [ - + ][ - + ]: 209 : Assert(t.getKind() == Kind::INTS_LOG2);
[ - - ]
1323 : : // if constant, we eliminate
1324 [ + + ]: 209 : if (t[0].isConst())
1325 : : {
1326 : : // log2 is only supported for integers
1327 [ - + ][ - + ]: 153 : Assert(t[0].getType().isInteger());
[ - - ]
1328 : 153 : const Rational& r = t[0].getConst<Rational>();
1329 : : // default to 0 for negative inputs
1330 [ + + ]: 153 : if (r.sgn() < 0)
1331 : : {
1332 : 2 : return RewriteResponse(REWRITE_DONE, rewriter::mkConst(d_nm, Integer(0)));
1333 : : }
1334 : : // for non-negative inputs, this
1335 : : // is captured by `length()` of `Integer`.
1336 : 152 : Integer i = r.getNumerator();
1337 : 152 : size_t const length = i.length();
1338 : : return RewriteResponse(REWRITE_DONE,
1339 : 304 : rewriter::mkConst(d_nm, Integer(length - 1)));
1340 : 152 : }
1341 : 56 : return RewriteResponse(REWRITE_DONE, t);
1342 : : }
1343 : :
1344 : 7960 : RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t)
1345 : : {
1346 [ + - ]: 15920 : Trace("arith-tf-rewrite")
1347 : 7960 : << "Rewrite transcendental function : " << t << std::endl;
1348 [ - + ][ - + ]: 7960 : Assert(t.getTypeOrNull(true).isReal());
[ - - ]
1349 : 7960 : NodeManager* nm = nodeManager();
1350 [ + + ][ + + ]: 7960 : switch (t.getKind())
[ + + ][ + + ]
1351 : : {
1352 : 1404 : case Kind::EXPONENTIAL:
1353 : : {
1354 [ + + ]: 1404 : if (t[0].isConst())
1355 : : {
1356 : 772 : Rational r = t[0].getConst<Rational>();
1357 [ + + ]: 772 : if (r.sgn() == 0)
1358 : : {
1359 : 54 : Node one = nm->mkConstReal(Rational(1));
1360 : : // (= (exp 0.0) 1.0)
1361 : 54 : return RewriteResponse(REWRITE_DONE, one);
1362 : 54 : }
1363 : : else
1364 : : {
1365 : 718 : return RewriteResponse(REWRITE_DONE, t);
1366 : : }
1367 : 772 : }
1368 [ + + ]: 632 : else if (t[0].getKind() == Kind::ADD)
1369 : : {
1370 : 65 : std::vector<Node> product;
1371 [ + + ]: 195 : for (const Node tc : t[0])
1372 : : {
1373 : 130 : Node tcr = rewriter::ensureReal(tc);
1374 : 130 : product.push_back(nm->mkNode(Kind::EXPONENTIAL, tcr));
1375 : 195 : }
1376 : : // We need to do a full rewrite here, since we can get exponentials of
1377 : : // constants, e.g. when we are rewriting exp(2 + x)
1378 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1379 : 130 : nm->mkNode(Kind::MULT, product));
1380 : 65 : }
1381 : : }
1382 : 567 : break;
1383 : 5764 : case Kind::SINE:
1384 [ + + ]: 5764 : if (t[0].isConst())
1385 : : {
1386 : 2177 : const Rational& rat = t[0].getConst<Rational>();
1387 [ + + ]: 2177 : if (rat.sgn() == 0)
1388 : : {
1389 : 110 : return RewriteResponse(REWRITE_DONE, nm->mkConstReal(Rational(0)));
1390 : : }
1391 [ + + ]: 2122 : else if (rat.sgn() == -1)
1392 : : {
1393 : : Node ret = nm->mkNode(Kind::NEG,
1394 : 330 : nm->mkNode(Kind::SINE, nm->mkConstReal(-rat)));
1395 : 165 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1396 : 165 : }
1397 : : }
1398 [ + + ][ - - ]: 3587 : else if ((t[0].getKind() == Kind::MULT
1399 [ - + ][ + - ]: 7078 : || t[0].getKind() == Kind::NONLINEAR_MULT)
[ - - ]
1400 : 7078 : && t[0][0].isConst() && t[0][0].getConst<Rational>().sgn() == -1)
1401 : : {
1402 : : // sin(-n*x) ---> -sin(n*x)
1403 : 30 : std::vector<Node> mchildren(t[0].begin(), t[0].end());
1404 : 15 : mchildren[0] = nm->mkConstReal(-t[0][0].getConst<Rational>());
1405 : : Node ret = nm->mkNode(
1406 : : Kind::NEG,
1407 : 30 : nm->mkNode(Kind::SINE, nm->mkNode(t[0].getKind(), mchildren)));
1408 : 15 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1409 : 15 : }
1410 : : else
1411 : : {
1412 : : // get the factor of PI in the argument
1413 : 3572 : Node pi_factor;
1414 : 3572 : Node pi;
1415 : 3572 : Node rem;
1416 : 3572 : std::map<Node, Node> msum;
1417 [ + - ]: 3572 : if (ArithMSum::getMonomialSum(t[0], msum))
1418 : : {
1419 : 3572 : pi = mkPi(nm);
1420 : 3572 : std::map<Node, Node>::iterator itm = msum.find(pi);
1421 [ + + ]: 3572 : if (itm != msum.end())
1422 : : {
1423 [ + + ]: 2116 : if (itm->second.isNull())
1424 : : {
1425 : 12 : pi_factor = rewriter::mkConst(d_nm, Integer(1));
1426 : : }
1427 : : else
1428 : : {
1429 : 2104 : pi_factor = itm->second;
1430 : : }
1431 : 2116 : msum.erase(pi);
1432 [ + + ]: 2116 : if (!msum.empty())
1433 : : {
1434 : 2033 : rem = ArithMSum::mkNode(nm, msum);
1435 : : }
1436 : : }
1437 : : }
1438 : : else
1439 : : {
1440 : 0 : DebugUnhandled();
1441 : : }
1442 : :
1443 : : // if there is a factor of PI
1444 [ + + ]: 3572 : if (!pi_factor.isNull())
1445 : : {
1446 [ + - ]: 4232 : Trace("arith-tf-rewrite-debug")
1447 : 2116 : << "Process pi factor = " << pi_factor << std::endl;
1448 : 2116 : Rational r = pi_factor.getConst<Rational>();
1449 : 2116 : Rational r_abs = r.abs();
1450 : 2116 : Rational rone = Rational(1);
1451 : 2116 : Rational rtwo = Rational(2);
1452 [ + + ]: 2116 : if (r_abs > rone)
1453 : : {
1454 : : // add/substract 2*pi beyond scope
1455 : 1 : Rational ra_div_two = (r_abs + rone) / rtwo;
1456 : 1 : Node new_pi_factor;
1457 [ + - ]: 1 : if (r.sgn() == 1)
1458 : : {
1459 : 1 : new_pi_factor = nm->mkConstReal(r - rtwo * ra_div_two.floor());
1460 : : }
1461 : : else
1462 : : {
1463 : 0 : Assert(r.sgn() == -1);
1464 : 0 : new_pi_factor = nm->mkConstReal(r + rtwo * ra_div_two.floor());
1465 : : }
1466 : 2 : Node new_arg = nm->mkNode(Kind::MULT, new_pi_factor, pi);
1467 [ + - ]: 1 : if (!rem.isNull())
1468 : : {
1469 : 1 : new_arg = nm->mkNode(Kind::ADD, new_arg, rem);
1470 : : }
1471 : 1 : new_arg = rewriter::ensureReal(new_arg);
1472 : : // sin( 2*n*PI + x ) = sin( x )
1473 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1474 : 2 : nm->mkNode(Kind::SINE, new_arg));
1475 : 1 : }
1476 [ + + ]: 2115 : else if (r_abs == rone)
1477 : : {
1478 : : // sin( PI + x ) = -sin( x )
1479 [ + + ]: 12 : if (rem.isNull())
1480 : : {
1481 : : return RewriteResponse(REWRITE_DONE,
1482 : 4 : nm->mkConstReal(Rational(0)));
1483 : : }
1484 : : else
1485 : : {
1486 : 10 : rem = rewriter::ensureReal(rem);
1487 : : return RewriteResponse(
1488 : : REWRITE_AGAIN_FULL,
1489 : 20 : nm->mkNode(Kind::NEG, nm->mkNode(Kind::SINE, rem)));
1490 : : }
1491 : : }
1492 [ + + ]: 2103 : else if (rem.isNull())
1493 : : {
1494 : : // other rational cases based on Niven's theorem
1495 : : // (https://en.wikipedia.org/wiki/Niven%27s_theorem)
1496 : 81 : Integer one = Integer(1);
1497 : 81 : Integer two = Integer(2);
1498 : 81 : Integer six = Integer(6);
1499 [ + - ]: 81 : if (r_abs.getDenominator() == two)
1500 : : {
1501 [ - + ][ - + ]: 81 : Assert(r_abs.getNumerator() == one);
[ - - ]
1502 : : return RewriteResponse(REWRITE_DONE,
1503 : 162 : nm->mkConstReal(Rational(r.sgn())));
1504 : : }
1505 [ - - ]: 0 : else if (r_abs.getDenominator() == six)
1506 : : {
1507 : 0 : Integer five = Integer(5);
1508 : 0 : if (r_abs.getNumerator() == one || r_abs.getNumerator() == five)
1509 : : {
1510 : : return RewriteResponse(
1511 : : REWRITE_DONE,
1512 : 0 : nm->mkConstReal(Rational(r.sgn()) / Rational(2)));
1513 : : }
1514 [ - - ]: 0 : }
1515 [ - + ][ - + ]: 243 : }
[ - + ]
1516 [ + + ][ + + ]: 2398 : }
[ + + ][ + + ]
1517 [ + + ][ + + ]: 3854 : }
[ + + ][ + + ]
1518 : 5435 : break;
1519 : 268 : case Kind::COSINE:
1520 : : {
1521 : : return RewriteResponse(
1522 : : REWRITE_AGAIN_FULL,
1523 : 536 : nm->mkNode(
1524 : : Kind::SINE,
1525 : 1072 : nm->mkNode(Kind::SUB,
1526 [ + + ][ - - ]: 1340 : nm->mkNode(Kind::MULT,
1527 : 536 : {nm->mkConstReal(Rational(1) / Rational(2)),
1528 : 536 : mkPi(nm)}),
1529 : 268 : t[0])));
1530 : : }
1531 : : break;
1532 : 57 : case Kind::TANGENT:
1533 : : {
1534 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1535 [ + + ][ - - ]: 285 : nm->mkNode(Kind::DIVISION,
1536 : 114 : {nm->mkNode(Kind::SINE, t[0]),
1537 : 171 : nm->mkNode(Kind::COSINE, t[0])}));
1538 : : }
1539 : : break;
1540 : 20 : case Kind::COSECANT:
1541 : : {
1542 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1543 [ + + ][ - - ]: 100 : nm->mkNode(Kind::DIVISION,
1544 : 40 : {nm->mkConstReal(Rational(1)),
1545 : 60 : nm->mkNode(Kind::SINE, t[0])}));
1546 : : }
1547 : : break;
1548 : 43 : case Kind::SECANT:
1549 : : {
1550 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1551 [ + + ][ - - ]: 215 : nm->mkNode(Kind::DIVISION,
1552 : 86 : {nm->mkConstReal(Rational(1)),
1553 : 129 : nm->mkNode(Kind::COSINE, t[0])}));
1554 : : }
1555 : : break;
1556 : 22 : case Kind::COTANGENT:
1557 : : {
1558 : : return RewriteResponse(REWRITE_AGAIN_FULL,
1559 [ + + ][ - - ]: 110 : nm->mkNode(Kind::DIVISION,
1560 : 44 : {nm->mkNode(Kind::COSINE, t[0]),
1561 : 66 : nm->mkNode(Kind::SINE, t[0])}));
1562 : : }
1563 : : break;
1564 : 382 : default: break;
1565 : : }
1566 : 6384 : return RewriteResponse(REWRITE_DONE, t);
1567 : : }
1568 : :
1569 : 46900 : Node ArithRewriter::expandDefinition(Node node)
1570 : : {
1571 : : // call eliminate operators, to eliminate partial operators only
1572 : 46900 : std::vector<SkolemLemma> lems;
1573 : 46900 : TrustNode ret = d_opElim.eliminate(node, lems, true);
1574 [ - + ][ - + ]: 46900 : Assert(lems.empty());
[ - - ]
1575 [ + + ]: 46900 : if (ret.isNull())
1576 : : {
1577 : 46696 : return Node::null();
1578 : : }
1579 : 204 : return ret.getNode();
1580 : 46900 : }
1581 : :
1582 : 8437 : RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r)
1583 : : {
1584 [ + - ]: 16874 : Trace("arith-rewriter") << "ArithRewriter : " << t << " == " << ret << " by "
1585 : 8437 : << r << std::endl;
1586 : 8437 : return RewriteResponse(REWRITE_AGAIN_FULL, ret);
1587 : : }
1588 : :
1589 : 225598 : Node ArithRewriter::rewriteIneqToBv(const Node& ineq)
1590 : : {
1591 [ - + ][ - + ]: 225598 : Assert(ineq.getKind() == Kind::GEQ);
[ - - ]
1592 : :
1593 : 451196 : Node left = rewriter::removeToReal(ineq[0]);
1594 : 451196 : Node right = rewriter::removeToReal(ineq[1]);
1595 : :
1596 : 225598 : rewriter::Sum sum;
1597 : 225598 : rewriter::addToSum(sum, left, false);
1598 : 225598 : rewriter::addToSum(sum, right, true);
1599 : :
1600 : 451196 : return rewriteIneqToBv(Kind::GEQ, sum, ineq);
1601 : 225598 : }
1602 : :
1603 : 225598 : Node ArithRewriter::rewriteIneqToBv(Kind kind,
1604 : : const rewriter::Sum& sum,
1605 : : const Node& ineq)
1606 : : {
1607 : 225598 : bool convertible = true;
1608 : : // the (single) bv2nat term in the sum
1609 : 225598 : Node bv2natTerm;
1610 : : // whether the bv2nat term is positive in the sum
1611 : 225598 : bool bv2natPol = false;
1612 : : // the remaining sum (constant)
1613 : 225598 : std::vector<Node> otherSum;
1614 : 225598 : NodeManager* nm = nodeManager();
1615 [ + + ]: 366215 : for (const std::pair<const Node, RealAlgebraicNumber>& m : sum)
1616 : : {
1617 [ + - ]: 366174 : if (m.second.isRational())
1618 : : {
1619 : 366174 : const Rational& r = m.second.toRational();
1620 : 366174 : Kind mk = m.first.getKind();
1621 [ + + ]: 366174 : if (mk == Kind::BITVECTOR_UBV_TO_INT)
1622 : : {
1623 : : // We currently only eliminate sums involving exactly one
1624 : : // (bv2nat x) monomial whose coefficient is +- 1, although more
1625 : : // cases could be handled here.
1626 [ + + ]: 47 : if (bv2natTerm.isNull())
1627 : : {
1628 [ + + ]: 45 : if (r.abs().isOne())
1629 : : {
1630 : 43 : bv2natPol = (r.sgn() == 1);
1631 : 43 : bv2natTerm = m.first;
1632 : 43 : continue;
1633 : : }
1634 : : }
1635 : : else
1636 : : {
1637 : 2 : convertible = false;
1638 : 2 : break;
1639 : : }
1640 : : }
1641 [ + + ][ + - ]: 366127 : else if (mk == Kind::CONST_INTEGER && m.second.isRational())
[ + + ]
1642 : : {
1643 [ + + ]: 150056 : if (r.isIntegral())
1644 : : {
1645 : 140574 : otherSum.push_back(nm->mkConstInt(r));
1646 : 140574 : continue;
1647 : : }
1648 : : }
1649 : : // if a non-constant, non-bv2nat term is in the sum, we fail
1650 [ + + ][ + ]: 366174 : }
1651 : 225555 : convertible = false;
1652 : 225555 : break;
1653 : : }
1654 [ + + ][ + - ]: 225598 : if (convertible && !bv2natTerm.isNull())
[ + + ]
1655 : : {
1656 : 41 : Node zero = nm->mkConstInt(Rational(0));
1657 : 41 : Kind bvKind =
1658 : : (kind == Kind::GT
1659 [ - + ][ - - ]: 82 : ? (bv2natPol ? Kind::BITVECTOR_UGT : Kind::BITVECTOR_ULT)
1660 [ + - ]: 41 : : (bv2natPol ? Kind::BITVECTOR_UGE : Kind::BITVECTOR_ULE));
1661 : 41 : Node bvt = bv2natTerm[0];
1662 : 41 : size_t bvsize = bvt.getType().getBitVectorSize();
1663 : 82 : Node w = nm->mkConstInt(Rational(Integer(2).pow(bvsize)));
1664 : 41 : Node osum = otherSum.empty()
1665 : : ? zero
1666 : 40 : : (otherSum.size() == 1 ? otherSum[0]
1667 [ + + ][ + - ]: 81 : : nm->mkNode(Kind::ADD, otherSum));
1668 : : // possibly negate the sum
1669 : : Node o = bv2natPol
1670 : 41 : ? (osum.getKind() == Kind::NEG ? osum[0]
1671 : : : nm->mkNode(Kind::NEG, osum))
1672 [ + - ][ - + ]: 82 : : osum;
[ + - ][ - - ]
1673 : 82 : Node ub = nm->mkNode(Kind::GEQ, o, w);
1674 : 82 : Node lb = nm->mkNode(Kind::LT, o, zero);
1675 : 41 : Node iToBvop = nm->mkConst(IntToBitVector(bvsize));
1676 : 164 : Node ret = nm->mkNode(
1677 : : Kind::ITE,
1678 : : {ub,
1679 : 41 : nm->mkConst(!bv2natPol),
1680 : 328 : nm->mkNode(
1681 : : Kind::ITE,
1682 : : {lb,
1683 : 82 : nm->mkConst(bv2natPol),
1684 : 82 : nm->mkNode(bvKind,
1685 : : bvt,
1686 : 246 : nm->mkNode(Kind::INT_TO_BITVECTOR, iToBvop, o))})});
1687 : : // E.g. (<= (bv2nat x) N) -->
1688 : : // (ite (>= N 2^w) true (ite (< N 0) false (bvule x ((_ int2bv w) N))
1689 : : // or (<= N (bv2nat x)) -->
1690 : : // (ite (>= N 2^w) false (ite (< N 0) true (bvuge x ((_ int2bv w) N))
1691 : : // where N is a constant. Note that ((_ int2bv w) N) will subsequently
1692 : : // be rewritten to the appropriate bitvector constant.
1693 : 41 : return ret;
1694 : 41 : }
1695 : 225557 : return ineq;
1696 : 225598 : }
1697 : :
1698 : 250 : Node ArithRewriter::expandPowConst(NodeManager* nm, const Node& t)
1699 : : {
1700 [ + + ]: 250 : if (t[1].isConst())
1701 : : {
1702 : 242 : const Rational& exp = t[1].getConst<Rational>();
1703 [ - + ]: 242 : if (!exp.isIntegral())
1704 : : {
1705 : 238 : return Node::null();
1706 : : }
1707 : 242 : TNode base = t[0];
1708 [ + + ]: 242 : if (exp.sgn() == 0)
1709 : : {
1710 : 50 : return nm->mkConstRealOrInt(t.getType(), Rational(1));
1711 : : }
1712 [ + + ]: 217 : else if (exp.sgn() > 0)
1713 : : {
1714 : 215 : Rational r(expr::NodeValue::MAX_CHILDREN);
1715 [ + + ]: 215 : if (exp <= r)
1716 : : {
1717 : 213 : unsigned num = exp.getNumerator().toUnsignedInt();
1718 : 213 : Node ret;
1719 [ + + ]: 213 : if (num == 1)
1720 : : {
1721 : 35 : ret = base;
1722 : : }
1723 : : else
1724 : : {
1725 : 178 : NodeBuilder nb(nm, Kind::MULT);
1726 [ + + ]: 939 : for (unsigned i = 0; i < num; ++i)
1727 : : {
1728 : 761 : nb << base;
1729 : : }
1730 [ - + ][ - + ]: 178 : Assert(nb.getNumChildren() > 0);
[ - - ]
1731 : 178 : ret = nb;
1732 : 178 : }
1733 : 213 : return ret;
1734 : 213 : }
1735 [ + + ]: 215 : }
1736 [ + + ]: 242 : }
1737 : 12 : return Node::null();
1738 : : }
1739 : :
1740 : : } // namespace arith
1741 : : } // namespace theory
1742 : : } // namespace cvc5::internal
|
