Fix int division (UnitTestBot#119)

* cvc: fix int division * core: fix int division rounding
dee-tree · Jun 23, 2023 · 856cbfe · 856cbfe
1 parent fe68394
commit 856cbfe
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 3 deletions.
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/ArithSimplificationRules.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/ArithSimplificationRules.kt
@@ -174,7 +174,7 @@ inline fun <T : KArithSort> KContext.simplifyArithDivLight(
         }
 
         if (lhs is KIntNumExpr) {
-            return mkIntNum(lhs.bigIntegerValue / rValue.numerator).uncheckedCast()
+            return mkIntNum(evalIntDiv(lhs.bigIntegerValue, rValue.numerator)).uncheckedCast()
         }
 
         if (lhs is KRealNumExpr) {
@@ -407,6 +407,26 @@ fun <T : KArithSort> KExpr<T>.toRealValue(): RealValue? = when (this) {
     else -> null
 }
 
+/**
+ * Eval integer div wrt Int theory rules.
+ * */
+fun evalIntDiv(a: BigInteger, b: BigInteger): BigInteger {
+    if (a >= BigInteger.ZERO) {
+        return a / b
+    }
+    val (divisionRes, rem) = a.divideAndRemainder(b)
+    if (rem == BigInteger.ZERO) {
+        return divisionRes
+    }
+
+    // round toward zero
+    return if (b >= BigInteger.ZERO) {
+        divisionRes - BigInteger.ONE
+    } else {
+        divisionRes + BigInteger.ONE
+    }
+}
+
 /**
  * Eval integer mod wrt Int theory rules.
  * */

diff --git a/ksmt-core/src/test/kotlin/io/ksmt/ArithSimplifyTest.kt b/ksmt-core/src/test/kotlin/io/ksmt/ArithSimplifyTest.kt
@@ -58,7 +58,11 @@ class ArithSimplifyTest : ExpressionSimplifyTest() {
     @Test
     fun testDiv() {
         testOperation(isInt = true, KContext::mkArithDiv, KContext::mkArithDivNoSimplify) {
-            listOf(mkIntNum(0), mkIntNum(1), mkIntNum(-1)).uncheckedCast()
+            listOf(
+                mkIntNum(0), mkIntNum(1), mkIntNum(-1),
+                // Values with non-trivial rounding
+                mkIntNum(47), mkIntNum(-47), mkIntNum(13), mkIntNum(-13)
+            ).uncheckedCast()
         }
 
         testOperation(isInt = false, KContext::mkArithDiv, KContext::mkArithDivNoSimplify) {

diff --git a/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt b/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt
@@ -1025,7 +1025,17 @@ class KCvc5ExprInternalizer(
     }
 
     override fun <T : KArithSort> transform(expr: KDivArithExpr<T>) = with(expr) {
-        transform(lhs, rhs) { lhs: Term, rhs: Term -> nsolver.mkTerm(Kind.DIVISION, lhs, rhs) }
+        transform(lhs, rhs) { lhs: Term, rhs: Term ->
+            arithDivide(sort, lhs, rhs)
+        }
+    }
+
+    private fun arithDivide(sort: KArithSort, lhs: Term, rhs: Term): Term = with(sort.ctx) {
+        when (sort) {
+            realSort -> nsolver.mkTerm(Kind.DIVISION, lhs, rhs)
+            intSort -> nsolver.mkTerm(Kind.INTS_DIVISION, lhs, rhs)
+            else -> throw KSolverUnsupportedFeatureException("Arith sort $sort is unsupported")
+        }
     }
 
     override fun <T : KArithSort> transform(expr: KPowerArithExpr<T>) = with(expr) {