bit-vector QE when all bound terms have the same linear coefficient

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

@@ -7,18 +7,19 @@ import io.ksmt.expr.transformer.KNonRecursiveTransformer
 import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KBvSort
 import io.ksmt.sort.KSort
+import io.ksmt.utils.uncheckedCast
 
 @Suppress("UNCHECKED_CAST")
 class KBvQETransformer(ctx: KContext, bound: KDecl<KBvSort>) : KNonRecursiveTransformer(ctx) {
     private var bounds = mutableListOf<KDecl<*>>()
     private var newBody: KExpr<KBoolSort> = ctx.mkTrue()
 
-//    // bool transformers
-//    override fun transform(expr: KAndExpr): KExpr<KBoolSort> {
-//    }
-//
-//    override fun transform(expr: KAndBinaryExpr): KExpr<KBoolSort> {
-//    }
+    override fun <T : KBvSort> transform(expr: KBvMulExpr<T>):
+            KExpr<T>  = with(ctx) {
+        return mkBvMulNoOverflowExpr(expr.arg0, expr.arg1, isSigned = false).uncheckedCast()
+    }
+
+
 
     override fun <T : KSort> transform(expr: KEqExpr<T>):
             KExpr<KBoolSort> = with(ctx) {
@@ -34,14 +35,6 @@ class KBvQETransformer(ctx: KContext, bound: KDecl<KBvSort>) : KNonRecursiveTran
         { l, r -> eqToAndNoSimplify(l, r) }
     }
 
-//    override fun transform(expr: KNotExpr): KExpr<KBoolSort> {
-//    }
-
-//    // bit-vec expressions transformers
-//    override fun <T : KBvSort> transform(expr: KBvUnsignedLessOrEqualExpr<T>): KExpr<KBoolSort> {
-//
-//    }
-
     companion object {
         fun transformBody(body: KExpr<KBoolSort>, bound: KDecl<KBvSort>): Pair<KExpr<KBoolSort>, List<KDecl<*>>> =
             with(KBvQETransformer(body.ctx, bound))

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

@@ -7,12 +7,11 @@ import io.ksmt.expr.rewrite.KBvQETransformer
 import io.ksmt.sort.*
 import io.ksmt.expr.rewrite.KExprCollector
 import io.ksmt.expr.rewrite.KQuantifierSubstitutor
+import io.ksmt.utils.*
 import io.ksmt.utils.BvUtils.bvMaxValueUnsigned
 import io.ksmt.utils.BvUtils.bvZero
 import io.ksmt.utils.BvUtils.bvOne
-import io.ksmt.utils.BvUtils.isBvOne
-import io.ksmt.utils.Permutations
-import io.ksmt.utils.uncheckedCast
+import io.ksmt.utils.BvUtils.isBvZero
 
 object BvConstants {
     var bvSize = 0u
@@ -73,9 +72,9 @@ fun prepareQuantifier(ctx: KContext, assertion: KQuantifier):
         return quantifierAssertion to isUniversal
     }
 
+// p.5, 1st and 2nd steps
 fun qePreprocess(ctx: KContext, body: KExpr<KBoolSort>, bound: KDecl<*>) :
         Pair<KExpr<KBoolSort>, List<KDecl<*>>?> {
-    // p.5, 1st and 2nd steps
     val collector = KExprCollector
     val boundExpressions = collector.collectDeclarations(body) {
             arg -> sameDecl(arg, bound)}
@@ -153,10 +152,28 @@ fun linearQE(ctx: KContext, body: KExpr<KBoolSort>, bound: KDecl<*>):
         return orderedInequalities
     }
 
+    fun sameCoefficients(coefficientExpressions: Set<KExpr<*>>): Boolean {
+        var fstCoef: KBitVecValue<*>? = null
+        for ((i, expr) in coefficientExpressions.withIndex())
+        {
+            val coef = hasLinearCoefficient(bound, expr).second
+            if (i == 0)
+                fstCoef = coef
+            else if (fstCoef != coef)
+                return false
+        }
+        return true
+    }
+
     val coefficientExpressions = KExprCollector.collectDeclarations(body) { expr ->
-        hasLinearCoefficient(bound, expr) }
-    if (coefficientExpressions.isNotEmpty())
-        TODO()
+        hasLinearCoefficient(bound, expr).first }
+    var coefficient: KBitVecValue<*>? = null
+    if (coefficientExpressions.isNotEmpty()) {
+        if (sameCoefficients(coefficientExpressions))
+            coefficient = hasLinearCoefficient(bound, coefficientExpressions.first()).second
+        else
+            TODO()
+    }
     var result: KExpr<KBoolSort> = KFalse(ctx)
     var orList = arrayOf<KExpr<KBoolSort>>()
 
@@ -197,11 +214,34 @@ fun linearQE(ctx: KContext, body: KExpr<KBoolSort>, bound: KDecl<*>):
                     geP as List<KExpr<KBvSort>>
                     val orderedGe = orderInequalities(geP)
 
+                    var coefficientExpr: KExpr<KBoolSort> = mkTrue()
+                    if (coefficient != null) {
+                        var addNotOverflow: KExpr<KBoolSort> = mkTrue()
+                        var isNextLess: KExpr<KBoolSort> = mkTrue()
+                        var remainderIsZero: KExpr<KBoolSort> = mkTrue()
+                        var nextMultiple: KExpr<KBvSort> = BvConstants.bvZero.uncheckedCast()
+
+                        if (leP.isNotEmpty()) {
+                            val bigIntegerBvSize = powerOfTwo(BvConstants.bvSize).toInt().toBigInteger()
+                            val gcd = coefficient.gcd(ctx, BvConstants.bvSize, bigIntegerBvSize)
+                            val remainder = mkBvUnsignedRemExpr(leP[leP.lastIndex], gcd.uncheckedCast())
+
+                            remainderIsZero = mkBvUnsignedLessOrEqualExpr(remainder, BvConstants.bvZero.uncheckedCast())
+                            val gcdMinusRemainder = mkBvSubExpr(gcd.uncheckedCast(), remainder)
+                            addNotOverflow = mkBvAddNoOverflowExpr(leP[leP.lastIndex], gcdMinusRemainder, false)
+                            nextMultiple = mkBvAddExpr(leP[leP.lastIndex], gcdMinusRemainder)
+                        }
+                        if (geP.isNotEmpty())
+                            isNextLess = mkBvUnsignedLessExpr(nextMultiple, geP[0])
+
+                        coefficientExpr = mkAnd(isNextLess, mkOr(addNotOverflow, remainderIsZero))
+                    }
+
                     orList += if (leP.isEmpty() or geP.isEmpty())
-                        mkAnd(*orderedLe, *orderedGe)
+                        mkAnd(*orderedLe, *orderedGe, coefficientExpr)
                     else {
                         val middleLe = createInequality(leP[leP.lastIndex], geP[0])
-                        mkAnd(*orderedLe, *orderedGe, middleLe)
+                        mkAnd(*orderedLe, *orderedGe, middleLe, coefficientExpr)
                     }
                 }
             }
