Yices macos arm (#153)

Saloed · web-flow · commit 5d2fb43126da · 2024-02-12T19:26:47.000+03:00
* Yices macos-arm build

* Update Yices macos build docs

* Upgrade version to 0.5.20
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 <pavel.balai@gmail.com>
 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
@@ -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
@@ -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

Original file line number	Diff line number	Diff line change
`@@ -11,7 +11,7 @@ plugins {`
`11`	`11`	`}`
`12`	`12`
`13`	`13`	`group = "io.ksmt"`
`14`		`-version = "0.5.19"`
	`14`	`+version = "0.5.20"`
`15`	`15`
`16`	`16`	`repositories {`
`17`	`17`	`mavenCentral()`