Symfpu module (#124)

* add symfpu module to support fp

* implement symfpu

* Fix casts

* Fix tests and configs

* Refactor tests

* Refactor tests

* Handle more exceptions in library loader

* Fix previousPowerOfTwo

* Refactor tests

* Remove debug prints

* Fix bv operations in utils

* Fix bv operations in utils

* Handle more exceptions in library loader

* Rework symfpu transformer

* ignore test data

* Remove redundant execution mode annotation

* Ignore all gradle builds

* Fix nan in packed bv

* Update docs

---------

Co-authored-by: Mark Vavilov <40399190+vavilovm@users.noreply.github.com>

Author: Saloed

.gitignore

@@ -3,5 +3,9 @@
 
 # Ignore Gradle build output directory
 build
+**/build/
 
 .idea
+
+# ignore ksmt test data
+ksmt-test/testData

README.md

@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.5)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.6)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.5")
+implementation("io.ksmt:ksmt-core:0.5.6")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.5")
+implementation("io.ksmt:ksmt-z3:0.5.6")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 
@@ -52,13 +52,15 @@ KSMT provides support for various solvers:
 
 You can also use SMT solvers across multiple theories:
 
-| Theory                  |         Z3         |      Bitwuzla      |       Yices2       |        cvc5        |
-|-------------------------|:------------------:|:------------------:|:------------------:|:------------------:|
-| Bitvectors              | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
-| Arrays                  | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
-| IEEE Floats             | :heavy_check_mark: | :heavy_check_mark: |                    | :heavy_check_mark: |
-| Uninterpreted Functions | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
-| Arithmetic              | :heavy_check_mark: |                    | :heavy_check_mark: | :heavy_check_mark: |
+| Theory                  |         Z3         |      Bitwuzla      |         Yices2          |        cvc5        |
+|-------------------------|:------------------:|:------------------:|:-----------------------:|:------------------:|
+| Bitvectors              | :heavy_check_mark: | :heavy_check_mark: |   :heavy_check_mark:    | :heavy_check_mark: |
+| Arrays                  | :heavy_check_mark: | :heavy_check_mark: |   :heavy_check_mark:    | :heavy_check_mark: |
+| IEEE Floats             | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: [^1] | :heavy_check_mark: |
+| Uninterpreted Functions | :heavy_check_mark: | :heavy_check_mark: |   :heavy_check_mark:    | :heavy_check_mark: |
+| Arithmetic              | :heavy_check_mark: |                    |   :heavy_check_mark:    | :heavy_check_mark: |
+
+[^1]: IEEE Floats are supported in Yices2 using ksmt-symfpu 
 
 ### Solver-agnostic formula representation
 

Requirements.md

@@ -25,7 +25,7 @@
 | [Model based projection](#model-based-projection)                                | TODO           |
 | [Support more theories](#support-more-theories)                                  | TODO           |
 | [Solver proofs](#solver-proofs)                                                  | TODO           |
-| [SymFpu](#symfpu)                                                                | In progress    |
+| [SymFpu](#symfpu)                                                                | Done           |
 | ...                                                                              | -              |
 
 

buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.5"
+version = "0.5.6"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.5")    
+    implementation("io.ksmt:ksmt-core:0.5.6")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.5")
+    implementation("io.ksmt:ksmt-z3:0.5.6")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.5")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.6")
 }
 ```
 

examples/build.gradle.kts

@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.5")
+    implementation("io.ksmt:ksmt-core:0.5.6")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.5")
+    implementation("io.ksmt:ksmt-z3:0.5.6")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.5")
+    implementation("io.ksmt:ksmt-runner:0.5.6")
 }
 
 java {