@@ -255,22 +295,3 @@ fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>):
     else
         curExpr.arg1 to false // bvule
 }
-
-fun sameDecl(expr: KExpr<*>, bound: KDecl<*>): Boolean =
-    expr is KConst<*> && expr.decl == bound
-
-fun occursInExponentialExpression(bound: KDecl<*>, assertion: KExpr<*>): Boolean =
-    assertion is KBvShiftLeftExpr<*> && sameDecl(assertion.shift, bound)
-
-fun hasLinearCoefficient(bound: KDecl<*>, assertion: KExpr<*>): Boolean
-{
-    if (assertion is KBvMulExpr<*>) {
-        val argPairs = arrayOf((assertion.arg0 to assertion.arg1),
-            (assertion.arg1 to assertion.arg0))
-        for ((arg, coef) in argPairs)
-        if (sameDecl(arg, bound))
-            if (coef is KBitVecValue<*> && !coef.isBvOne())
-                return true
-    }
-    return false
-}

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

@@ -0,0 +1,65 @@
+package io.ksmt.utils
+
+import io.ksmt.KContext
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.*
+import io.ksmt.utils.BvUtils.bigIntValue
+import io.ksmt.utils.BvUtils.isBvOne
+import java.math.BigInteger
+
+object Permutations {
+    fun <T> getPermutations(set: Set<T>): Set<List<T>> {
+        fun <T> allPermutations(list: List<T>): Set<List<T>> {
+            val result: MutableSet<List<T>> = mutableSetOf()
+            if (list.isEmpty())
+                result.add(list)
+            for (item in list) {
+                allPermutations(list - item).forEach { tail ->
+                    result.add(tail + item)
+                }
+            }
+            return result
+        }
+
+        if (set.isEmpty()) return setOf(emptyList())
+        return allPermutations(set.toList())
+    }
+}
+
+fun KBitVecValue<*>.gcd(ctx: KContext, bvSize: UInt, number: BigInteger):
+        KBitVecValue<*> {
+    val bvValue = this.bigIntValue()
+    val bigIntegerGCD = bvValue.gcd(number)
+    return ctx.mkBv(bigIntegerGCD, bvSize)
+}
+
+fun sameDecl(expr: KExpr<*>, bound: KDecl<*>): Boolean =
+    expr is KConst<*> && expr.decl == bound
+
+fun occursInExponentialExpression(bound: KDecl<*>, assertion: KExpr<*>): Boolean =
+    assertion is KBvShiftLeftExpr<*> && sameDecl(assertion.shift, bound)
+
+fun hasLinearCoefficient(bound: KDecl<*>, assertion: KExpr<*>): Pair<Boolean, KBitVecValue<*>?>
+{
+    val arg0: KExpr<*>
+    val arg1: KExpr<*>
+    when (assertion) {
+        is KBvMulExpr<*> -> {
+            arg0 = assertion.arg0
+            arg1 = assertion.arg1
+        }
+
+        is KBvMulNoOverflowExpr<*> -> {
+            arg0 = assertion.arg0
+            arg1 = assertion.arg1
+        }
+
+        else -> return false to null
+    }
+    val argPairs = arrayOf((arg0 to arg1), (arg1 to arg0))
+    for ((arg, coef) in argPairs)
+        if (sameDecl(arg, bound))
+            if (coef is KBitVecValue<*> && !coef.isBvOne())
+                return true to coef
+    return false to null
+}

ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt

