From 76c456174353f19b48099c9c7d89f45f2bad0274 Mon Sep 17 00:00:00 2001 From: Anzhela Sukhanova Date: Fri, 30 Jun 2023 17:22:08 +0300 Subject: [PATCH 01/10] start work on QE for BV arithmetic --- .../simplify/BvQuantifierElimination.kt | 71 +++++++++++++++++++ .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 37 ++++++++++ 2 files changed, 108 insertions(+) create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt create mode 100644 ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt new file mode 100644 index 000000000..868bd9b9f --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -0,0 +1,71 @@ +package io.ksmt.expr.rewrite.simplify + +import io.ksmt.KContext +import io.ksmt.decl.KDecl +import io.ksmt.expr.* +import io.ksmt.sort.* + +fun isBoundTerm(assertion: KExpr): Boolean +{ + var curAssertion = assertion + while (curAssertion is KNotExpr) + curAssertion = curAssertion.arg + return curAssertion is KQuantifier +} + +fun qePreprocess(ctx: KContext, + assertions: List>, + boundAssertions: ArrayList, + notAssertions: ArrayList, + freeAssertions: ArrayList>) +{ + with (ctx) + { + for ((i, assertion) in assertions.withIndex()) { + var notNumber = 0 + var newAssertion = assertion + while (newAssertion is KNotExpr) + { + notNumber += 1 + newAssertion = newAssertion.arg + } + + //For now, we assume that all bound variables are under the one quantifier + if (newAssertion is KQuantifier) + { + val isUniversal = newAssertion is KUniversalQuantifier + var body = newAssertion.body + val bounds = newAssertion.bounds + if (isUniversal) + body = mkNot(body) + body = simplifyNot(body) + newAssertion = mkExistentialQuantifier(body, bounds) + if ((isUniversal and (notNumber % 2 == 0)) or + (notNumber % 2 == 1)) + notAssertions[i] = true + boundAssertions.add(newAssertion) + } + else + freeAssertions.add(assertion) + } + } +} + +fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr +{ + val qfAssertion = KTrue(ctx) + var bounds = assertion.bounds + val boundNum = bounds.size + var curBound = bounds[boundNum - 1] + var curAssert = assertion + if (varOccursLinearly(curAssert, curBound)) + println() + else + println() + return qfAssertion +} + +fun varOccursLinearly(assertion: KExistentialQuantifier, bound: KDecl<*>): Boolean +{ + return true +} diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt new file mode 100644 index 000000000..3ced3c3c4 --- /dev/null +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -0,0 +1,37 @@ +package io.ksmt.expr.rewrite.simplify + +import io.ksmt.KContext +import io.ksmt.expr.KExistentialQuantifier +import io.ksmt.expr.KExpr +import io.ksmt.solver.z3.KZ3SMTLibParser +import io.ksmt.sort.KBoolSort +import kotlin.test.Test + +class BvQETest { + private val ctx = KContext() + + @Test + fun mainTest() { + + val formula = + """ + (declare-fun y () (_ BitVec 4)) + (assert (exists ((x (_ BitVec 4))) (not (not (bvult (bvmul x #b0111) y))))) + (assert (bvult (bvnot y) #b1000)) + """ + + val assertions = KZ3SMTLibParser(ctx).parse(formula) + + val boundAssertions = arrayListOf() + val notAssertions = arrayListOf() + val freeAssertions = arrayListOf>() + + qePreprocess(ctx, assertions, boundAssertions, notAssertions, freeAssertions) + var qfAssertions = arrayListOf>() + for (assert in boundAssertions) + { + val qfAssertion = qeProcess(ctx, assert) + qfAssertions.add(qfAssertion) + } + } +} \ No newline at end of file From 9056f3575efa72eac2207f3f371c5a3bcc74221f Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Tue, 18 Jul 2023 17:49:27 +0300 Subject: [PATCH 02/10] add the simplest case of QE for BV theory --- .../io/ksmt/expr/rewrite/KExprCollector.kt | 25 +++ .../expr/rewrite/KQuantifierSubstitutor.kt | 16 ++ .../simplify/BvQuantifierElimination.kt | 176 +++++++++++++----- .../main/kotlin/io/ksmt/utils/Permutations.kt | 19 ++ .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 40 ++-- 5 files changed, 211 insertions(+), 65 deletions(-) create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KExprCollector.kt create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KQuantifierSubstitutor.kt create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KExprCollector.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KExprCollector.kt new file mode 100644 index 000000000..60834109b --- /dev/null +++ b/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>() + + override fun transformExpr(expr: KExpr): KExpr { + if (predicate(expr)) + exprCollected += expr + return super.transformExpr(expr) + } + + companion object{ + fun collectDeclarations(expr: KExpr<*>, predicate: (KExpr<*>) -> Boolean): Set> = + KExprCollector(expr.ctx, predicate) + .apply { apply(expr) } + .exprCollected + } +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KQuantifierSubstitutor.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KQuantifierSubstitutor.kt new file mode 100644 index 000000000..7f00cba3d --- /dev/null +++ b/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 = + transformExpr(expr) + + override fun transform(expr: KUniversalQuantifier): KExpr = + transformExpr(expr) +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index 868bd9b9f..a0f370b38 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -4,68 +4,146 @@ import io.ksmt.KContext import io.ksmt.decl.KDecl import io.ksmt.expr.* import io.ksmt.sort.* +import io.ksmt.expr.rewrite.KExprCollector +import io.ksmt.expr.rewrite.KQuantifierSubstitutor +import io.ksmt.utils.BvUtils.bvMaxValueSigned +import io.ksmt.utils.BvUtils.bvMaxValueUnsigned +import io.ksmt.utils.BvUtils.bvMinValueSigned +import io.ksmt.utils.BvUtils.bvZero +import io.ksmt.utils.BvUtils.isBvOne +import io.ksmt.utils.Permutations +import io.ksmt.utils.uncheckedCast -fun isBoundTerm(assertion: KExpr): Boolean -{ - var curAssertion = assertion - while (curAssertion is KNotExpr) - curAssertion = curAssertion.arg - return curAssertion is KQuantifier +object BvConstants { + var bvSize = 0u + var bvMaxValueSigned: KBitVecValue<*>? = null + var bvMinValueSigned: KBitVecValue<*>? = null + var bvMaxValueUnsigned: KBitVecValue<*>? = null + var bvZero: KBitVecValue<*>? = null + + fun init(ctx: KContext, expr: KDecl<*>) { + if (expr.sort is KBvSort) { + bvSize = expr.sort.sizeBits + bvMaxValueSigned = ctx.bvMaxValueSigned(bvSize) + bvMinValueSigned = ctx.bvMinValueSigned(bvSize) + bvMaxValueUnsigned = ctx.bvMaxValueUnsigned(bvSize) + bvZero = ctx.bvZero(bvSize) + } else + assert(false) { "Unexpected theory." } + } } -fun qePreprocess(ctx: KContext, - assertions: List>, - boundAssertions: ArrayList, - notAssertions: ArrayList, - freeAssertions: ArrayList>) -{ - with (ctx) - { - for ((i, assertion) in assertions.withIndex()) { - var notNumber = 0 - var newAssertion = assertion - while (newAssertion is KNotExpr) - { - notNumber += 1 - newAssertion = newAssertion.arg - } +fun quantifierElimination(ctx: KContext, assertions: List>): List> = + with(ctx) { + val qfAssertions = arrayListOf>() + + for (assertion in assertions) { + val quantifierExpressions = KExprCollector.collectDeclarations(assertion) { it is KQuantifier } + if (quantifierExpressions.isEmpty()) + qfAssertions.add(assertion) + for (curExpr in quantifierExpressions) { + val qExpr = curExpr as KQuantifier + + BvConstants.init(ctx, qExpr.bounds[0]) - //For now, we assume that all bound variables are under the one quantifier - if (newAssertion is KQuantifier) - { - val isUniversal = newAssertion is KUniversalQuantifier - var body = newAssertion.body - val bounds = newAssertion.bounds + val (quantifierExpr, isUniversal) = qePreprocess(ctx, qExpr) + var qfExpr = qeProcess(ctx, quantifierExpr) if (isUniversal) - body = mkNot(body) - body = simplifyNot(body) - newAssertion = mkExistentialQuantifier(body, bounds) - if ((isUniversal and (notNumber % 2 == 0)) or - (notNumber % 2 == 1)) - notAssertions[i] = true - boundAssertions.add(newAssertion) + qfExpr = mkNot(qfExpr) + + // println(curExpr.body) + val substitutor = KQuantifierSubstitutor(this).apply { + substitute(qExpr, qfExpr) + } + val qfAssertion = substitutor.apply(assertion) + qfAssertions.add(qfAssertion) } - else - freeAssertions.add(assertion) } + return qfAssertions + } + +fun qePreprocess(ctx: KContext, assertion: KQuantifier): + Pair = + with (ctx) { + val isUniversal = (assertion is KUniversalQuantifier) + var body = assertion.body + val bounds = assertion.bounds + if (isUniversal) + body = mkNot(body) + body = simplifyNot(body) + // TODO toRequiredForm(body, bounds) p.5, 1st and 2nd steps + val quantifierAssertion = mkExistentialQuantifier(body, bounds) + return quantifierAssertion to isUniversal } + +fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr { + var qfAssertion: KExpr = assertion + val bounds = assertion.bounds + for (curBound in bounds.reversed()) { + val expExpressions = KExprCollector.collectDeclarations(assertion) { expr -> + occursInExponentialExpression(curBound, expr) } + if (expExpressions.isEmpty()) + qfAssertion = linearQE(ctx, assertion, curBound) + else + TODO() + } + + return qfAssertion } -fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr +fun linearQE(ctx: KContext, assertion: KExistentialQuantifier, bound: KDecl<*>): + KExpr { - val qfAssertion = KTrue(ctx) - var bounds = assertion.bounds - val boundNum = bounds.size - var curBound = bounds[boundNum - 1] - var curAssert = assertion - if (varOccursLinearly(curAssert, curBound)) - println() + val coefficientExpressions = KExprCollector.collectDeclarations(assertion) { expr -> + hasLinearCoefficient(bound, expr) } + if (coefficientExpressions.isNotEmpty()) + TODO() + val body = assertion.body + + if (body is KAndExpr) { + val lessSet = mutableSetOf>() + val greaterSet = mutableSetOf>() + for (expr in body.args) { + if (isBvNonStrictGreater(expr)) + greaterSet.add(expr) + if (isBvNonStrictLess(expr)) + lessSet.add(expr) + } + val lessPermutations = Permutations.getPermutations(lessSet) + val greaterPermutations = Permutations.getPermutations(lessSet) + TODO() + } + + else if (isBvNonStrictGreater(body) || isBvNonStrictLess(body)) + return KTrue(ctx) + else - println() - return qfAssertion + assert(false) { "Expression is not in required form." } + + return KFalse(ctx) } -fun varOccursLinearly(assertion: KExistentialQuantifier, bound: KDecl<*>): Boolean +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 { - return true + 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 } + +fun isBvNonStrictGreater(expr: KExpr<*>): Boolean = + (expr is KBvUnsignedGreaterOrEqualExpr<*>) || (expr is KBvSignedGreaterOrEqualExpr<*>) + +fun isBvNonStrictLess(expr: KExpr<*>): Boolean = + (expr is KBvUnsignedLessOrEqualExpr<*>) || (expr is KBvSignedLessOrEqualExpr<*>) \ No newline at end of file diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt new file mode 100644 index 000000000..61a51c8dd --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt @@ -0,0 +1,19 @@ +package io.ksmt.utils + +object Permutations { + + fun getPermutations(set: Set): Set> { + fun allPermutations(list: List): Set> { + val result: MutableSet> = mutableSetOf() + for (i in list.indices) { + allPermutations(list - list[i]).forEach { item -> + result.add(item + list[i]) + } + } + return result + } + + if (set.isEmpty()) return setOf(emptyList()) + return allPermutations(set.toList()) + } +} \ No newline at end of file diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index 3ced3c3c4..bce575e8b 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -1,37 +1,45 @@ package io.ksmt.expr.rewrite.simplify import io.ksmt.KContext -import io.ksmt.expr.KExistentialQuantifier -import io.ksmt.expr.KExpr import io.ksmt.solver.z3.KZ3SMTLibParser -import io.ksmt.sort.KBoolSort import kotlin.test.Test class BvQETest { private val ctx = KContext() @Test - fun mainTest() { + fun simplestTest() { + val formula = + """ + (declare-fun y () (_ BitVec 4)) + (assert (exists ((x (_ BitVec 4))) (bvult x y))) + """ + val assertions = KZ3SMTLibParser(ctx).parse(formula) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } + @Test + fun linTest() { val formula = """ (declare-fun y () (_ BitVec 4)) (assert (exists ((x (_ BitVec 4))) (not (not (bvult (bvmul x #b0111) y))))) (assert (bvult (bvnot y) #b1000)) """ - val assertions = KZ3SMTLibParser(ctx).parse(formula) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } - val boundAssertions = arrayListOf() - val notAssertions = arrayListOf() - val freeAssertions = arrayListOf>() - - qePreprocess(ctx, assertions, boundAssertions, notAssertions, freeAssertions) - var qfAssertions = arrayListOf>() - for (assert in boundAssertions) - { - val qfAssertion = qeProcess(ctx, assert) - qfAssertions.add(qfAssertion) - } + @Test + fun expTest() { + 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) } } \ No newline at end of file From ab868d7c78474c572548f3710cdaec1bd471c28f Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Tue, 29 Aug 2023 11:55:36 +0300 Subject: [PATCH 03/10] extend quantifier elimination for linear bv-expressions --- .../io/ksmt/expr/rewrite/KBvQETransformer.kt | 54 +++++ .../io/ksmt/expr/rewrite/KExprSubstitutor.kt | 5 +- .../simplify/BvQuantifierElimination.kt | 202 +++++++++++++----- .../main/kotlin/io/ksmt/utils/Permutations.kt | 8 +- .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 60 +++++- 5 files changed, 268 insertions(+), 61 deletions(-) create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt new file mode 100644 index 000000000..f9c848380 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt @@ -0,0 +1,54 @@ +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 + +@Suppress("UNCHECKED_CAST") +class KBvQETransformer(ctx: KContext, bound: KDecl) : KNonRecursiveTransformer(ctx) { + private var bounds = mutableListOf>() + private var newBody: KExpr = ctx.mkTrue() + +// // bool transformers +// override fun transform(expr: KAndExpr): KExpr { +// } +// +// override fun transform(expr: KAndBinaryExpr): KExpr { +// } + + override fun transform(expr: KEqExpr): + KExpr = with(ctx) { + fun eqToAndNoSimplify(l: KExpr, r: KExpr): KExpr = + mkAndNoSimplify( + mkBvUnsignedLessOrEqualExprNoSimplify(l, r), + mkBvUnsignedLessOrEqualExprNoSimplify(r, l) + ) + + expr as KEqExpr + return transformExprAfterTransformedDefault( + expr, expr.lhs, expr.rhs, { eq -> eqToAndNoSimplify(eq.lhs, eq.rhs)}) + { l, r -> eqToAndNoSimplify(l, r) } + } + +// override fun transform(expr: KNotExpr): KExpr { +// } + +// // bit-vec expressions transformers +// override fun transform(expr: KBvUnsignedLessOrEqualExpr): KExpr { +// +// } + + companion object { + fun transformBody(body: KExpr, bound: KDecl): Pair, List>> = + with(KBvQETransformer(body.ctx, bound)) + { + newBody = apply(body) + return newBody to bounds + } + } + +} \ No newline at end of file diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KExprSubstitutor.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KExprSubstitutor.kt index 3d9c31691..4e35cac7b 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KExprSubstitutor.kt +++ b/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 transformExpr(expr: KExpr): KExpr = - exprExprSubstitution[expr]?.uncheckedCast() ?: expr + override fun transformExpr(expr: KExpr): KExpr { + return exprExprSubstitution[expr]?.uncheckedCast() ?: expr + } override fun transformApp(expr: KApp): KExpr { val substitution: KDecl = declDeclSubstitution[expr.decl]?.uncheckedCast() ?: return transformExpr(expr) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index a0f370b38..4d3b88e16 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -3,55 +3,53 @@ 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.BvUtils.bvMaxValueSigned import io.ksmt.utils.BvUtils.bvMaxValueUnsigned -import io.ksmt.utils.BvUtils.bvMinValueSigned 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 object BvConstants { var bvSize = 0u - var bvMaxValueSigned: KBitVecValue<*>? = null - var bvMinValueSigned: KBitVecValue<*>? = null var bvMaxValueUnsigned: KBitVecValue<*>? = null var bvZero: KBitVecValue<*>? = null + var bvOne: KBitVecValue<*>? = null fun init(ctx: KContext, expr: KDecl<*>) { if (expr.sort is KBvSort) { bvSize = expr.sort.sizeBits - bvMaxValueSigned = ctx.bvMaxValueSigned(bvSize) - bvMinValueSigned = ctx.bvMinValueSigned(bvSize) bvMaxValueUnsigned = ctx.bvMaxValueUnsigned(bvSize) bvZero = ctx.bvZero(bvSize) + bvOne = ctx.bvOne(bvSize) } else assert(false) { "Unexpected theory." } } } -fun quantifierElimination(ctx: KContext, assertions: List>): List> = - with(ctx) { +fun quantifierElimination(ctx: KContext, assertions: List>) : + List> = with(ctx) { val qfAssertions = arrayListOf>() for (assertion in assertions) { - val quantifierExpressions = KExprCollector.collectDeclarations(assertion) { it is KQuantifier } + val quantifierExpressions: Set> = + KExprCollector.collectDeclarations(assertion) { it is KQuantifier } if (quantifierExpressions.isEmpty()) qfAssertions.add(assertion) - for (curExpr in quantifierExpressions) { - val qExpr = curExpr as KQuantifier + for (qExpr in quantifierExpressions) { + qExpr as KQuantifier BvConstants.init(ctx, qExpr.bounds[0]) - val (quantifierExpr, isUniversal) = qePreprocess(ctx, qExpr) + val (quantifierExpr, isUniversal) = prepareQuantifier(ctx, qExpr) var qfExpr = qeProcess(ctx, quantifierExpr) if (isUniversal) qfExpr = mkNot(qfExpr) - // println(curExpr.body) val substitutor = KQuantifierSubstitutor(this).apply { substitute(qExpr, qfExpr) } @@ -62,7 +60,7 @@ fun quantifierElimination(ctx: KContext, assertions: List>): Li return qfAssertions } -fun qePreprocess(ctx: KContext, assertion: KQuantifier): +fun prepareQuantifier(ctx: KContext, assertion: KQuantifier): Pair = with (ctx) { val isUniversal = (assertion is KUniversalQuantifier) @@ -70,57 +68,163 @@ fun qePreprocess(ctx: KContext, assertion: KQuantifier): val bounds = assertion.bounds if (isUniversal) body = mkNot(body) - body = simplifyNot(body) - // TODO toRequiredForm(body, bounds) p.5, 1st and 2nd steps val quantifierAssertion = mkExistentialQuantifier(body, bounds) return quantifierAssertion to isUniversal } +fun qePreprocess(ctx: KContext, body: KExpr, bound: KDecl<*>) : + Pair, List>?> { + // p.5, 1st and 2nd steps + 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) + return newBody to bounds +} + fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr { var qfAssertion: KExpr = assertion - val bounds = assertion.bounds + var bounds = assertion.bounds + var body = assertion.body for (curBound in bounds.reversed()) { - val expExpressions = KExprCollector.collectDeclarations(assertion) { expr -> - occursInExponentialExpression(curBound, expr) } - if (expExpressions.isEmpty()) - qfAssertion = linearQE(ctx, assertion, curBound) - else - TODO() + 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, assertion: KExistentialQuantifier, bound: KDecl<*>): - KExpr -{ - val coefficientExpressions = KExprCollector.collectDeclarations(assertion) { expr -> + +fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): + KExpr = with(ctx) { + fun orderInequalities(permutation: List>): Array> + { + var orderedInequalities = arrayOf>() + + if (permutation.isNotEmpty()) { + var lastExpr = permutation[0] + for ((i, expr) in permutation.withIndex()) { + if (i % 2 == 0) + lastExpr = expr + else { + val lessOrEqual = mkBvSignedLessOrEqualExpr(lastExpr, expr) + orderedInequalities += lessOrEqual + } + } + } + return orderedInequalities + } + + val coefficientExpressions = KExprCollector.collectDeclarations(body) { expr -> hasLinearCoefficient(bound, expr) } if (coefficientExpressions.isNotEmpty()) TODO() - val body = assertion.body - - if (body is KAndExpr) { - val lessSet = mutableSetOf>() - val greaterSet = mutableSetOf>() - for (expr in body.args) { - if (isBvNonStrictGreater(expr)) - greaterSet.add(expr) - if (isBvNonStrictLess(expr)) - lessSet.add(expr) + var result: KExpr = KFalse(ctx) + + when (body) { + is KAndExpr, is KNotExpr, is KBvUnsignedLessOrEqualExpr<*> -> { + val leSet = mutableSetOf>() + val geSet = mutableSetOf>() + var freeSet = arrayOf>() + val args: MutableList> = when(body) { + is KAndExpr -> body.args.toMutableList() + else -> mutableListOf(body) + } + while (args.isNotEmpty()) { + val expr = args[0] + val (isLe, freeSubExpr) = getFreeSubExpr(ctx, expr, bound) + if (isLe == null) { + when (freeSubExpr) + { + null -> freeSet += expr + is KAndExpr -> args += freeSubExpr.args + } + } + else if (isLe) + leSet.add(freeSubExpr!!) + else + geSet.add(freeSubExpr!!) + args.removeFirst() + } + val lePermutations = Permutations.getPermutations(leSet) + val gePermutations = Permutations.getPermutations(geSet) + for (leP in lePermutations) { + @Suppress("UNCHECKED_CAST") + leP as List> + val orderedLe = orderInequalities(leP) + + for (geP in gePermutations) { + @Suppress("UNCHECKED_CAST") + geP as List> + val orderedGe = orderInequalities(geP) + + result = if (leP.isEmpty() or geP.isEmpty()) + mkAnd(*orderedLe, *orderedGe, *freeSet) + else { + val middleLe = mkBvUnsignedLessOrEqualExpr(leP[leP.lastIndex], geP[0]) + mkAnd(*orderedLe, *orderedGe, middleLe, *freeSet) + } + } + } } - val lessPermutations = Permutations.getPermutations(lessSet) - val greaterPermutations = Permutations.getPermutations(lessSet) - TODO() + else -> assert(false) { "Expression ${body}:${body.javaClass.typeName} " + + "is not in required form." } } + return result +} - else if (isBvNonStrictGreater(body) || isBvNonStrictLess(body)) - return KTrue(ctx) - +fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): + Pair?> = with(ctx) { + val curExpr = if (expr is KNotExpr) expr.arg else expr + if (curExpr is KAndExpr) + return null to expr + else if (curExpr !is KBvUnsignedLessOrEqualExpr<*>) + assert(false) { "Expression ${curExpr}:${curExpr.javaClass.typeName} " + + "is not in required form." } + + @Suppress("UNCHECKED_CAST") + curExpr as KBvUnsignedLessOrEqualExpr + val collector = KExprCollector + val bvOneExpr: KExpr = 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 = mkBvUnsignedLessExpr(curExpr.arg0, bvOneExpr) + val falseBranch = mkBvSubExpr(curExpr.arg0, bvOneExpr) + val newFreeSubExpr = mkIte(condition, mkFalse().uncheckedCast(), falseBranch) + true to newFreeSubExpr // bvult + } + else + false to curExpr.arg0 // bvuge + } + return if (expr is KNotExpr) { + val condition: KExpr = (curExpr.arg1 == BvConstants.bvMaxValueUnsigned).uncheckedCast() + val falseBranch = mkBvAddExpr(curExpr.arg1, bvOneExpr) + val newFreeSubExpr = mkIte(condition, BvConstants.bvZero.uncheckedCast(), falseBranch) + false to newFreeSubExpr // bvugt + } else - assert(false) { "Expression is not in required form." } - - return KFalse(ctx) + true to curExpr.arg1 // bvule } fun sameDecl(expr: KExpr<*>, bound: KDecl<*>): Boolean = @@ -141,9 +245,3 @@ fun hasLinearCoefficient(bound: KDecl<*>, assertion: KExpr<*>): Boolean } return false } - -fun isBvNonStrictGreater(expr: KExpr<*>): Boolean = - (expr is KBvUnsignedGreaterOrEqualExpr<*>) || (expr is KBvSignedGreaterOrEqualExpr<*>) - -fun isBvNonStrictLess(expr: KExpr<*>): Boolean = - (expr is KBvUnsignedLessOrEqualExpr<*>) || (expr is KBvSignedLessOrEqualExpr<*>) \ No newline at end of file diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt index 61a51c8dd..99ceff18f 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt @@ -5,9 +5,11 @@ object Permutations { fun getPermutations(set: Set): Set> { fun allPermutations(list: List): Set> { val result: MutableSet> = mutableSetOf() - for (i in list.indices) { - allPermutations(list - list[i]).forEach { item -> - result.add(item + list[i]) + if (list.isEmpty()) + result.add(list) + for (item in list) { + allPermutations(list - item).forEach { tail -> + result.add(tail + item) } } return result diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index bce575e8b..b45d91afc 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -8,23 +8,75 @@ class BvQETest { private val ctx = KContext() @Test - fun simplestTest() { + fun linTestWithoutLinCoef0() { val formula = """ (declare-fun y () (_ BitVec 4)) - (assert (exists ((x (_ BitVec 4))) (bvult x y))) + (assert (exists ((x (_ BitVec 4))) (bvule x y))) """ val assertions = KZ3SMTLibParser(ctx).parse(formula) + println(assertions) val qfAssertions = quantifierElimination(ctx, assertions) println(qfAssertions) } @Test - fun linTest() { + fun linTestWithoutLinCoef1() { + 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) + } + + @Test + fun linTestWithoutLinCoef2() { + 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) + } + + @Test + fun linTestWithoutLinCoef3() { + 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) + } + + @Test + fun linTestWithoutLinCoef4() { + 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) + } + + @Test + fun linTest0() { val formula = """ (declare-fun y () (_ BitVec 4)) - (assert (exists ((x (_ BitVec 4))) (not (not (bvult (bvmul x #b0111) y))))) + (assert (exists ((x (_ BitVec 4))) (bvult (bvmul x #b0111) y))) (assert (bvult (bvnot y) #b1000)) """ val assertions = KZ3SMTLibParser(ctx).parse(formula) From 9dd2eeb49e8089e09b1f0aaed08cf98f02e04e78 Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Mon, 11 Sep 2023 16:40:12 +0300 Subject: [PATCH 04/10] fix problem in QE for BV theory --- .../simplify/BvQuantifierElimination.kt | 43 +++-- .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 163 +++++++++++------- 2 files changed, 131 insertions(+), 75 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index 4d3b88e16..7d52a3a5f 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -20,12 +20,13 @@ object BvConstants { var bvZero: KBitVecValue<*>? = null var bvOne: KBitVecValue<*>? = null - fun init(ctx: KContext, expr: KDecl<*>) { + fun init(ctx: KContext, expr: KDecl<*>) = with(ctx) + { if (expr.sort is KBvSort) { bvSize = expr.sort.sizeBits - bvMaxValueUnsigned = ctx.bvMaxValueUnsigned(bvSize) - bvZero = ctx.bvZero(bvSize) - bvOne = ctx.bvOne(bvSize) + bvMaxValueUnsigned = bvMaxValueUnsigned(bvSize) + bvZero = bvZero(bvSize) + bvOne = bvOne(bvSize) } else assert(false) { "Unexpected theory." } } @@ -112,6 +113,25 @@ fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr, bound: KDecl<*>): KExpr = with(ctx) { + + fun createInequality(lessExpr: KExpr, greaterExpr: KExpr): KExpr { + var condition: KExpr = mkTrue() + var expr0 = lessExpr + if (expr0 is KAndExpr) { + condition = expr0.args[0] + expr0 = expr0.args[1].uncheckedCast() + } + var expr1 = greaterExpr + if (expr1 is KAndExpr) { + condition = mkAnd(expr1.args[0], condition) + expr1 = expr1.args[1].uncheckedCast() + } + val lessOrEqual = mkBvUnsignedLessOrEqualExpr(expr0, expr1) + val newInequality: KExpr = if (condition is KTrue) lessOrEqual else + mkIte(condition, mkFalse().uncheckedCast(), lessOrEqual) + return newInequality + } + fun orderInequalities(permutation: List>): Array> { var orderedInequalities = arrayOf>() @@ -122,8 +142,8 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): if (i % 2 == 0) lastExpr = expr else { - val lessOrEqual = mkBvSignedLessOrEqualExpr(lastExpr, expr) - orderedInequalities += lessOrEqual + val newInequality = createInequality(lastExpr, expr) + orderedInequalities += newInequality } } } @@ -176,7 +196,7 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): result = if (leP.isEmpty() or geP.isEmpty()) mkAnd(*orderedLe, *orderedGe, *freeSet) else { - val middleLe = mkBvUnsignedLessOrEqualExpr(leP[leP.lastIndex], geP[0]) + val middleLe = createInequality(leP[leP.lastIndex], geP[0]) mkAnd(*orderedLe, *orderedGe, middleLe, *freeSet) } } @@ -211,16 +231,19 @@ fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): return if (expr is KNotExpr) { val condition = mkBvUnsignedLessExpr(curExpr.arg0, bvOneExpr) val falseBranch = mkBvSubExpr(curExpr.arg0, bvOneExpr) - val newFreeSubExpr = mkIte(condition, mkFalse().uncheckedCast(), falseBranch) + val newFreeSubExpr = mkAnd(condition, falseBranch.uncheckedCast(), order = false) true to newFreeSubExpr // bvult } else false to curExpr.arg0 // bvuge } return if (expr is KNotExpr) { - val condition: KExpr = (curExpr.arg1 == BvConstants.bvMaxValueUnsigned).uncheckedCast() + val condition: KExpr = mkBvUnsignedGreaterOrEqualExpr( + curExpr.arg1, + BvConstants.bvMaxValueUnsigned.uncheckedCast() + ) val falseBranch = mkBvAddExpr(curExpr.arg1, bvOneExpr) - val newFreeSubExpr = mkIte(condition, BvConstants.bvZero.uncheckedCast(), falseBranch) + val newFreeSubExpr = mkAnd(condition, falseBranch.uncheckedCast(), order = false) false to newFreeSubExpr // bvugt } else diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index b45d91afc..54a335e71 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -5,93 +5,126 @@ import io.ksmt.solver.z3.KZ3SMTLibParser import kotlin.test.Test class BvQETest { - private val ctx = KContext() + class LinearTestsWithoutLinearCoefficients { + private val ctx = KContext() - @Test - fun linTestWithoutLinCoef0() { - val formula = - """ + @Test + fun xLessOrEqualY() { + val formula = + """ (declare-fun y () (_ BitVec 4)) - (assert (exists ((x (_ BitVec 4))) (bvule x y))) + (assert (exists ((x (_ BitVec 4))) (bvule x y))) """ - val assertions = KZ3SMTLibParser(ctx).parse(formula) - println(assertions) - val qfAssertions = quantifierElimination(ctx, assertions) - println(qfAssertions) - } + val assertions = KZ3SMTLibParser(ctx).parse(formula) + println(assertions) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } - @Test - fun linTestWithoutLinCoef1() { - val formula = + @Test + fun xLessOrEqualZero() { + val formula = + """ + (assert (exists ((x (_ BitVec 4))) (bvult x #b0000))) """ - (assert (exists ((x (_ BitVec 4))) (bvult x #b0000))) - """ - val assertions = KZ3SMTLibParser(ctx).parse(formula) - println(assertions) - val qfAssertions = quantifierElimination(ctx, assertions) - println(qfAssertions) - } + val assertions = KZ3SMTLibParser(ctx).parse(formula) + println(assertions) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } - @Test - fun linTestWithoutLinCoef2() { - val formula = + @Test + fun xLessOrEqualOne() { + val formula = + """ + (assert (exists ((x (_ BitVec 4))) (bvult x #b0001))) """ - (assert (exists ((x (_ BitVec 4))) (bvult x #b0001))) - """ - val assertions = KZ3SMTLibParser(ctx).parse(formula) - println(assertions) - val qfAssertions = quantifierElimination(ctx, assertions) - println(qfAssertions) - } + val assertions = KZ3SMTLibParser(ctx).parse(formula) + println(assertions) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } - @Test - fun linTestWithoutLinCoef3() { - val formula = - """ + @Test + fun regularTest0() { + val formula = + """ (declare-fun y () (_ BitVec 4)) - (assert (exists ((x (_ BitVec 4))) (and (bvule x y) (bvuge x #b0010)))) - (assert (bvule y #b1000)) + (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) - } + val assertions = KZ3SMTLibParser(ctx).parse(formula) + println(assertions) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } - @Test - fun linTestWithoutLinCoef4() { - val formula = + @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) + } + + @Test + fun notExistsTest() { + val formula = + """ (declare-fun y () (_ BitVec 4)) - (assert (exists ((x (_ BitVec 4))) (and (bvult x y) (bvule y #b0000)))) + (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) + val assertions = KZ3SMTLibParser(ctx).parse(formula) + println(assertions) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } } - @Test - fun linTest0() { - val formula = - """ + class LinearTests { + private val ctx = KContext() + + @Test + fun linTest0() { + 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))) (bvult (bvmul x #b0111) y))) + (assert (bvult (bvnot y) #b1000)) """ - val assertions = KZ3SMTLibParser(ctx).parse(formula) - val qfAssertions = quantifierElimination(ctx, assertions) - println(qfAssertions) + val assertions = KZ3SMTLibParser(ctx).parse(formula) + val qfAssertions = quantifierElimination(ctx, assertions) + println(qfAssertions) + } } - @Test - fun expTest() { - val formula = - """ + class ExponentialTests { + private val ctx = KContext() + + @Test + fun expTest() { + 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) + val assertions = KZ3SMTLibParser(ctx).parse(formula) + quantifierElimination(ctx, assertions) + } } } \ No newline at end of file From 332d5f57b29fa86fe94219097397d4ee5c32503a Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Wed, 13 Sep 2023 15:52:28 +0300 Subject: [PATCH 05/10] Add QE result check and fix some problems --- .../simplify/BvQuantifierElimination.kt | 38 +++++++++++-------- .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 30 +++++++++++++++ 2 files changed, 52 insertions(+), 16 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index 7d52a3a5f..4147986c4 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -114,7 +114,8 @@ fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr, bound: KDecl<*>): KExpr = with(ctx) { - fun createInequality(lessExpr: KExpr, greaterExpr: KExpr): KExpr { + fun createInequality(lessExpr: KExpr, greaterExpr: KExpr?): + KExpr { var condition: KExpr = mkTrue() var expr0 = lessExpr if (expr0 is KAndExpr) { @@ -126,18 +127,20 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): condition = mkAnd(expr1.args[0], condition) expr1 = expr1.args[1].uncheckedCast() } - val lessOrEqual = mkBvUnsignedLessOrEqualExpr(expr0, expr1) + val lessOrEqual = if (expr1 == null) mkTrue() else mkBvUnsignedLessOrEqualExpr(expr0, expr1) val newInequality: KExpr = if (condition is KTrue) lessOrEqual else mkIte(condition, mkFalse().uncheckedCast(), lessOrEqual) return newInequality } - fun orderInequalities(permutation: List>): Array> - { + fun orderInequalities(permutation: List>): + Array> { var orderedInequalities = arrayOf>() if (permutation.isNotEmpty()) { var lastExpr = permutation[0] + if (permutation.size == 1) + orderedInequalities += createInequality(lastExpr, null) for ((i, expr) in permutation.withIndex()) { if (i % 2 == 0) lastExpr = expr @@ -155,6 +158,7 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): if (coefficientExpressions.isNotEmpty()) TODO() var result: KExpr = KFalse(ctx) + var orList = arrayOf>() when (body) { is KAndExpr, is KNotExpr, is KBvUnsignedLessOrEqualExpr<*> -> { @@ -167,15 +171,15 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): } while (args.isNotEmpty()) { val expr = args[0] - val (isLe, freeSubExpr) = getFreeSubExpr(ctx, expr, bound) - if (isLe == null) { + val (freeSubExpr, isLess) = getFreeSubExpr(ctx, expr, bound) + if (isLess == null) { when (freeSubExpr) { null -> freeSet += expr is KAndExpr -> args += freeSubExpr.args } } - else if (isLe) + else if (isLess) leSet.add(freeSubExpr!!) else geSet.add(freeSubExpr!!) @@ -193,14 +197,16 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): geP as List> val orderedGe = orderInequalities(geP) - result = if (leP.isEmpty() or geP.isEmpty()) - mkAnd(*orderedLe, *orderedGe, *freeSet) + orList += if (leP.isEmpty() or geP.isEmpty()) + mkAnd(*orderedLe, *orderedGe) else { val middleLe = createInequality(leP[leP.lastIndex], geP[0]) - mkAnd(*orderedLe, *orderedGe, middleLe, *freeSet) + mkAnd(*orderedLe, *orderedGe, middleLe) } } } + result = mkOr(*orList) + result = mkAnd(result, *freeSet) } else -> assert(false) { "Expression ${body}:${body.javaClass.typeName} " + "is not in required form." } @@ -209,10 +215,10 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): } fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): - Pair?> = with(ctx) { + Pair?, Boolean?> = with(ctx) { val curExpr = if (expr is KNotExpr) expr.arg else expr if (curExpr is KAndExpr) - return null to expr + return expr to null else if (curExpr !is KBvUnsignedLessOrEqualExpr<*>) assert(false) { "Expression ${curExpr}:${curExpr.javaClass.typeName} " + "is not in required form." } @@ -232,10 +238,10 @@ fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): val condition = mkBvUnsignedLessExpr(curExpr.arg0, bvOneExpr) val falseBranch = mkBvSubExpr(curExpr.arg0, bvOneExpr) val newFreeSubExpr = mkAnd(condition, falseBranch.uncheckedCast(), order = false) - true to newFreeSubExpr // bvult + newFreeSubExpr to false // bvult } else - false to curExpr.arg0 // bvuge + curExpr.arg0 to true // bvuge } return if (expr is KNotExpr) { val condition: KExpr = mkBvUnsignedGreaterOrEqualExpr( @@ -244,10 +250,10 @@ fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): ) val falseBranch = mkBvAddExpr(curExpr.arg1, bvOneExpr) val newFreeSubExpr = mkAnd(condition, falseBranch.uncheckedCast(), order = false) - false to newFreeSubExpr // bvugt + newFreeSubExpr to true // bvugt } else - true to curExpr.arg1 // bvule + curExpr.arg1 to false // bvule } fun sameDecl(expr: KExpr<*>, bound: KDecl<*>): Boolean = diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index 54a335e71..9f9e0ba1e 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -1,9 +1,33 @@ 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>, + quantifierFreeAssertions: List>): + 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) { + println(solver.model()) + return false + } + } + return true +} + class BvQETest { class LinearTestsWithoutLinearCoefficients { private val ctx = KContext() @@ -19,6 +43,7 @@ class BvQETest { println(assertions) val qfAssertions = quantifierElimination(ctx, assertions) println(qfAssertions) + assert(xorEquivalenceCheck(ctx, assertions, qfAssertions)) } @Test @@ -31,6 +56,7 @@ class BvQETest { println(assertions) val qfAssertions = quantifierElimination(ctx, assertions) println(qfAssertions) + assert(xorEquivalenceCheck(ctx, assertions, qfAssertions)) } @Test @@ -43,6 +69,7 @@ class BvQETest { println(assertions) val qfAssertions = quantifierElimination(ctx, assertions) println(qfAssertions) + assert(xorEquivalenceCheck(ctx, assertions, qfAssertions)) } @Test @@ -57,6 +84,7 @@ class BvQETest { println(assertions) val qfAssertions = quantifierElimination(ctx, assertions) println(qfAssertions) + assert(xorEquivalenceCheck(ctx, assertions, qfAssertions)) } @Test @@ -80,6 +108,7 @@ class BvQETest { println(assertions) val qfAssertions = quantifierElimination(ctx, assertions) println(qfAssertions) + assert(xorEquivalenceCheck(ctx, assertions, qfAssertions)) } @Test @@ -93,6 +122,7 @@ class BvQETest { println(assertions) val qfAssertions = quantifierElimination(ctx, assertions) println(qfAssertions) + assert(xorEquivalenceCheck(ctx, assertions, qfAssertions)) } } From ba34becfece13a65c1d5161c8f17515c52ffca28 Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Tue, 19 Sep 2023 16:18:19 +0300 Subject: [PATCH 06/10] Fix some problems in QE for BV theory --- .../simplify/BvQuantifierElimination.kt | 44 +++++++-------- .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 53 ++++++++++++++++++- 2 files changed, 74 insertions(+), 23 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index 4147986c4..ec5b69287 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -116,19 +116,22 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): fun createInequality(lessExpr: KExpr, greaterExpr: KExpr?): KExpr { - var condition: KExpr = mkTrue() - var expr0 = lessExpr - if (expr0 is KAndExpr) { - condition = expr0.args[0] - expr0 = expr0.args[1].uncheckedCast() - } - var expr1 = greaterExpr - if (expr1 is KAndExpr) { - condition = mkAnd(expr1.args[0], condition) - expr1 = expr1.args[1].uncheckedCast() - } - val lessOrEqual = if (expr1 == null) mkTrue() else mkBvUnsignedLessOrEqualExpr(expr0, expr1) - val newInequality: KExpr = if (condition is KTrue) lessOrEqual else + var condition: KExpr = mkFalse() + var conditionChanged = false + val argList = mutableListOf>() + + for (item in mutableListOf(lessExpr, greaterExpr ?: BvConstants.bvMaxValueUnsigned)) + if (item is KAndExpr) { + condition = mkOr(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 = if (!conditionChanged) lessOrEqual else mkIte(condition, mkFalse().uncheckedCast(), lessOrEqual) return newInequality } @@ -141,13 +144,10 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): var lastExpr = permutation[0] if (permutation.size == 1) orderedInequalities += createInequality(lastExpr, null) - for ((i, expr) in permutation.withIndex()) { - if (i % 2 == 0) - lastExpr = expr - else { - val newInequality = createInequality(lastExpr, expr) - orderedInequalities += newInequality - } + for (expr in permutation) { + val newInequality = createInequality(lastExpr, expr) + orderedInequalities += newInequality + lastExpr = expr } } return orderedInequalities @@ -237,7 +237,7 @@ fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): return if (expr is KNotExpr) { val condition = mkBvUnsignedLessExpr(curExpr.arg0, bvOneExpr) val falseBranch = mkBvSubExpr(curExpr.arg0, bvOneExpr) - val newFreeSubExpr = mkAnd(condition, falseBranch.uncheckedCast(), order = false) + val newFreeSubExpr = mkAndNoSimplify(condition, falseBranch.uncheckedCast()) newFreeSubExpr to false // bvult } else @@ -249,7 +249,7 @@ fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): BvConstants.bvMaxValueUnsigned.uncheckedCast() ) val falseBranch = mkBvAddExpr(curExpr.arg1, bvOneExpr) - val newFreeSubExpr = mkAnd(condition, falseBranch.uncheckedCast(), order = false) + val newFreeSubExpr = mkAndNoSimplify(condition, falseBranch.uncheckedCast()) newFreeSubExpr to true // bvugt } else diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index 9f9e0ba1e..5c0924e43 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -21,7 +21,7 @@ fun xorEquivalenceCheck(ctx: KContext, solver.assert(xorExpr) val status = solver.check() if (status == KSolverStatus.SAT) { - println(solver.model()) + print("\n${solver.model()}\n") return false } } @@ -87,6 +87,57 @@ class BvQETest { assert(xorEquivalenceCheck(ctx, assertions, qfAssertions)) } + @Test + fun regularTest1() { + 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 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 = From eef876f0724f1a4f3ff1067816901e0c7a4af4a3 Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Wed, 18 Oct 2023 16:52:57 +0300 Subject: [PATCH 07/10] bit-vector QE when all bound terms have the same linear coefficient --- .../io/ksmt/expr/rewrite/KBvQETransformer.kt | 21 ++--- .../simplify/BvQuantifierElimination.kt | 77 ++++++++++------- .../utils/BvQuantifierEliminationUtils.kt | 65 +++++++++++++++ .../main/kotlin/io/ksmt/utils/Permutations.kt | 21 ----- .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 82 ++++++++++++++++--- 5 files changed, 191 insertions(+), 75 deletions(-) create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/utils/BvQuantifierEliminationUtils.kt delete mode 100644 ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt index f9c848380..98d1d1c6b 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt +++ b/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) : KNonRecursiveTransformer(ctx) { private var bounds = mutableListOf>() private var newBody: KExpr = ctx.mkTrue() -// // bool transformers -// override fun transform(expr: KAndExpr): KExpr { -// } -// -// override fun transform(expr: KAndBinaryExpr): KExpr { -// } + override fun transform(expr: KBvMulExpr): + KExpr = with(ctx) { + return mkBvMulNoOverflowExpr(expr.arg0, expr.arg1, isSigned = false).uncheckedCast() + } + + override fun transform(expr: KEqExpr): KExpr = with(ctx) { @@ -34,14 +35,6 @@ class KBvQETransformer(ctx: KContext, bound: KDecl) : KNonRecursiveTran { l, r -> eqToAndNoSimplify(l, r) } } -// override fun transform(expr: KNotExpr): KExpr { -// } - -// // bit-vec expressions transformers -// override fun transform(expr: KBvUnsignedLessOrEqualExpr): KExpr { -// -// } - companion object { fun transformBody(body: KExpr, bound: KDecl): Pair, List>> = with(KBvQETransformer(body.ctx, bound)) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index ec5b69287..064de30a1 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/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, bound: KDecl<*>) : Pair, List>?> { - // 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, bound: KDecl<*>): return orderedInequalities } + fun sameCoefficients(coefficientExpressions: Set>): 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 = KFalse(ctx) var orList = arrayOf>() @@ -197,11 +214,34 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): geP as List> val orderedGe = orderInequalities(geP) + var coefficientExpr: KExpr = mkTrue() + if (coefficient != null) { + var addNotOverflow: KExpr = mkTrue() + var isNextLess: KExpr = mkTrue() + var remainderIsZero: KExpr = mkTrue() + var nextMultiple: KExpr = 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 -} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/BvQuantifierEliminationUtils.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/BvQuantifierEliminationUtils.kt new file mode 100644 index 000000000..607c8e385 --- /dev/null +++ b/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 getPermutations(set: Set): Set> { + fun allPermutations(list: List): Set> { + val result: MutableSet> = 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?> +{ + 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 +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt deleted file mode 100644 index 99ceff18f..000000000 --- a/ksmt-core/src/main/kotlin/io/ksmt/utils/Permutations.kt +++ /dev/null @@ -1,21 +0,0 @@ -package io.ksmt.utils - -object Permutations { - - fun getPermutations(set: Set): Set> { - fun allPermutations(list: List): Set> { - val result: MutableSet> = 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()) - } -} \ No newline at end of file diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index 5c0924e43..4d3c42297 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/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 { From 51a28947964bec1228cd762765729e0d318fc572 Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Fri, 27 Oct 2023 09:35:50 +0300 Subject: [PATCH 08/10] small change in file of QE for BV theory --- .../io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index 064de30a1..c05a46778 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -11,7 +11,6 @@ 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.isBvZero object BvConstants { var bvSize = 0u @@ -72,7 +71,7 @@ fun prepareQuantifier(ctx: KContext, assertion: KQuantifier): return quantifierAssertion to isUniversal } -// p.5, 1st and 2nd steps +// 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, bound: KDecl<*>) : Pair, List>?> { val collector = KExprCollector From 02ab33e3ca8e1d72b57e4c9b22f0e3b2a67cb6a6 Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Tue, 7 Nov 2023 20:30:06 +0300 Subject: [PATCH 09/10] bit-vector QE when bound terms have different linear coefficients --- .../io/ksmt/expr/rewrite/KBvQETransformer.kt | 7 - .../simplify/BvQuantifierElimination.kt | 200 ++++++++++-------- .../utils/BvQuantifierEliminationUtils.kt | 36 +++- .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 32 ++- 4 files changed, 169 insertions(+), 106 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt index 98d1d1c6b..d1f159f3c 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/KBvQETransformer.kt @@ -14,13 +14,6 @@ class KBvQETransformer(ctx: KContext, bound: KDecl) : KNonRecursiveTran private var bounds = mutableListOf>() private var newBody: KExpr = ctx.mkTrue() - override fun transform(expr: KBvMulExpr): - KExpr = with(ctx) { - return mkBvMulNoOverflowExpr(expr.arg0, expr.arg1, isSigned = false).uncheckedCast() - } - - - override fun transform(expr: KEqExpr): KExpr = with(ctx) { fun eqToAndNoSimplify(l: KExpr, r: KExpr): KExpr = diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index c05a46778..e3a6ae63b 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -11,6 +11,7 @@ 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 @@ -104,7 +105,6 @@ fun qeProcess(ctx: KContext, assertion: KExistentialQuantifier): KExpr, bound: KDecl<*>): fun createInequality(lessExpr: KExpr, greaterExpr: KExpr?): KExpr { - var condition: KExpr = mkFalse() + var condition: KExpr = mkTrue() var conditionChanged = false val argList = mutableListOf>() - for (item in mutableListOf(lessExpr, greaterExpr ?: BvConstants.bvMaxValueUnsigned)) + for (item in mutableListOf(lessExpr, greaterExpr ?: BvConstants.bvMaxValueUnsigned)) { if (item is KAndExpr) { - condition = mkOr(item.args[0], condition) + condition = mkAnd(item.args[0], condition) conditionChanged = true argList.add(item.args[1].uncheckedCast()) - } - else { + } else { argList.add(item.uncheckedCast()) } + } val lessOrEqual = mkBvUnsignedLessOrEqualExpr(argList[0], argList[1]) val newInequality: KExpr = if (!conditionChanged) lessOrEqual else - mkIte(condition, mkFalse().uncheckedCast(), lessOrEqual) + mkAnd(condition, lessOrEqual) return newInequality } @@ -141,7 +141,7 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): if (permutation.isNotEmpty()) { var lastExpr = permutation[0] if (permutation.size == 1) - orderedInequalities += createInequality(lastExpr, null) + return arrayOf(createInequality(lastExpr, null)) for (expr in permutation) { val newInequality = createInequality(lastExpr, expr) orderedInequalities += newInequality @@ -151,106 +151,124 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): return orderedInequalities } - fun sameCoefficients(coefficientExpressions: Set>): 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 + fun getOneCoefficientExpressions(coefficientExpressions: MutableSet>, coefficient: KBitVecValue<*>?): + MutableSet> { + val resultSet = mutableSetOf>() + for (expr in coefficientExpressions) { + val (isLinear, coef) = hasLinearCoefficient(this, bound, expr) + if (isLinear && coefficient == coef) + resultSet.add(expr) } - return true - } - - val coefficientExpressions = KExprCollector.collectDeclarations(body) { expr -> - hasLinearCoefficient(bound, expr).first } - var coefficient: KBitVecValue<*>? = null - if (coefficientExpressions.isNotEmpty()) { - if (sameCoefficients(coefficientExpressions)) - coefficient = hasLinearCoefficient(bound, coefficientExpressions.first()).second - else - TODO() + return resultSet } - var result: KExpr = KFalse(ctx) - var orList = arrayOf>() + var resultArray = arrayOf>() when (body) { is KAndExpr, is KNotExpr, is KBvUnsignedLessOrEqualExpr<*> -> { val leSet = mutableSetOf>() val geSet = mutableSetOf>() - var freeSet = arrayOf>() - val args: MutableList> = when(body) { + var freeArray = arrayOf>() + + val bodyArgs: MutableList> = when (body) { is KAndExpr -> body.args.toMutableList() else -> mutableListOf(body) } - while (args.isNotEmpty()) { - val expr = args[0] - val (freeSubExpr, isLess) = getFreeSubExpr(ctx, expr, bound) + val bodyArgMap = mutableMapOf, Pair?, Boolean?>>() + while (bodyArgs.isNotEmpty()) { + val curExpr = bodyArgs[0] + val (freeSubExpr, isLess) = getFreeSubExpr(ctx, curExpr, bound) if (isLess == null) { - when (freeSubExpr) - { - null -> freeSet += expr - is KAndExpr -> args += freeSubExpr.args + when (freeSubExpr) { + null -> freeArray += curExpr as KExpr + is KAndExpr -> bodyArgs += freeSubExpr.args } } - else if (isLess) - leSet.add(freeSubExpr!!) else - geSet.add(freeSubExpr!!) - args.removeFirst() + bodyArgMap[curExpr] = freeSubExpr to isLess + bodyArgs.removeFirst() } - val lePermutations = Permutations.getPermutations(leSet) - val gePermutations = Permutations.getPermutations(geSet) - for (leP in lePermutations) { - @Suppress("UNCHECKED_CAST") - leP as List> - val orderedLe = orderInequalities(leP) - - for (geP in gePermutations) { + + while (bodyArgMap.isNotEmpty()){ + val bodyArg = bodyArgMap.keys.first() + val coefficient = hasLinearCoefficient(this, bound, bodyArg).second + val oneCoefExprSet = getOneCoefficientExpressions(bodyArgMap.keys, coefficient) + 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>() + + for (leP in lePermutations) { @Suppress("UNCHECKED_CAST") - geP as List> - val orderedGe = orderInequalities(geP) - - var coefficientExpr: KExpr = mkTrue() - if (coefficient != null) { - var addNotOverflow: KExpr = mkTrue() - var isNextLess: KExpr = mkTrue() - var remainderIsZero: KExpr = mkTrue() - var nextMultiple: KExpr = 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]) + leP as List> + val orderedLe = orderInequalities(leP) - coefficientExpr = mkAnd(isNextLess, mkOr(addNotOverflow, remainderIsZero)) - } + for (geP in gePermutations) { + @Suppress("UNCHECKED_CAST") + geP as List> + val orderedGe = orderInequalities(geP) + + var coefficientExpr: KExpr = mkTrue() + if (!coefficient!!.isBvOne()) { + var addNotOverflow: KExpr = mkTrue() + var isNextLess: KExpr = mkTrue() + var remainderIsZero: KExpr = mkTrue() + var nextMultiple: KExpr = BvConstants.bvZero.uncheckedCast() + + var withOverflowCheck: KExpr = 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]) + } - 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) + 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) + } + if (geP.isNotEmpty()) { + val initFstGe = geP[0] + var fstGe = initFstGe + if (initFstGe is KAndExpr) { + fstGe = initFstGe.args[1].uncheckedCast() + withOverflowCheck = mkAnd(withOverflowCheck, initFstGe.args[0]) + } + isNextLess = mkBvUnsignedLessExpr(nextMultiple, fstGe) + } + 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), *freeArray) } - result = mkOr(*orList) - result = mkAnd(result, *freeSet) } - else -> assert(false) { "Expression ${body}:${body.javaClass.typeName} " + - "is not in required form." } + else -> assert(false) { + "Expression ${body}:${body.javaClass.typeName} " + + "is not in required form." + } } - return result + return mkAnd(*resultArray) } fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): @@ -274,21 +292,21 @@ fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): if (boundExpressions.isEmpty()) return null to null // return if (expr is KNotExpr) { - val condition = mkBvUnsignedLessExpr(curExpr.arg0, bvOneExpr) - val falseBranch = mkBvSubExpr(curExpr.arg0, bvOneExpr) - val newFreeSubExpr = mkAndNoSimplify(condition, falseBranch.uncheckedCast()) + 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 = mkBvUnsignedGreaterOrEqualExpr( + val condition: KExpr = mkBvUnsignedLessExpr( curExpr.arg1, BvConstants.bvMaxValueUnsigned.uncheckedCast() ) - val falseBranch = mkBvAddExpr(curExpr.arg1, bvOneExpr) - val newFreeSubExpr = mkAndNoSimplify(condition, falseBranch.uncheckedCast()) + val trueBranch = mkBvAddExpr(curExpr.arg1, bvOneExpr) + val newFreeSubExpr = mkAndNoSimplify(condition, trueBranch.uncheckedCast()) newFreeSubExpr to true // bvugt } else diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/BvQuantifierEliminationUtils.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/BvQuantifierEliminationUtils.kt index 607c8e385..a2661d1af 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/utils/BvQuantifierEliminationUtils.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/BvQuantifierEliminationUtils.kt @@ -3,7 +3,11 @@ 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 @@ -39,19 +43,37 @@ fun sameDecl(expr: KExpr<*>, bound: KDecl<*>): Boolean = fun occursInExponentialExpression(bound: KDecl<*>, assertion: KExpr<*>): Boolean = assertion is KBvShiftLeftExpr<*> && sameDecl(assertion.shift, bound) -fun hasLinearCoefficient(bound: KDecl<*>, assertion: KExpr<*>): Pair?> +fun hasLinearCoefficient(ctx: KContext, bound: KDecl<*>, assertion: KExpr<*>): Pair?> { + 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(BvConstants.bvSize) + else + false to null + } + val arg0: KExpr<*> val arg1: KExpr<*> - when (assertion) { + when (mulTerm) { is KBvMulExpr<*> -> { - arg0 = assertion.arg0 - arg1 = assertion.arg1 + arg0 = mulTerm.arg0 + arg1 = mulTerm.arg1 } is KBvMulNoOverflowExpr<*> -> { - arg0 = assertion.arg0 - arg1 = assertion.arg1 + arg0 = mulTerm.arg0 + arg1 = mulTerm.arg1 } else -> return false to null @@ -59,7 +81,7 @@ fun hasLinearCoefficient(bound: KDecl<*>, assertion: KExpr<*>): Pair && !coef.isBvOne()) + if (coef is KBitVecValue<*>) return true to coef return false to null } diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index 4d3c42297..a4cb7b359 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -250,13 +250,43 @@ class BvQETest { 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 test() { + 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 expTest() { + fun test() { val formula = """ (declare-fun y () (_ BitVec 4)) From 212fd7b698cd75cbee1fb6b91e876d039529b4b9 Mon Sep 17 00:00:00 2001 From: AnzhelaSukhanova Date: Thu, 9 Nov 2023 12:16:53 +0300 Subject: [PATCH 10/10] correct bit-vector QE --- .../simplify/BvQuantifierElimination.kt | 17 ++++++++--------- .../io/ksmt/expr/rewrite/simplify/BvQETest.kt | 18 +++++++++++++++++- 2 files changed, 25 insertions(+), 10 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt index e3a6ae63b..48673e119 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvQuantifierElimination.kt @@ -163,12 +163,9 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): } var resultArray = arrayOf>() + var freeArray = arrayOf>() when (body) { is KAndExpr, is KNotExpr, is KBvUnsignedLessOrEqualExpr<*> -> { - val leSet = mutableSetOf>() - val geSet = mutableSetOf>() - var freeArray = arrayOf>() - val bodyArgs: MutableList> = when (body) { is KAndExpr -> body.args.toMutableList() else -> mutableListOf(body) @@ -192,6 +189,9 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): val bodyArg = bodyArgMap.keys.first() val coefficient = hasLinearCoefficient(this, bound, bodyArg).second val oneCoefExprSet = getOneCoefficientExpressions(bodyArgMap.keys, coefficient) + + val leSet = mutableSetOf>() + val geSet = mutableSetOf>() for (curExpr in oneCoefExprSet) { val (freeSubExpr, isLess) = bodyArgMap[curExpr]!! if (isLess!!) @@ -218,7 +218,6 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): var coefficientExpr: KExpr = mkTrue() if (!coefficient!!.isBvOne()) { var addNotOverflow: KExpr = mkTrue() - var isNextLess: KExpr = mkTrue() var remainderIsZero: KExpr = mkTrue() var nextMultiple: KExpr = BvConstants.bvZero.uncheckedCast() @@ -241,15 +240,15 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): addNotOverflow = mkBvAddNoOverflowExpr(lastLe, gcdMinusRemainder, false) nextMultiple = mkBvAddExpr(lastLe, gcdMinusRemainder) } + var fstGe = BvConstants.bvMaxValueUnsigned if (geP.isNotEmpty()) { val initFstGe = geP[0] - var fstGe = initFstGe if (initFstGe is KAndExpr) { fstGe = initFstGe.args[1].uncheckedCast() withOverflowCheck = mkAnd(withOverflowCheck, initFstGe.args[0]) } - isNextLess = mkBvUnsignedLessExpr(nextMultiple, fstGe) } + val isNextLess = mkBvUnsignedLessExpr(nextMultiple, fstGe.uncheckedCast()) coefficientExpr = mkAnd(withOverflowCheck, isNextLess, mkOr(addNotOverflow, remainderIsZero)) } orList += if (leP.isEmpty() or geP.isEmpty()) @@ -260,7 +259,7 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): } } } - resultArray += mkAnd(mkOr(*orList), *freeArray) + resultArray += mkAnd(mkOr(*orList)) } } else -> assert(false) { @@ -268,7 +267,7 @@ fun linearQE(ctx: KContext, body: KExpr, bound: KDecl<*>): "is not in required form." } } - return mkAnd(*resultArray) + return mkAnd(*resultArray, *freeArray) } fun getFreeSubExpr(ctx: KContext, expr: KExpr<*>, bound: KDecl<*>): diff --git a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt index a4cb7b359..cbbd4bb4e 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/expr/rewrite/simplify/BvQETest.kt @@ -266,7 +266,23 @@ class BvQETest { } @Test - fun 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))