Quantifier elimination for the theory of bit vectors

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

@@ -0,0 +1,40 @@
+package io.ksmt.expr.rewrite
+
+import io.ksmt.KContext
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.*
+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()
+
+    override fun <T : KSort> transform(expr: KEqExpr<T>):
+            KExpr<KBoolSort> = with(ctx) {
+        fun eqToAndNoSimplify(l: KExpr<KBvSort>, r: KExpr<KBvSort>): KExpr<KBoolSort> =
+            mkAndNoSimplify(
+                mkBvUnsignedLessOrEqualExprNoSimplify(l, r),
+                mkBvUnsignedLessOrEqualExprNoSimplify(r, l)
+            )
+
+        expr as KEqExpr<KBvSort>
+        return transformExprAfterTransformedDefault(
+            expr, expr.lhs, expr.rhs, { eq -> eqToAndNoSimplify(eq.lhs, eq.rhs)})
+        { l, r -> eqToAndNoSimplify(l, r) }
+    }
+
+    companion object {
+        fun transformBody(body: KExpr<KBoolSort>, bound: KDecl<KBvSort>): Pair<KExpr<KBoolSort>, List<KDecl<*>>> =
+            with(KBvQETransformer(body.ctx, bound))
+            {
+                newBody = apply(body)
+                return newBody to bounds
+            }
+    }
+
+}

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

@@ -0,0 +1,25 @@
+package io.ksmt.expr.rewrite
+
+import io.ksmt.KContext
+import io.ksmt.expr.*
+import io.ksmt.expr.transformer.KNonRecursiveTransformer
+import io.ksmt.sort.KSort
+
+open class KExprCollector(ctx: KContext, private val predicate: (KExpr<*>) -> Boolean):
+    KNonRecursiveTransformer(ctx)
+{
+    private val exprCollected = hashSetOf<KExpr<*>>()
+
+    override fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T> {
+        if (predicate(expr))
+            exprCollected += expr
+        return super.transformExpr(expr)
+    }
+
+    companion object{
+        fun collectDeclarations(expr: KExpr<*>, predicate: (KExpr<*>) -> Boolean): Set<KExpr<*>> =
+            KExprCollector(expr.ctx, predicate)
+                .apply { apply(expr) }
+                .exprCollected
+    }
+}

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

@@ -47,8 +47,9 @@ open class KExprSubstitutor(ctx: KContext) : KNonRecursiveTransformer(ctx) {
         declDeclSubstitution[from] = to
     }
 
