diff --git a/README.md b/README.md index 186d7bb7d..d8bd8bb81 100644 --- a/README.md +++ b/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.19) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.20) [![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.19") +implementation("io.ksmt:ksmt-core:0.5.20") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.19") +implementation("io.ksmt:ksmt-z3:0.5.20") ``` Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts index 708537b7a..81d521be4 100644 --- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts +++ b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts @@ -11,7 +11,7 @@ plugins { } group = "io.ksmt" -version = "0.5.19" +version = "0.5.20" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 71fb1bf21..342bb5619 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -34,7 +34,7 @@ repositories { ```kotlin dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.19") + implementation("io.ksmt:ksmt-core:0.5.20") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.19") + implementation("io.ksmt:ksmt-z3:0.5.20") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.19") + implementation("io.ksmt:ksmt-bitwuzla:0.5.20") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index dfe2396ee..20d8c7536 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.19") + implementation("io.ksmt:ksmt-core:0.5.20") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.19") + implementation("io.ksmt:ksmt-z3:0.5.20") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.19") + implementation("io.ksmt:ksmt-runner:0.5.20") } java { diff --git a/ksmt-yices/bindings-native/macos_build.sh b/ksmt-yices/bindings-native/macos_build.sh new file mode 100644 index 000000000..603006ef7 --- /dev/null +++ b/ksmt-yices/bindings-native/macos_build.sh @@ -0,0 +1,53 @@ +YICES_VERSION="2.6.4" + +export MACOSX_DEPLOYMENT_TARGET=11.1 +#apt-get install -y openjdk-8-jdk +#omp install openjdk11 + +export CC=oa64-clang +export CXX=oa64-clang++ + +JAVAC="/usr/bin/javac" +JAVA_HOME="/usr/local/osxcross/macports/pkgs/opt/local/Library/Java/JavaVirtualMachines/openjdk11/Contents/Home" +CPPFLAGS="-I $JAVA_HOME/include -I $JAVA_HOME/include/darwin -I $(realpath ../dist-mac/include) -I $(realpath ../libgmp/dist/include)" +CXXFLAGS="-fpermissive -g -fPIC -O3 -stdlib=libc++" +export LIBS="$(realpath ../libgmp/dist/lib/libgmp.a) $(realpath ../dist-mac/lib/libyices.2.dylib)" +export LDFLAGS="-L$(realpath ../libgmp/dist/lib) -L$(realpath ../dist-mac/lib/)" + +YICES_2_JAVA_LIB_NAME="libyices2java.dylib" + +rm -rf yices2_java_bindings + +# https://github.com/SRI-CSL/yices2_java_bindings/commit/d9858e540425072443830d2638db5ffdc8c92cd1 +git clone https://github.com/SRI-CSL/yices2_java_bindings +cd yices2_java_bindings +git checkout d9858e5 + +# +# Patch description +# +# Bindings native part: +# 1. Fix cardinality check in `expand function`. +# 2. Provide methods to extract values of product/sum components +# +# Bindings java part: +# 1. Add the corresponding methods and classes to interact +# with native product/sum value extraction methods +# 2. Disable default native library load +# +git apply ../yices-bindings-patch.patch + + +rm -rf build +mkdir build +cd build + +cp ../src/main/java/com/sri/yices/yicesJNI.cpp . + +$JAVAC -h . ../src/main/java/com/sri/yices/*.java + +$CXX $LD_STATIC_FLAGS $CPPFLAGS $CXXFLAGS -c yicesJNI.cpp + +$CXX $LD_STATIC_FLAGS $LDFLAGS -s -shared -o $YICES_2_JAVA_LIB_NAME yicesJNI.o $LIBS + +cp $YICES_2_JAVA_LIB_NAME ../../ diff --git a/ksmt-yices/bindings-native/yices-bindings-patch.patch b/ksmt-yices/bindings-native/yices-bindings-patch.patch index 54af02555..aab8307ce 100644 --- a/ksmt-yices/bindings-native/yices-bindings-patch.patch +++ b/ksmt-yices/bindings-native/yices-bindings-patch.patch @@ -529,10 +529,19 @@ Subject: [PATCH 5/7] Minor change 1 file changed, 4 insertions(+) diff --git a/src/main/java/com/sri/yices/YVal.java b/src/main/java/com/sri/yices/YVal.java -index 574ba57..1509541 100644 +index 574ba57..8daa156 100644 --- a/src/main/java/com/sri/yices/YVal.java +++ b/src/main/java/com/sri/yices/YVal.java -@@ -27,4 +27,8 @@ public String toString(){ +@@ -7,7 +7,7 @@ package com.sri.yices; + * yices_get_value evaluates a term and returns a node descriptor from + * which the term value can be constructed. + * Within a model, each node has an integer identifier and a tag that +- * specifies the node’s type. All DAG-exploration functions store this ++ * specifies the nodes type. All DAG-exploration functions store this + * information in records of type YVal. + * + * I see no reason to make it anything more than a glorified C-struct. +@@ -27,4 +27,8 @@ public class YVal { return String.format("<%s: %d>", tag, id); } @@ -542,6 +551,7 @@ index 574ba57..1509541 100644 + } } + From dc29fd6c861384a3cc32eadd7cdc716b914a2efe Mon Sep 17 00:00:00 2001 From: Pavel Balay Date: Mon, 6 Feb 2023 02:53:12 +0300 diff --git a/ksmt-yices/dist/macos/build.sh b/ksmt-yices/dist/macos/build.sh new file mode 100644 index 000000000..5219fe6cb --- /dev/null +++ b/ksmt-yices/dist/macos/build.sh @@ -0,0 +1,21 @@ +#apt-get install -y autoconf gperf + +export CC=oa64-clang +export CXX=oa64-clang++ + +autoconf + +export CFLAGS="-O3" +export CXXFLAGS="-O3" +export CPPFLAGS="-I$(realpath libgmp/dist/include)" +export LIBS=$(realpath libgmp/dist/lib/libgmp.a) +export LDFLAGS="-L$(realpath libgmp/dist/lib)" + +./configure --enable-thread-safety --disable-mcsat --host=arm64-apple-darwin20.2 \ + --prefix=$(realpath dist-mac) \ + --with-pic-gmp=$(realpath libgmp/dist/lib/libgmp.a) \ + --with-pic-gmp-include-dir=$(realpath libgmp/dist/include) + +make MODE=release ARCH=arm64-apple-darwin20.2 POSIXOS=darwin show-details dist install + +llvm-install-name-tool-14 -id libyices.2.dylib dist-mac/lib/libyices.2.dylib diff --git a/ksmt-yices/dist/macos/libgmp_build.sh b/ksmt-yices/dist/macos/libgmp_build.sh new file mode 100644 index 000000000..9a4be44c1 --- /dev/null +++ b/ksmt-yices/dist/macos/libgmp_build.sh @@ -0,0 +1,13 @@ +#wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz && tar Jxf gmp-6.3.0.tar.xz +cd gmp-6.3.0 + +export CC=oa64-clang +export CXX=oa64-clang++ +export CFLAGS="-O3" +export CXXFLAGS="-O3" + +./configure --host=arm64-apple-darwin20.2 --prefix=$(realpath ../dist) \ + --enable-static=yes --enable-shared=no --enable-cxx --with-pic + +make -j$(nproc) +make install diff --git a/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip b/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip index 0884b4e55..cee2a43db 100644 Binary files a/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip and b/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip differ