Binary AND/OR operations (#84)

* open expression builders * Specialized binary AND/OR expressions * Specialized transformers for binary AND/OR * Specialized internalizers for binary AND/OR * Staged And/Or simplification * Fix array-n serialization * Version up to 0.4.4
UnitTestBot · Mar 15, 2023 · 3f5f29b · 3f5f29b
1 parent a4eb7b4
commit 3f5f29b
Show file tree

Hide file tree

Showing 25 changed files with 790 additions and 325 deletions.
diff --git a/README.md b/README.md
@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.3")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.4")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.3")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
 ```
 
 ## 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.3"
+version = "0.4.4"
 
 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.3")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.4")    
 }
 ```
 
 #### 3. Add one or more SMT solver dependencies:
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.3")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.3")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.4")
 }
 ```
 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.3")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.4")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.3")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.4")
 }
 
 java {

diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
@@ -7,6 +7,7 @@ import org.ksmt.decl.KDecl
 import org.ksmt.decl.KDeclVisitor
 import org.ksmt.decl.KFuncDecl
 import org.ksmt.expr.KAddArithExpr
+import org.ksmt.expr.KAndBinaryExpr
 import org.ksmt.expr.KAndExpr
 import org.ksmt.expr.KArray2Lambda
 import org.ksmt.expr.KArray2Select
@@ -136,6 +137,7 @@ import org.ksmt.expr.KLtArithExpr
 import org.ksmt.expr.KModIntExpr
 import org.ksmt.expr.KMulArithExpr
 import org.ksmt.expr.KNotExpr
+import org.ksmt.expr.KOrBinaryExpr
 import org.ksmt.expr.KOrExpr
 import org.ksmt.expr.KPowerArithExpr
 import org.ksmt.expr.KQuantifier
@@ -330,6 +332,10 @@ open class KBitwuzlaExprInternalizer(
         }
     }
 
+    override fun transform(expr: KAndBinaryExpr) = with(expr) {
+        transform(lhs, rhs, BitwuzlaKind.BITWUZLA_KIND_AND)
+    }
+
     override fun transform(expr: KOrExpr) = with(expr) {
         transformList(args) { args: LongArray ->
             when (args.size) {
@@ -342,6 +348,10 @@ open class KBitwuzlaExprInternalizer(
         }
     }
 
+    override fun transform(expr: KOrBinaryExpr) = with(expr) {
+        transform(lhs, rhs, BitwuzlaKind.BITWUZLA_KIND_OR)
+    }
+
     override fun transform(expr: KNotExpr) = with(expr) {
         transform(arg, BitwuzlaKind.BITWUZLA_KIND_NOT)
     }