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 | |
| parent | ef7e56f4217ece19b1caf743e5b1db0d3f549226 (diff) | |
Eliminate negative constant coefficients in div/mod (#2929)
Fixes #1399.
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 17 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/issue1399.smt2 | 12 |
3 files changed, 23 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()); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8d69a1a69..1ed879400 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -25,6 +25,7 @@ set(regress_0_tests regress0/arith/integers/ackermann6.smt2 regress0/arith/integers/arith-int-042.cvc regress0/arith/integers/arith-int-042.min.cvc + regress0/arith/issue1399.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc regress0/arith/miplib2.cvc diff --git a/test/regress/regress0/arith/issue1399.smt2 b/test/regress/regress0/arith/issue1399.smt2 new file mode 100644 index 000000000..80305260e --- /dev/null +++ b/test/regress/regress0/arith/issue1399.smt2 @@ -0,0 +1,12 @@ +(set-logic LIA) +(set-info :status sat) + +(define-fun findIdx ((y1 Int)(y2 Int)(k1 Int)) Int (div (* (- 7) (mod y1 (- 5))) 2)) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun k () Int) + +(assert (not (and (=> (< x1 x2) (=> (< k x1) (= (findIdx x1 x2 k) 0))) + (=> (< x1 x2) (=> (> k x2) (= (findIdx x1 x2 k) 2))) + (=> (< x1 x2) (=> (and (> k x1) (< k x2)) (= (findIdx x1 x2 k) 1)))))) +(check-sat) |