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)
+}