-    override fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T> =
-        exprExprSubstitution[expr]?.uncheckedCast() ?: expr
+    override fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T> {
+        return exprExprSubstitution[expr]?.uncheckedCast() ?: expr
+    }
 
     override fun <T : KSort, A : KSort> transformApp(expr: KApp<T, A>): KExpr<T> {
         val substitution: KDecl<T> = declDeclSubstitution[expr.decl]?.uncheckedCast() ?: return transformExpr(expr)

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

@@ -0,0 +1,16 @@
+package io.ksmt.expr.rewrite
+
+import io.ksmt.KContext
+import io.ksmt.expr.KExistentialQuantifier
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KUniversalQuantifier
+import io.ksmt.sort.KBoolSort
+
+class KQuantifierSubstitutor(ctx: KContext) : KExprSubstitutor(ctx) {
+
+    override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
+        transformExpr(expr)
+
+    override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> =
+        transformExpr(expr)
+}

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

@@ -0,0 +1,313 @@
+package io.ksmt.expr.rewrite.simplify
+
+import io.ksmt.KContext
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.*
+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
+
+object BvConstants {
+    var bvSize = 0u
+    var bvMaxValueUnsigned: KBitVecValue<*>? = null
+    var bvZero: KBitVecValue<*>? = null
+    var bvOne: KBitVecValue<*>? = null
+
+    fun init(ctx: KContext, expr: KDecl<*>) = with(ctx)
+    {
+        if (expr.sort is KBvSort) {
+            bvSize = expr.sort.sizeBits
+            bvMaxValueUnsigned = bvMaxValueUnsigned<KBvSort>(bvSize)
+            bvZero = bvZero<KBvSort>(bvSize)
+            bvOne = bvOne<KBvSort>(bvSize)
+        } else
+            assert(false) { "Unexpected theory." }
+    }
+}
+
+fun quantifierElimination(ctx: KContext, assertions: List<KExpr<KBoolSort>>) :
+        List<KExpr<KBoolSort>> = with(ctx) {
+        val qfAssertions = arrayListOf<KExpr<KBoolSort>>()
+
+        for (assertion in assertions) {
+            val quantifierExpressions: Set<KExpr<*>> =
+                KExprCollector.collectDeclarations(assertion) { it is KQuantifier }
+            if (quantifierExpressions.isEmpty())
+                qfAssertions.add(assertion)
+            for (qExpr in quantifierExpressions) {
+                qExpr as KQuantifier
+
+                BvConstants.init(ctx, qExpr.bounds[0])
+
+                val (quantifierExpr, isUniversal) = prepareQuantifier(ctx, qExpr)
+                var qfExpr = qeProcess(ctx, quantifierExpr)
+                if (isUniversal)
+                    qfExpr = mkNot(qfExpr)
+
+                val substitutor = KQuantifierSubstitutor(this).apply {
+                    substitute(qExpr, qfExpr)
+                }
+                val qfAssertion = substitutor.apply(assertion)
+                qfAssertions.add(qfAssertion)
+            }
+        }
+        return qfAssertions
+    }
+
+fun prepareQuantifier(ctx: KContext, assertion: KQuantifier):
+        Pair<KExistentialQuantifier, Boolean> =
+    with (ctx) {
+        val isUniversal = (assertion is KUniversalQuantifier)
+        var body = assertion.body
+        val bounds = assertion.bounds
+        if (isUniversal)
+            body = mkNot(body)
+        val quantifierAssertion = mkExistentialQuantifier(body, bounds)
+        return quantifierAssertion to isUniversal
+    }
+
+// p.5, 1st and 2nd steps: https://www.researchgate.net/publication/228686393_On_the_expansion_N_2x_of_Presburger_arithmetic
+fun qePreprocess(ctx: KContext, body: KExpr<KBoolSort>, bound: KDecl<*>) :
+        Pair<KExpr<KBoolSort>, List<KDecl<*>>?> {
+    val collector = KExprCollector
+    val boundExpressions = collector.collectDeclarations(body) {
+            arg -> sameDecl(arg, bound)}
+    if (boundExpressions.isEmpty())
+        return body to null
+
+    val (newBody, bounds) = @Suppress("UNCHECKED_CAST")
+    KBvQETransformer.transformBody(body, bound as KDecl<KBvSort>)
+    return newBody to bounds
+}
+
+fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr<KBoolSort> {
+    var qfAssertion: KExpr<KBoolSort> = assertion
+    var bounds = assertion.bounds
+    var body = assertion.body
+    for (curBound in bounds.reversed()) {
+        val (newBody, newBounds) = qePreprocess(ctx, body, curBound)
+        qfAssertion = if (newBounds != null) {
+            if (newBounds.isNotEmpty())
+                bounds = newBounds + bounds
+            val expExpressions = KExprCollector.collectDeclarations(assertion) { expr ->
+                occursInExponentialExpression(curBound, expr)
+            }
+            if (expExpressions.isEmpty())
+                linearQE(ctx, newBody, curBound)
+            else
+                TODO()
+        } else
+            newBody
+    }
+    return qfAssertion
+}
+
+
+fun linearQE(ctx: KContext, body: KExpr<KBoolSort>, bound: KDecl<*>):
+        KExpr<KBoolSort> = with(ctx) {
+
+    fun createInequality(lessExpr: KExpr<KBvSort>, greaterExpr: KExpr<KBvSort>?):
+            KExpr<KBoolSort> {
+        var condition: KExpr<KBoolSort> = mkTrue()
+        var conditionChanged = false
+        val argList = mutableListOf<KExpr<KBvSort>>()
+
+        for (item in mutableListOf(lessExpr, greaterExpr ?: BvConstants.bvMaxValueUnsigned)) {
+            if (item is KAndExpr) {
+                condition = mkAnd(item.args[0], condition)
+                conditionChanged = true
+                argList.add(item.args[1].uncheckedCast())
+            } else {
+                argList.add(item.uncheckedCast())
+            }
+        }
+
+        val lessOrEqual = mkBvUnsignedLessOrEqualExpr(argList[0], argList[1])
+        val newInequality: KExpr<KBoolSort> = if (!conditionChanged) lessOrEqual else
+            mkAnd(condition, lessOrEqual)
+        return newInequality
+    }
+
+    fun orderInequalities(permutation: List<KExpr<KBvSort>>):
+            Array<KExpr<KBoolSort>> {
+        var orderedInequalities = arrayOf<KExpr<KBoolSort>>()
+
+        if (permutation.isNotEmpty()) {
+            var lastExpr = permutation[0]
+            if (permutation.size == 1)
+                return arrayOf(createInequality(lastExpr, null))
+            for (expr in permutation) {
+                val newInequality = createInequality(lastExpr, expr)
+                orderedInequalities += newInequality
+                lastExpr = expr
+            }
+        }
+        return orderedInequalities
+    }
+
+    fun getOneCoefficientExpressions(coefficientExpressions: MutableSet<KExpr<*>>, coefficient: KBitVecValue<*>?):
+            MutableSet<KExpr<*>> {
+        val resultSet = mutableSetOf<KExpr<*>>()
+        for (expr in coefficientExpressions) {
+            val (isLinear, coef) = hasLinearCoefficient(this, bound, expr)
+            if (isLinear && coefficient == coef)
+                resultSet.add(expr)
+        }
+        return resultSet
+    }
+
+    var resultArray = arrayOf<KExpr<KBoolSort>>()
+    var freeArray = arrayOf<KExpr<KBoolSort>>()
+    when (body) {
+        is KAndExpr, is KNotExpr, is KBvUnsignedLessOrEqualExpr<*> -> {
+            val bodyArgs: MutableList<KExpr<*>> = when (body) {
+                is KAndExpr -> body.args.toMutableList()
+                else -> mutableListOf(body)
+            }
+            val bodyArgMap = mutableMapOf<KExpr<*>, Pair<KExpr<*>?, Boolean?>>()
+            while (bodyArgs.isNotEmpty()) {
+                val curExpr = bodyArgs[0]
+                val (freeSubExpr, isLess) = getFreeSubExpr(ctx, curExpr, bound)
+                if (isLess == null) {
+                    when (freeSubExpr) {
+                        null -> freeArray += curExpr as KExpr<KBoolSort>
+                        is KAndExpr -> bodyArgs += freeSubExpr.args
+                    }
+                }
+                else
+                    bodyArgMap[curExpr] = freeSubExpr to isLess
+                bodyArgs.removeFirst()
+            }
+
+            while (bodyArgMap.isNotEmpty()){
+                val bodyArg = bodyArgMap.keys.first()
+                val coefficient = hasLinearCoefficient(this, bound, bodyArg).second
+                val oneCoefExprSet = getOneCoefficientExpressions(bodyArgMap.keys, coefficient)
+
+                val leSet = mutableSetOf<KExpr<*>>()
+                val geSet = mutableSetOf<KExpr<*>>()
+                for (curExpr in oneCoefExprSet) {
+                    val (freeSubExpr, isLess) = bodyArgMap[curExpr]!!
+                    if (isLess!!)
+                        leSet.add(freeSubExpr!!)
+                    else
+                        geSet.add(freeSubExpr!!)
+
+                    bodyArgMap.remove(curExpr)
+                }
+                val lePermutations = Permutations.getPermutations(leSet)
+                val gePermutations = Permutations.getPermutations(geSet)
+                var orList = arrayOf<KExpr<KBoolSort>>()
+
+                for (leP in lePermutations) {
+                    @Suppress("UNCHECKED_CAST")
+                    leP as List<KExpr<KBvSort>>
+                    val orderedLe = orderInequalities(leP)
+
+                    for (geP in gePermutations) {
+                        @Suppress("UNCHECKED_CAST")
+                        geP as List<KExpr<KBvSort>>
+                        val orderedGe = orderInequalities(geP)
+
+                        var coefficientExpr: KExpr<KBoolSort> = mkTrue()
+                        if (!coefficient!!.isBvOne()) {
+                            var addNotOverflow: KExpr<KBoolSort> = mkTrue()
+                            var remainderIsZero: KExpr<KBoolSort> = mkTrue()
+                            var nextMultiple: KExpr<KBvSort> = BvConstants.bvZero.uncheckedCast()
+
+                            var withOverflowCheck: KExpr<KBoolSort> = mkTrue()
+                            if (leP.isNotEmpty()) {
+                                val initLastLe = leP[leP.lastIndex]
+                                var lastLe = initLastLe
+                                if (initLastLe is KAndExpr) {
+                                    lastLe = initLastLe.args[1].uncheckedCast()
+                                    withOverflowCheck = mkAnd(withOverflowCheck, initLastLe.args[0])
+                                }
+
+                                val bigIntegerBvSize = powerOfTwo(BvConstants.bvSize).toInt().toBigInteger()
+                                val gcd = coefficient.gcd(ctx, BvConstants.bvSize, bigIntegerBvSize)
+                                val remainder = mkBvUnsignedRemExpr(lastLe, gcd.uncheckedCast())
+
+                                remainderIsZero =
+                                    mkBvUnsignedLessOrEqualExpr(remainder, BvConstants.bvZero.uncheckedCast())
+                                val gcdMinusRemainder = mkBvSubExpr(gcd.uncheckedCast(), remainder)
+                                addNotOverflow = mkBvAddNoOverflowExpr(lastLe, gcdMinusRemainder, false)
+                                nextMultiple = mkBvAddExpr(lastLe, gcdMinusRemainder)
+                            }
+                            var fstGe = BvConstants.bvMaxValueUnsigned
+                            if (geP.isNotEmpty()) {
+                                val initFstGe = geP[0]
+                                if (initFstGe is KAndExpr) {
+                                    fstGe = initFstGe.args[1].uncheckedCast()
+                                    withOverflowCheck = mkAnd(withOverflowCheck, initFstGe.args[0])
+                                }
+                            }
+                            val isNextLess = mkBvUnsignedLessExpr(nextMultiple, fstGe.uncheckedCast())
+                            coefficientExpr = mkAnd(withOverflowCheck, isNextLess, mkOr(addNotOverflow, remainderIsZero))
+                        }
+                        orList += if (leP.isEmpty() or geP.isEmpty())
+                            mkAnd(*orderedLe, *orderedGe, coefficientExpr)
+                        else {
+                            val middleLe = createInequality(leP[leP.lastIndex], geP[0])
+                            mkAnd(*orderedLe, *orderedGe, middleLe, coefficientExpr)
+                        }
+                    }
+                }
+                resultArray += mkAnd(mkOr(*orList))
+            }
+        }
+        else -> assert(false) {
+            "Expression ${body}:${body.javaClass.typeName} " +
+                    "is not in required form."
+        }
+    }
+    return mkAnd(*resultArray, *freeArray)
+}
+
+fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>):
+        Pair<KExpr<*>?, Boolean?> = with(ctx) {
+    val curExpr = if (expr is KNotExpr) expr.arg else expr
+    if (curExpr is KAndExpr)
+        return expr to null
+    else if (curExpr !is KBvUnsignedLessOrEqualExpr<*>)
+        assert(false) { "Expression ${curExpr}:${curExpr.javaClass.typeName} " +
+                "is not in required form." }
+
+    @Suppress("UNCHECKED_CAST")
+    curExpr as KBvUnsignedLessOrEqualExpr<KBvSort>
+    val collector = KExprCollector
+    val bvOneExpr: KExpr<KBvSort> = BvConstants.bvOne.uncheckedCast()
+    var boundExpressions = collector.collectDeclarations(curExpr.arg0) {
+        arg -> sameDecl(arg, bound)}
+    if (boundExpressions.isEmpty()) {
+        boundExpressions = collector.collectDeclarations(curExpr.arg1) {
+                arg -> sameDecl(arg, bound)}
+        if (boundExpressions.isEmpty())
+            return null to null //
+        return if (expr is KNotExpr) {
+            val condition = mkBvUnsignedGreaterOrEqualExpr(curExpr.arg0, bvOneExpr)
+            val trueBranch = mkBvSubExpr(curExpr.arg0, bvOneExpr)
+            val newFreeSubExpr = mkAndNoSimplify(condition, trueBranch.uncheckedCast())
+            newFreeSubExpr to false // bvult
+        }
+        else
+            curExpr.arg0 to true // bvuge
+    }
+    return if (expr is KNotExpr) {
+        val condition: KExpr<KBoolSort> = mkBvUnsignedLessExpr(
+            curExpr.arg1,
+            BvConstants.bvMaxValueUnsigned.uncheckedCast()
+        )
+        val trueBranch = mkBvAddExpr(curExpr.arg1, bvOneExpr)
+        val newFreeSubExpr = mkAndNoSimplify(condition, trueBranch.uncheckedCast())
+        newFreeSubExpr to true // bvugt
+    }
+    else
+        curExpr.arg1 to false // bvule
+}

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

