diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-13 18:22:28 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-13 16:22:28 -0700 |
commit | 1f09fa5f3de7c23ea4713984fce658d13e8e3e36 (patch) | |
tree | 287539b7e6272689b246816ed6df2aa53ed6f5a4 /src | |
parent | ef7e56f4217ece19b1caf743e5b1db0d3f549226 (diff) |
Eliminate negative constant coefficients in div/mod (#2929)
Fixes #1399.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 267fcc383..6dd6ffd56 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -734,13 +734,16 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){ Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); return RewriteResponse(REWRITE_AGAIN, n); } - }else if(dIsConstant && d.getConst<Rational>().isNegativeOne()){ - if(k == kind::INTS_MODULUS || k == kind::INTS_MODULUS_TOTAL){ - return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); - }else{ - Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL); - return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::UMINUS, n)); - } + } + else if (dIsConstant && d.getConst<Rational>().sgn() < 0) + { + // pull negation + // (div x (- c)) ---> (- (div x c)) + // (mod x (- c)) ---> (mod x c) + NodeManager* nm = NodeManager::currentNM(); + Node nn = nm->mkNode(k, t[0], nm->mkConst(-t[1].getConst<Rational>())); + Node ret = k == kind::INTS_DIVISION ? nm->mkNode(kind::UMINUS, nn) : nn; + return RewriteResponse(REWRITE_AGAIN, nn); }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){ Assert(d.getConst<Rational>().isIntegral()); Assert(n.getConst<Rational>().isIntegral()); |