@@ -73,7 +73,7 @@ class BvQETest {
         }
 
         @Test
-        fun regularTest0() {
+        fun test0() {
             val formula =
                 """
             (declare-fun y () (_ BitVec 4))
@@ -88,13 +88,27 @@ class BvQETest {
         }
 
         @Test
-        fun regularTest1() {
+        fun test1() {
             val formula =
                 """
             (declare-fun y () (_ BitVec 4))
             
-            (assert (exists ((x (_ BitVec 4))) 
-            (and (bvule x y) (bvult x #b0010))))
+            (assert (exists ((x (_ BitVec 4))) (and (bvule x y) (bvult x #b0010))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun test2() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            
+            (assert (exists ((x (_ BitVec 4))) (and (bvule x y) (bvule (bvmul y #b1000) x))))
             """
             val assertions = KZ3SMTLibParser(ctx).parse(formula)
             println(assertions)
@@ -111,8 +125,7 @@ class BvQETest {
             (declare-fun b () (_ BitVec 4))
             (declare-fun c () (_ BitVec 4))
             
-            (assert (exists ((x (_ BitVec 4))) 
-            (and (bvule x a) (bvuge b x) (bvult x c))))
+            (assert (exists ((x (_ BitVec 4))) (and (bvule x a) (bvuge b x) (bvult x c))))
             """
             val assertions = KZ3SMTLibParser(ctx).parse(formula)
             println(assertions)
@@ -128,8 +141,7 @@ class BvQETest {
             (declare-fun a () (_ BitVec 4))
             (declare-fun b () (_ BitVec 4))
             
-            (assert (exists ((x (_ BitVec 4))) 
-            (and (bvult x a) (bvugt b x))))
+            (assert (exists ((x (_ BitVec 4))) (and (bvult x a) (bvugt b x))))
             """
             val assertions = KZ3SMTLibParser(ctx).parse(formula)
             println(assertions)
@@ -177,21 +189,67 @@ class BvQETest {
         }
     }
 
-    class LinearTests {
+    class TestsWithSameLinearCoefficient {
         private val ctx = KContext()
 
         @Test
-        fun linTest0() {
+        fun test0() {
             val formula =
                 """
             (declare-fun y () (_ BitVec 4))
-            (assert (exists ((x (_ BitVec 4))) (bvult (bvmul x #b0111) y)))
-            (assert (bvult (bvnot y) #b1000))
+            (assert (exists ((x (_ BitVec 4))) (bvule y (bvmul x #b0111))))
+            (assert (bvule #b1111 y))
             """
             val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
             val qfAssertions = quantifierElimination(ctx, assertions)
             println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
         }
+
+        @Test
+        fun test1() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            (assert (exists ((x (_ BitVec 4))) (bvule y (bvmul x #b1000))))
+            (assert (bvule #b1111 y))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun allInequalities() {
+            val formula =
+                """
+            (declare-fun a () (_ BitVec 4))
+            (declare-fun b () (_ BitVec 4))
+            (declare-fun c () (_ BitVec 4))
+            (declare-fun d () (_ BitVec 4))
+            (declare-fun e () (_ BitVec 4))
+            (declare-fun f () (_ BitVec 4))
+            (declare-fun g () (_ BitVec 4))
+            (declare-fun h () (_ BitVec 4))
+            
+            (assert (exists ((x (_ BitVec 4))) 
+            (let ((x15 (bvmul x #b1111)))
+            (and (bvule x15 a) (bvuge b x15) (bvuge x15 c) (bvule d x15) 
+            (bvult x15 e) (bvugt f x15) (bvugt x15 g) (bvult h x15)))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+    }
+
+    class TestsWithDifferentLinearCoefficient {
+        private val ctx = KContext()
     }
 
     class ExponentialTests {