Skip to content

Add a build script for Yices on macOS #628

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
daniel-raffler wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Add a build script for Yices on macOS #628

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cf98f4c
Yices: Add build script for macOS binaries
daniel-raffler Mar 25, 2026
944caf4
Yices: Add a guide for building solver the Yices binaries on macOS
daniel-raffler Mar 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 14 additions & 14 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,20 +61,20 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,

JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):

| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description |
|-------------------------------------------------------------------------|:-------------------:|:-------------------:|:------------------:|:------------------:|:-------------------------------------------------------:|:------------------:|:----------------------------------------------------------------------------|
| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: | | | | a fast solver for bitvector logic |
| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated |
| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | |
| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ | | |
| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² | | | | | |
| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries |
| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ | | |
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | | | | | an older version of Z3 that still provides interpolation support |
| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description |
|-------------------------------------------------------------------------|:-------------------:|:-------------------:|:------------------:|:------------------:|:-------------------------------------------------------:|:-----------------------------------------:|:----------------------------------------------------------------------------|
| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: | | | | a fast solver for bitvector logic |
| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | | | | a fast solver for bitvector logic, misses formula introspection, deprecated |
| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | | | | |
| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | |
| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ | | |
| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² | | | | | |
| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | | | | based on MathSAT5, with support for optimization queries |
| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | | :heavy_check_mark: | | [partial](doc/How-to-build-for-macOS.md)⁴ | [partial](doc/How-to-build-for-macOS.md)⁴ | |
| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | | | | | an older version of Z3 that still provides interpolation support |

We support a reasonable list of operating systems and versions.
- Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
Expand Down
96 changes: 96 additions & 0 deletions build/build-publish-solvers/solver-yices.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,13 @@ SPDX-License-Identifier: Apache-2.0
<condition property="yices-java.installed">
<available file="${yices2.buildDir}/yices2_java_bindings/dist/lib" type="dir"/>
</condition>

<condition property="build.architecture" value="arm64" else="x64">
<os arch="aarch64"/>
</condition>
<condition property="build.homebrew" value="/opt/homebrew" else="/usr/local">
<os arch="aarch64"/>
</condition>
</target>

<target name="download-cudd" depends="build-initialize" unless="cudd.downloaded">
Expand Down Expand Up @@ -89,6 +96,23 @@ SPDX-License-Identifier: Apache-2.0
<arg value="clean"/>
</exec>
</target>
<target name="build-cudd-macOS" depends="download-cudd" unless="cudd.installed">
<exec executable="aclocal" dir="${yices2.buildDir}/cudd" failonerror="true"/>
<exec executable="autoconf" dir="${yices2.buildDir}/cudd" failonerror="true"/>
<exec executable="automake" dir="${yices2.buildDir}/cudd" failonerror="true"/>
<!-- macOS build -->
<exec executable="./configure" dir="${yices2.buildDir}/cudd" failonerror="true">
<env key="CFLAGS" value="-fPIC"/>
<arg value="--prefix=${yices2.buildDir}/cudd/install/${build.architecture}-macos"/>
</exec>
<exec executable="make" dir="${yices2.buildDir}/cudd" failonerror="true">
<arg value="-j"/>
<arg value="install"/>
</exec>
<exec executable="make" dir="${yices2.buildDir}/cudd" failonerror="true">
<arg value="clean"/>
</exec>
</target>

