Fix integer mod/rem simplification (#115)

Author: Saloed

ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/ArithSimplification.kt

@@ -15,7 +15,6 @@ import io.ksmt.sort.KRealSort
 import io.ksmt.utils.ArithUtils.RealValue
 import io.ksmt.utils.ArithUtils.bigIntegerValue
 import io.ksmt.utils.ArithUtils.compareTo
-import io.ksmt.utils.ArithUtils.modWithNegativeNumbers
 import io.ksmt.utils.ArithUtils.numericValue
 import io.ksmt.utils.ArithUtils.toRealValue
 import io.ksmt.utils.uncheckedCast
@@ -231,12 +230,21 @@ fun KContext.simplifyIntMod(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<K
         }
 
         if (rValue != BigInteger.ZERO && lhs is KIntNumExpr) {
-            return mkIntNum(modWithNegativeNumbers(lhs.bigIntegerValue, rValue))
+            return mkIntNum(evalIntMod(lhs.bigIntegerValue, rValue))
         }
     }
     return mkIntModNoSimplify(lhs, rhs)
 }
 
+/**
+ * Eval integer mod wrt Int theory rules.
+ * */
+private fun evalIntMod(a: BigInteger, b: BigInteger): BigInteger {
+    val remainder = a.rem(b)
+    if (remainder >= BigInteger.ZERO) return remainder
+    return if (b >= BigInteger.ZERO) remainder + b else remainder - b
+}
+
 fun KContext.simplifyIntRem(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KIntSort> {
     if (rhs is KIntNumExpr) {
         val rValue = rhs.bigIntegerValue
@@ -246,12 +254,20 @@ fun KContext.simplifyIntRem(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<K
         }
 
         if (rValue != BigInteger.ZERO && lhs is KIntNumExpr) {
-            return mkIntNum(lhs.bigIntegerValue.rem(rValue))
+            return mkIntNum(evalIntRem(lhs.bigIntegerValue, rValue))
         }
     }
     return mkIntRemNoSimplify(lhs, rhs)
 }
 
+/**
+ * Eval integer rem wrt Int theory rules.
+ * */
+private fun evalIntRem(a: BigInteger, b: BigInteger): BigInteger {
+    val mod = evalIntMod(a, b)
+    return if (b >= BigInteger.ZERO) mod else -mod
+}
+
 fun KContext.simplifyIntToReal(arg: KExpr<KIntSort>): KExpr<KRealSort> {
     if (arg is KIntNumExpr) {
         return mkRealNum(arg)

ksmt-core/src/main/kotlin/io/ksmt/utils/ArithUtils.kt

@@ -44,24 +44,6 @@ object ArithUtils {
             else -> decl.value.toBigInteger()
         }
 
-    /**
-     * BigInteger doesn't support mod operation with negative modulus.
-     * We use the mod operation with absolute values and then manually
-     * recover the result depending on the arguments signs.
-     * */
-    fun modWithNegativeNumbers(a: BigInteger, b: BigInteger): BigInteger {
-        val aAbs = a.abs()
-        val bAbs = b.abs()
-        val u = aAbs.mod(bAbs)
-        return when {
-            u == BigInteger.ZERO -> BigInteger.ZERO
-            a >= BigInteger.ZERO && b >= BigInteger.ZERO -> u
-            a < BigInteger.ZERO && b >= BigInteger.ZERO -> -u + b
-            a >= BigInteger.ZERO && b < BigInteger.ZERO -> u + b
-            else -> -u
-        }
-    }
-
     class RealValue private constructor(
         numerator: BigInteger,
         denominator: BigInteger

ksmt-core/src/test/kotlin/io/ksmt/ArithSimplifyTest.kt

@@ -80,14 +80,22 @@ class ArithSimplifyTest : ExpressionSimplifyTest() {
     @Test
     fun testIntMod() {
         testOperation(isInt = true, KContext::mkIntMod, KContext::mkIntModNoSimplify) {
-            listOf(mkIntNum(0), mkIntNum(1), mkIntNum(-1)).uncheckedCast()
+            listOf(
+                mkIntNum(0), mkIntNum(1), mkIntNum(-1),
+                // Values with non-trivial remainder
+                mkIntNum(47), mkIntNum(-47), mkIntNum(13), mkIntNum(-13),
+            ).uncheckedCast()
         }
     }
 
     @Test
     fun testIntRem() {
         testOperation(isInt = true, KContext::mkIntRem, KContext::mkIntRemNoSimplify) {
-            listOf(mkIntNum(0), mkIntNum(1), mkIntNum(-1)).uncheckedCast()
+            listOf(
+                mkIntNum(0), mkIntNum(1), mkIntNum(-1),
+                // Values with non-trivial remainder
+                mkIntNum(47), mkIntNum(-47), mkIntNum(13), mkIntNum(-13),
+            ).uncheckedCast()
         }
     }