From 1f09fa5f3de7c23ea4713984fce658d13e8e3e36 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 13 Oct 2019 18:22:28 -0500
Subject: [PATCH] Eliminate negative constant coefficients in div/mod (#2929)

Fixes #1399.
---
 src/theory/arith/arith_rewriter.cpp        | 17 ++++++++++-------
 test/regress/CMakeLists.txt                |  1 +
 test/regress/regress0/arith/issue1399.smt2 | 12 ++++++++++++
 3 files changed, 23 insertions(+), 7 deletions(-)
 create mode 100644 test/regress/regress0/arith/issue1399.smt2

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)
-- 
2.30.2