<target name="download-libpoly" depends="build-initialize" unless="libpoly.downloaded">
<exec executable="git" dir="${yices2.buildDir}" failonerror="true">
Expand Down Expand Up @@ -129,6 +153,23 @@ SPDX-License-Identifier: Apache-2.0
</exec>
<delete dir="${yices2.buildDir}/libpoly/build"/>
</target>
<target name="build-libpoly-macOS" depends="download-libpoly" unless="libpoly.installed">
<!-- macOS build -->
<mkdir dir="${yices2.buildDir}/libpoly/build"/>
<exec executable="cmake" dir="${yices2.buildDir}/libpoly/build" failonerror="true">
<arg value=".."/>
<arg value="-DCMAKE_BUILD_TYPE=Release"/>
<arg value="-DCMAKE_INSTALL_PREFIX=${yices2.buildDir}/libpoly/install/${build.architecture}-macos"/>
<arg value="-DGMP_INCLUDE_DIR=${build.homebrew}/include"/>
<arg value="-DGMP_LIBRARY=${build.homebrew}/lib/libgmp.a"/>
<arg value="-DLIBPOLY_BUILD_PYTHON_API=OFF"/>
</exec>
<exec executable="make" dir="${yices2.buildDir}/libpoly/build" failonerror="true">
<arg value="-j"/>
<arg value="install"/>
</exec>
<delete dir="${yices2.buildDir}/libpoly/build"/>
</target>

<target name="download-yices2" depends="build-initialize" unless="yices.downloaded">
<exec executable="git" dir="${yices2.buildDir}" failonerror="true">
Expand Down Expand Up @@ -183,6 +224,33 @@ SPDX-License-Identifier: Apache-2.0
<arg value="OPTION=mingw32"/>
</exec>
</target>
<target name="build-yices2-macOS"
depends="build-cudd-macOS, build-libpoly-macOS, download-yices2" unless="yices.installed">
<exec executable="git" dir="${yices2.buildDir}/yices2" failonerror="true">
<arg value="apply"/>
<arg value="${basedir}/lib/native/source/yices2/yices.patch"/>
</exec>
<exec executable="autoconf" dir="${yices2.buildDir}/yices2" failonerror="true"/>
<delete file="${yices2.buildDir}/yices2/INSTALL"/>
<mkdir dir="${yices2.buildDir}/yices2/install"/>
<!-- macOS build -->
<exec executable="./configure" dir="${yices2.buildDir}/yices2" failonerror="true">
<env key="LDFLAGS" value="-L${build.homebrew}/lib -L${yices2.buildDir}/libpoly/install/${build.architecture}-macos/lib -L${yices2.buildDir}/cudd/install/${build.architecture}-macos/lib"/>
<env key="CFLAGS" value="-I${build.homebrew}/include -I${yices2.buildDir}/libpoly/install/${build.architecture}-macos/include -I${yices2.buildDir}/cudd/install/${build.architecture}-macos/include"/>
<arg value="--enable-mcsat"/>
<arg value="--enable-thread-safety"/>
<arg value="--prefix=${yices2.buildDir}/yices2/install/${build.architecture}-macos"/>
</exec>
<exec executable="make" dir="${yices2.buildDir}/yices2" failonerror="true">
<arg value="-j"/>
</exec>
<exec executable="make" dir="${yices2.buildDir}/yices2" failonerror="true">
<arg value="install"/>
</exec>
<exec executable="make" dir="${yices2.buildDir}/yices2" failonerror="true">
<arg value="clean"/>
</exec>
</target>
<target name="clean-yices2" depends="build-initialize, clean-yices2-java" if="yices.installed">
<delete dir="${yices2.buildDir}/yices2/install"/>
<exec executable="git" dir="${yices2.buildDir}/yices2" failonerror="true">
Expand Down Expand Up @@ -235,6 +303,25 @@ SPDX-License-Identifier: Apache-2.0
<arg value="install"/>
</exec>
</target>
<target name="build-yices2-java-macOS"
depends="build-yices2-macOS, download-yices2-java"
unless="yices-java.installed">
<exec executable="git" dir="${yices2.buildDir}/yices2_java_bindings" failonerror="true">
<arg value="apply"/>
<arg value="${basedir}/lib/native/source/yices2/jni.patch"/>
</exec>
<mkdir dir="${yices2.buildDir}/yices2_java_bindings/dist/lib"/>
<!-- macOS build -->
<exec executable="ant" dir="${yices2.buildDir}/yices2_java_bindings" failonerror="true">
<env key="OS" value="darwin"/>
<env key="JNI_PATH" value="${java.home}/include"/>
<env key="GMP_PATH" value="${build.homebrew}"/>
<env key="CUDD_PATH" value="${yices2.buildDir}/cudd/install/${build.architecture}-macos"/>
<env key="POLY_PATH" value="${yices2.buildDir}/libpoly/install/${build.architecture}-macos"/>
<env key="YICES_PATH" value="${yices2.buildDir}/yices2/install/${build.architecture}-macos"/>
<arg value="install"/>
</exec>
</target>
<target name="clean-yices2-java" depends="build-initialize" if="yices-java.installed">
<exec executable="ant" dir="${yices2.buildDir}/yices2_java_bindings" failonerror="true">
<arg value="clean"/>
Expand All @@ -246,6 +333,15 @@ SPDX-License-Identifier: Apache-2.0
</exec>
</target>

