Expression arguments ordering (#89)

* Parametrized and/or simplifiers * Arguments ordering option for AND,OR,EQ,DISTINCT * Version up (0.4.5)
UnitTestBot · Mar 27, 2023 · 5eb06c6 · 5eb06c6
1 parent 4cddd01
commit 5eb06c6
Show file tree

Hide file tree

Showing 15 changed files with 306 additions and 149 deletions.
diff --git a/README.md b/README.md
@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.4")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
 ```
 
 ## Usage

diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
@@ -9,7 +9,7 @@ plugins {
 }
 
 group = "org.ksmt"
-version = "0.4.4"
+version = "0.4.5"
 
 repositories {
     mavenCentral()

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -18,17 +18,17 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.4")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")    
 }
 ```
 
 #### 3. Add one or more SMT solver dependencies:
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.5")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 

diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
@@ -10,9 +10,9 @@ repositories {
 
 dependencies {
     // core
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
 }
 
 java {

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
@@ -291,7 +291,6 @@ import org.ksmt.expr.KUnaryMinusArithExpr
 import org.ksmt.expr.KUniversalQuantifier
 import org.ksmt.expr.KXorExpr
 import org.ksmt.expr.rewrite.simplify.simplifyAnd
-import org.ksmt.expr.rewrite.simplify.simplifyAndNoFlat
 import org.ksmt.expr.rewrite.simplify.simplifyArithAdd
 import org.ksmt.expr.rewrite.simplify.simplifyArithDiv
 import org.ksmt.expr.rewrite.simplify.simplifyArithGe
@@ -392,7 +391,6 @@ import org.ksmt.expr.rewrite.simplify.simplifyIntToReal
 import org.ksmt.expr.rewrite.simplify.simplifyIte
 import org.ksmt.expr.rewrite.simplify.simplifyNot
 import org.ksmt.expr.rewrite.simplify.simplifyOr
-import org.ksmt.expr.rewrite.simplify.simplifyOrNoFlat
 import org.ksmt.expr.rewrite.simplify.simplifyRealIsInt
 import org.ksmt.expr.rewrite.simplify.simplifyRealToFpExpr
 import org.ksmt.expr.rewrite.simplify.simplifyRealToInt
@@ -666,17 +664,56 @@ open class KContext(
     private val andNaryCache = mkAstInterner<KAndNaryExpr>()
     private val andBinaryCache = mkAstInterner<KAndBinaryExpr>()
 
-    open fun mkAnd(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyAnd, ::mkAndNoSimplify)
+    /**
+     * Create boolean AND expression.
+     *
+     * @param flat flat nested AND expressions
+     * @param order reorder arguments to ensure that (and a b) == (and b a)
+     * */
+    @JvmOverloads
+    open fun mkAnd(
+        args: List<KExpr<KBoolSort>>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        args,
+        simplifier = { exprArgs -> simplifyAnd(exprArgs, flat, order) },
+        createNoSimplify = ::mkAndNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkAnd(args, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkAndNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyAndNoFlat, ::mkAndNoSimplify)
+        mkAnd(args, flat = false)
 
-    open fun mkAnd(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyAnd, ::mkAndNoSimplify)
+    /**
+     * Create boolean binary AND expression.
+     *
+     * @param flat flat nested AND expressions
+     * @param order reorder arguments to ensure that (and a b) == (and b a)
+     * */
+    @JvmOverloads
+    open fun mkAnd(
+        lhs: KExpr<KBoolSort>,
+        rhs: KExpr<KBoolSort>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        lhs, rhs,
+        simplifier = { a, b -> simplifyAnd(a, b, flat, order) },
+        createNoSimplify = ::mkAndNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkAnd(lhs, rhs, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkAndNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyAndNoFlat, ::mkAndNoSimplify)
+        mkAnd(lhs, rhs, flat = false)
 
     open fun mkAndNoSimplify(args: List<KExpr<KBoolSort>>): KAndExpr =
         if (args.size == 2) {
@@ -697,17 +734,56 @@ open class KContext(
     private val orNaryCache = mkAstInterner<KOrNaryExpr>()
     private val orBinaryCache = mkAstInterner<KOrBinaryExpr>()
 
-    open fun mkOr(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyOr, ::mkOrNoSimplify)
+    /**
+     * Create boolean OR expression.
+     *
+     * @param flat flat nested OR expressions
+     * @param order reorder arguments to ensure that (or a b) == (or b a)
+     * */
+    @JvmOverloads
+    open fun mkOr(
+        args: List<KExpr<KBoolSort>>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        args,
+        simplifier = { exprArgs -> simplifyOr(exprArgs, flat, order) },
+        createNoSimplify = ::mkOrNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkOr(args, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkOrNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyOrNoFlat, ::mkOrNoSimplify)
+        mkOr(args, flat = false)
 
-    open fun mkOr(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyOr, ::mkOrNoSimplify)
+    /**
+     * Create boolean binary OR expression.
+     *
+     * @param flat flat nested OR expressions
+     * @param order reorder arguments to ensure that (or a b) == (or b a)
+     * */
+    @JvmOverloads
+    open fun mkOr(
+        lhs: KExpr<KBoolSort>,
+        rhs: KExpr<KBoolSort>,
+        flat: Boolean = true,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        lhs, rhs,
+        simplifier = { a, b -> simplifyOr(a, b, flat, order) },
+        createNoSimplify = ::mkOrNoSimplify
+    )
 
+    @Deprecated(
+        "NoFlat builders are deprecated",
+        replaceWith = ReplaceWith("mkOr(lhs, rhs, flat = false)"),
+        level = DeprecationLevel.ERROR
+    )
     open fun mkOrNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyOrNoFlat, ::mkOrNoSimplify)
+        mkOr(lhs, rhs, flat = false)
 
     open fun mkOrNoSimplify(args: List<KExpr<KBoolSort>>): KOrExpr =
         if (args.size == 2) {
@@ -767,8 +843,21 @@ open class KContext(
 
     private val eqCache = mkAstInterner<KEqExpr<out KSort>>()
 
-    open fun <T : KSort> mkEq(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort> =
-        mkSimplified(lhs, rhs, KContext::simplifyEq, ::mkEqNoSimplify)
+    /**
+     * Create EQ expression.
+     *
+     * @param order reorder arguments to ensure that (= a b) == (= b a)
+     * */
+    @JvmOverloads
+    open fun <T : KSort> mkEq(
+        lhs: KExpr<T>,
+        rhs: KExpr<T>,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        lhs, rhs,
+        simplifier = { l, r -> simplifyEq(l, r, order) },
+        createNoSimplify = ::mkEqNoSimplify
+    )
 
     open fun <T : KSort> mkEqNoSimplify(lhs: KExpr<T>, rhs: KExpr<T>): KEqExpr<T> =
         eqCache.createIfContextActive {
@@ -778,8 +867,20 @@ open class KContext(
 
     private val distinctCache = mkAstInterner<KDistinctExpr<out KSort>>()
 
-    open fun <T : KSort> mkDistinct(args: List<KExpr<T>>): KExpr<KBoolSort> =
-        mkSimplified(args, KContext::simplifyDistinct, ::mkDistinctNoSimplify)
+    /**
+     * Create DISTINCT expression.
+     *
+     * @param order reorder arguments to ensure that (distinct a b) == (distinct b a)
+     * */
+    @JvmOverloads
+    open fun <T : KSort> mkDistinct(
+        args: List<KExpr<T>>,
+        order: Boolean = true
+    ): KExpr<KBoolSort> = mkSimplified(
+        args,
+        simplifier = { exprArgs -> simplifyDistinct(exprArgs, order) },
+        createNoSimplify = ::mkDistinctNoSimplify
+    )
 
     open fun <T : KSort> mkDistinctNoSimplify(args: List<KExpr<T>>): KDistinctExpr<T> =
         distinctCache.createIfContextActive {