Eliminate negative constant coefficients in div/mod (#2929)

Fixes #1399.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 267fcc3834eea8dadc9fc2d1ea3a8a2037300c3c..6dd6ffd56cf77c772f6f9a74a543249495988b65 100644 (file)
--- 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 8d69a1a69477715935bd2a9e6cb3279756c3957d..1ed879400b463f5227098d0d2ff15743d16a1fbf 100644 (file)
--- 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 (file)
index 0000000..8030526
--- /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)