<target name="publish-yices2-macOS" depends="load-ivy, build-yices2-java-macOS"
description="Compile Yices2 binaries for macOS">
<condition property="install.architecture" value="arm64" else="x86_64">
<os arch="aarch64"/>
</condition>
<mkdir dir="lib/native/${build.architecture}-macosx"/>
<copy file="${yices2.buildDir}/yices2_java_bindings/dist/lib/libyices2java.dylib" tofile="lib/native/${install.architecture}-macosx/libyices2java.dylib" failonerror="true"/>
</target>

<target name="publish-yices2" depends="load-ivy, build-yices2-java"
description="Publish Yices2 binaries to Ivy repo.">
<sequential>
Expand Down
43 changes: 43 additions & 0 deletions doc/How-to-build-for-macOS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
<!--
This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt

SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>

SPDX-License-Identifier: Apache-2.0
-->

# Building solver binaries for macOS

We currently can't provide binaries for all supported solvers on macOS. However, it's often
possible to build the necessary binaries from source, and we try to include a simple build
script wherever possible

## Yices

To build the Yices binaries, we first need some build dependencies and GMP, which can all be
installed via Homebrew:

```shell
brew update
brew install gperf lcov autoconf automake libtool
brew install gmp
```

Then, we build the Yices2 binaries by running the build script included with JavaSMT:

```shell
git clone git@github.com:sosy-lab/java-smt.git
cd java-smt
ant publish-yices2-macOS
```

The script will build several dependencies before compiling Yices and may run for up to 10
minutes. Once it's finished the binary `libyices2java.dylib` can be found under `lib/native`.
Depending on your system architecture, it will be either in the `arm64-macos` (ARM) or
`x64_64-macos` (Intel) folder

You can then either copy the binary to your project folder, or
set `DYLD_LIBRARY_PATH` to include the binary folder to make sure Yices will be found when
running JavaSMT
10 changes: 7 additions & 3 deletions lib/native/source/yices2/jni.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,9 +52,13 @@ diff --git a/src/main/java/com/sri/yices/Makefile b/src/main/java/com/sri/yices/
+LIBS := -lyices -lcudd -lpoly -lgmpxx -lgmp

CXX ?= g++

@@ -86,7 +94,10 @@
$(CXX) $(CPPFLAGS) $(CXXFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)

@@ -83,10 +91,13 @@
$(CXX) $(CPPFLAGS) $(CXXFLAGS) -Wall -c yicesJNI.cpp

libyices2java.dylib: yicesJNI.o
- $(CXX) $(CPPFLAGS) $(CXXFLAGS) -dynamiclib -o $@ yicesJNI.o $(LIBS)
+ $(CXX) $(CFLAGS) $(LDFLAGS) -o $@ yicesJNI.o -dynamiclib $(YICES_PATH)/lib/libyices.a $(CUDD_PATH)/lib/libcudd.a $(POLY_PATH)/lib/libpoly.a $(GMP_PATH)/lib/libgmpxx.a $(GMP_PATH)/lib/libgmp.a -lc -lm

libyices2java.so: yicesJNI.o
- $(CXX) $(CFLAGS) $(LDFLAGS) -shared -o $@ yicesJNI.o $(LIBS)
Expand Down
Loading