Skip to content

Commit a600b47

Browse files
SaloedSaloed
authored
Documentation update (#92)
* Update readme: add MacOS-m1 platform * Build instructions * Upgrade version: 0.4.6
1 parent 7193fa0 commit a600b47

File tree

7 files changed

+219
-16
lines changed

7 files changed

+219
-16
lines changed

‎README.md‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,9 @@ repositories {
1414
}
1515

1616
// core
17-
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")
17+
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.6")
1818
// z3 solver
19-
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
19+
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.6")
2020
```
2121

2222
## Usage
@@ -26,17 +26,17 @@ Also, check out the [Java examples](examples/src/main/java).
2626
# Features
2727
Currently, KSMT supports the following SMT solvers:
2828

29-
| SMT Solver | Linux-x64 | Windows-x64 | MacOS-x64 |
30-
|--------------------------------------------------|:------------------:|:------------------:|:------------------:|
31-
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
32-
| [Bitwuzla](https://github.com/bitwuzla/bitwuzla) | :heavy_check_mark: | :heavy_check_mark: | |
33-
| [Yices2](https://github.com/SRI-CSL/yices2) | :heavy_check_mark: | :heavy_check_mark: | |
34-
| [cvc5](https://github.com/cvc5/cvc5) | :heavy_check_mark: | :heavy_check_mark: | |
29+
| SMT Solver | Linux-x64 | Windows-x64 | MacOS-aarch64 | MacOS-x64 |
30+
|--------------------------------------------------|:------------------:|:------------------:|:------------------:|:------------------:|
31+
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
32+
| [Bitwuzla](https://github.com/bitwuzla/bitwuzla) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
33+
| [Yices2](https://github.com/SRI-CSL/yices2) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
34+
| [cvc5](https://github.com/cvc5/cvc5) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
3535

3636
KSMT can express formulas in the following theories:
3737

38-
| Theory | Z3 | Bitwuzla | Yices2 | cvc5 |
39-
|-------------------------|:------------------:|:------------------:|--------------------|--------------------|
38+
| Theory | Z3 | Bitwuzla | Yices2 | cvc5 |
39+
|-------------------------|:------------------:|:------------------:|:------------------:|:------------------:|
4040
| Bitvectors | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
4141
| Arrays | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |
4242
| IEEE Floats | :heavy_check_mark: | :heavy_check_mark: | | :heavy_check_mark: |

‎buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ plugins {
99
}
1010

1111
group = "org.ksmt"
12-
version = "0.4.5"
12+
version = "0.4.6"
1313

1414
repositories {
1515
mavenCentral()

‎docs/getting-started.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,17 +18,17 @@ repositories {
1818
```kotlin
1919
dependencies {
2020
// core
21-
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")
21+
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.6")
2222
}
2323
```
2424

2525
#### 3. Add one or more SMT solver dependencies:
2626
```kotlin
2727
dependencies {
2828
// z3
29-
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
29+
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.6")
3030
// bitwuzla
31-
implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.5")
31+
implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.6")
3232
}
3333
```
3434
SMT solver specific packages are provided with solver native binaries.

‎examples/build.gradle.kts‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,9 @@ repositories {
1010

1111
dependencies {
1212
// core
13-
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.5")
13+
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.6")
1414
// z3 solver
15-
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.5")
15+
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.6")
1616
}
1717

1818
java {

‎ksmt-bitwuzla/dist/build.md‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
### Build details
2+
3+
We build Bitwuzla with the following configuration:
4+
```shell
5+
./configure production --shared --only-cadical
6+
```
7+
To make our distribution portable we statically link Bitwuzla against `libgmp`.
8+
9+
Jni bindings `bitwuzla_jni` are built without any tricks.
10+
11+
### Building on windows
12+
To produce Windows builds we use MSYS2 environment prepared as described [here](https://github.com/aytey/bitwuzla/blob/refreshed_windows_instructions/docs/building_on_windows.rst).
13+
Also, it is important to link statically with `libwinpthread`.
14+
15+
### Expected dynamic dependencies
16+
To ensure that our distribution is portable, we verify that the produced binaries have no dependencies that might not be present on the user's machine.
17+
18+
#### Linux x64
19+
```shell
20+
$ ldd libbitwuzla.so
21+
linux-vdso.so.1 (0x00007ffce92d0000)
22+
libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x00007f2fdaa00000)
23+
libm.so.6 => /usr/lib/libm.so.6 (0x00007f2fdad18000)
24+
libgcc_s.so.1 => /usr/lib/libgcc_s.so.1 (0x00007f2fdb192000)
25+
libc.so.6 => /usr/lib/libc.so.6 (0x00007f2fda819000)
26+
/usr/lib64/ld-linux-x86-64.so.2 (0x00007f2fdb1e0000)
27+
$ ldd libbitwuzla_jni.so
28+
libbitwuzla.so => not found
29+
linux-vdso.so.1 (0x00007ffd1ddc6000)
30+
libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x00007f6188800000)
31+
libm.so.6 => /usr/lib/libm.so.6 (0x00007f6188b18000)
32+
libgcc_s.so.1 => /usr/lib/libgcc_s.so.1 (0x00007f6189006000)
33+
libc.so.6 => /usr/lib/libc.so.6 (0x00007f6188619000)
34+
/usr/lib64/ld-linux-x86-64.so.2 (0x00007f618906d000)
35+
```
36+
37+
#### Windows x64
38+
```shell
39+
$ ldd libbitwuzla.dll
40+
ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
41+
KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
42+
KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
43+
msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
44+
CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000)
45+
bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000)
46+
$ ldd libbitwuzla_jni.dll
47+
ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
48+
KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
49+
KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
50+
msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
51+
libbitwuzla.dll => not found
52+
CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000)
53+
bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000)
54+
```
55+
56+
#### MacOS aarch64
57+
```shell
58+
$ otool -L libbitwuzla.dylib
59+
libbitwuzla.dylib:
60+
@rpath/libbitwuzla.dylib (compatibility version 0.0.0, current version 0.0.0)
61+
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0)
62+
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
63+
$ otool -L libbitwuzla_jni.dylib
64+
libbitwuzla_jni.dylib:
65+
@rpath/libbitwuzla_jni.dylib (compatibility version 0.0.0, current version 0.0.0)
66+
@rpath/libbitwuzla.dylib (compatibility version 0.0.0, current version 0.0.0)
67+
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0)
68+
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
69+
```

‎ksmt-cvc5/dist/build.md‎

Lines changed: 69 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
### Build details
2+
3+
We build cvc5 with the following configuration:
4+
```shell
5+
./configure.sh production --auto-download --ipo --no-static --no-cln --no-glpk --no-editline --cryptominisat --java-bindings
6+
```
7+
To make our distribution portable we statically link cvc5 against `libgmp`.
8+
9+
#### Building on Windows
10+
To produce Windows builds we use the same approach as in [`ksmt-bitwuzla`](../../ksmt-bitwuzla/dist/build.md).
11+
Also, we use addition configuration flag:
12+
```shell
13+
./configure.sh ... --win64-native
14+
```
15+
16+
### Expected dynamic dependencies
17+
To ensure that our distribution is portable, we verify that the produced binaries have no dependencies that might not be present on the user's machine.
18+
19+
#### Linux x64
20+
```shell
21+
$ ldd libcvc5.so libcvc5jni.so
22+
libcvc5.so:
23+
linux-vdso.so.1 (0x00007ffe22381000)
24+
libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x00007ff4c7800000)
25+
libm.so.6 => /usr/lib/libm.so.6 (0x00007ff4c8bf4000)
26+
libgcc_s.so.1 => /usr/lib/libgcc_s.so.1 (0x00007ff4c8bd4000)
27+
libc.so.6 => /usr/lib/libc.so.6 (0x00007ff4c7619000)
28+
/usr/lib64/ld-linux-x86-64.so.2 (0x00007ff4c8d0a000)
29+
libcvc5jni.so:
30+
linux-vdso.so.1 (0x00007ffccbbb5000)
31+
libcvc5.so => not found
32+
libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x00007fa594e00000)
33+
libgcc_s.so.1 => /usr/lib/libgcc_s.so.1 (0x00007fa5962db000)
34+
libc.so.6 => /usr/lib/libc.so.6 (0x00007fa594c19000)
35+
libm.so.6 => /usr/lib/libm.so.6 (0x00007fa5961f3000)
36+
/usr/lib64/ld-linux-x86-64.so.2 (0x00007fa596389000)
37+
```
38+
#### Windows x64
39+
```shell
40+
$ ldd libcvc5.dll libcvc5jni.dll
41+
libcvc5.dll:
42+
ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
43+
KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
44+
KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
45+
msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
46+
CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000)
47+
bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000)
48+
libcvc5jni.dll:
49+
ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
50+
KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
51+
KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
52+
msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
53+
libcvc5.dll => not found
54+
CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000)
55+
bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000)
56+
```
57+
#### MacOS aarch64
58+
```shell
59+
$ otool -L libcvc5.dylib libcvc5jni.dylib
60+
libcvc5.dylib:
61+
@rpath/libcvc5.dylib (compatibility version 0.0.0, current version 0.0.0)
62+
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0)
63+
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
64+
libcvc5jni.dylib:
65+
@rpath/libcvc5jni.dylib (compatibility version 0.0.0, current version 0.0.0)
66+
@rpath/libcvc5.dylib (compatibility version 0.0.0, current version 0.0.0)
67+
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0)
68+
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
69+
```

‎ksmt-yices/dist/build.md‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
### Build details
2+
3+
We build Yices with the following commands:
4+
```shell
5+
autoconf
6+
./configure --enable-thread-safety --disable-mcsat
7+
make MODE=release static-distribution
8+
```
9+
10+
To build Jni bindings `yices2java` we use the provided `Makefile` but we statically link `libgmp`.
11+
12+
#### Building on Windows
13+
To produce Windows builds we use the same approach as in [`ksmt-bitwuzla`](../../ksmt-bitwuzla/dist/build.md).
14+
15+
Yices defines enum constants `STATUS_INTERRUPTED` and `STATUS_ERROR` (`/src/include/yices_types.h`) that conflict with those defined in the Windows stdlib.
16+
We need to resolve this conflict before build.
17+
The simplest and working approach is to replace all occurrences of these constants.
18+
19+
### Expected dynamic dependencies
20+
To ensure that our distribution is portable, we verify that the produced binaries have no dependencies that might not be present on the user's machine.
21+
22+
#### Linux x64
23+
```shell
24+
$ ldd libyices.so libyices2java.so
25+
libyices.so:
26+
linux-vdso.so.1 (0x00007ffeeecff000)
27+
libm.so.6 => /usr/lib/libm.so.6 (0x00007f59eacec000)
28+
libc.so.6 => /usr/lib/libc.so.6 (0x00007f59eab05000)
29+
/usr/lib64/ld-linux-x86-64.so.2 (0x00007f59eb03b000)
30+
libyices2java.so:
31+
linux-vdso.so.1 (0x00007ffeafe26000)
32+
libyices.so.2.6 => not found
33+
libm.so.6 => /usr/lib/libm.so.6 (0x00007f38936e1000)
34+
libc.so.6 => /usr/lib/libc.so.6 (0x00007f38934fa000)
35+
/usr/lib64/ld-linux-x86-64.so.2 (0x00007f3893835000)
36+
```
37+
#### Windows x64
38+
```shell
39+
$ ldd libyices.dll libyices2java.dll
40+
libyices.dll:
41+
ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
42+
KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
43+
KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
44+
msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
45+
libyices2java.dll:
46+
ntdll.dll => /c/Windows/SYSTEM32/ntdll.dll (0x7ffb7a190000)
47+
KERNEL32.DLL => /c/Windows/System32/KERNEL32.DLL (0x7ffb78240000)
48+
KERNELBASE.dll => /c/Windows/System32/KERNELBASE.dll (0x7ffb77a70000)
49+
msvcrt.dll => /c/Windows/System32/msvcrt.dll (0x7ffb79410000)
50+
libyices.dll => not found
51+
CRYPTBASE.DLL => /c/Windows/SYSTEM32/CRYPTBASE.DLL (0x7ffb77190000)
52+
bcryptPrimitives.dll => /c/Windows/System32/bcryptPrimitives.dll (0x7ffb77de0000)
53+
```
54+
#### MacOS aarch64
55+
```shell
56+
$ otool -L libyices.dylib libyices2java.dylib
57+
libyices.dylib:
58+
@rpath/libyices.dylib (compatibility version 2.6.0, current version 2.6.4)
59+
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
60+
libyices2java.dylib:
61+
@rpath/libyices2java.dylib (compatibility version 0.0.0, current version 0.0.0)
62+
@rpath/libyices.dylib (compatibility version 2.6.0, current version 2.6.4)
63+
/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.36.0)
64+
/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1319.0.0)
65+
```

0 commit comments

Comments
 (0)