@@ -0,0 +1,87 @@
+package io.ksmt.utils
+
+import io.ksmt.KContext
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.*
+import io.ksmt.expr.rewrite.KExprCollector
+import io.ksmt.expr.rewrite.simplify.BvConstants
+import io.ksmt.sort.KBvSort
+import io.ksmt.utils.BvUtils.bigIntValue
+import io.ksmt.utils.BvUtils.bvOne
+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(ctx: KContext, bound: KDecl<*>, assertion: KExpr<*>): Pair<Boolean, KBitVecValue<*>?>
+{
+    val mulTerms = KExprCollector.collectDeclarations(assertion) {
+            arg -> arg is KBvMulExpr || arg is KBvMulNoOverflowExpr<*>}
+    var mulTerm: KExpr<*>? = null
+    for (curTerm in mulTerms) {
+        val mulTerms = KExprCollector.collectDeclarations(curTerm) { arg -> sameDecl(arg, bound) }
+        if (mulTerms.isNotEmpty()) {
+            mulTerm = curTerm
+            break
+        }
+    }
+    if (mulTerm == null) {
+        val linearTerms = KExprCollector.collectDeclarations(assertion) { arg -> sameDecl(arg, bound) }
+        return if (linearTerms.isNotEmpty())
+            true to ctx.bvOne<KBvSort>(BvConstants.bvSize)
+        else
+            false to null
+    }
+
+    val arg0: KExpr<*>
+    val arg1: KExpr<*>
+    when (mulTerm) {
+        is KBvMulExpr<*> -> {
+            arg0 = mulTerm.arg0
+            arg1 = mulTerm.arg1
+        }
+
+        is KBvMulNoOverflowExpr<*> -> {
+            arg0 = mulTerm.arg0
+            arg1 = mulTerm.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<*>)
+                return true to coef
+    return false to null
+}

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

@@ -0,0 +1,315 @@
+package io.ksmt.expr.rewrite.simplify
+
+import io.ksmt.KContext
+import io.ksmt.expr.KExpr
+import io.ksmt.solver.KSolverStatus
+import io.ksmt.solver.z3.KZ3SMTLibParser
+import io.ksmt.solver.z3.KZ3Solver
+import io.ksmt.sort.KBoolSort
+import kotlin.test.Test
+
+
+fun xorEquivalenceCheck(ctx: KContext,
+                        quantifierAssertions: List<KExpr<KBoolSort>>,
+                        quantifierFreeAssertions: List<KExpr<KBoolSort>>):
+        Boolean = with(ctx) {
+    for ((i, qAssertion) in quantifierAssertions.withIndex()) {
+        val qfAssertion = quantifierFreeAssertions[i]
+        val xorExpr = mkXor(qAssertion, qfAssertion)
+
+        val solver = KZ3Solver(ctx)
+        solver.assert(xorExpr)
+        val status = solver.check()
+        if (status == KSolverStatus.SAT) {
+            print("\n${solver.model()}\n")
+            return false
+        }
+    }
+    return true
+}
+
+class BvQETest {
+    class LinearTestsWithoutLinearCoefficients {
+        private val ctx = KContext()
+
+        @Test
+        fun xLessOrEqualY() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            (assert (exists ((x (_ BitVec 4))) (bvule x y)))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun xLessOrEqualZero() {
+            val formula =
+                """
+            (assert (exists ((x (_ BitVec 4))) (bvult x #b0000)))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun xLessOrEqualOne() {
+            val formula =
+                """
+            (assert (exists ((x (_ BitVec 4))) (bvult x #b0001)))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun test0() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            (assert (exists ((x (_ BitVec 4))) (and (bvule x y) (bvuge x #b0010))))
+            (assert (bvule y #b1000))
+            """
+            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))) (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)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun threeLess() {
+            val formula =
+                """
+            (declare-fun a () (_ BitVec 4))
+            (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))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun twoLess() {
+            val formula =
+                """
+            (declare-fun a () (_ BitVec 4))
+            (declare-fun b () (_ BitVec 4))
+            
+            (assert (exists ((x (_ BitVec 4))) (and (bvult x a) (bvugt b x))))
+            """
+            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))) 
+            (and (bvule x a) (bvuge b x) (bvuge x c) (bvule d x) 
+            (bvult x e) (bvugt f x) (bvugt x g) (bvult h x))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun notExistsTest() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            (assert (exists ((x (_ BitVec 4))) (and (bvult x y) (bvule y #b0000))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+    }
+
+    class TestsWithSameLinearCoefficient {
+        private val ctx = KContext()
+
+        @Test
+        fun test0() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            (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()
+
+        @Test
+        fun falseTest() {
+            val formula =
+                """
+            (assert (exists ((x (_ BitVec 4))) 
+            (and (bvugt x #b0001) (bvult (bvmul x #b0010) #b0011) (bvuge (bvmul x #b0100) #b0101))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+
+        @Test
+        fun test0() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            
+            (assert (exists ((x (_ BitVec 4))) 
+            (and (bvule x #b0111) (bvule (bvmul x #b0010) 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))) 
+            (and (bvugt x #b0001) (bvult (bvmul x #b0010) #b0011) (bvuge (bvmul x #b0100) y))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            println(assertions)
+            val qfAssertions = quantifierElimination(ctx, assertions)
+            println(qfAssertions)
+            assert(xorEquivalenceCheck(ctx, assertions, qfAssertions))
+        }
+    }
+
+    class ExponentialTests {
+        private val ctx = KContext()
+
+        @Test
+        fun test() {
+            val formula =
+                """
+            (declare-fun y () (_ BitVec 4))
+            (assert (exists ((x (_ BitVec 4))) (or (bvult (bvshl #b0001 x) y) (= (bvshl #b0001 x) y))))
+            """
+            val assertions = KZ3SMTLibParser(ctx).parse(formula)
+            quantifierElimination(ctx, assertions)
+        }
+    }
+}