Add bitwuzla

README.md

@@ -56,18 +56,19 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,
 
 Currently JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
 
-| SMT Solver | Linux64 | Windows64 | MacOS | Description |
-| --- |:---:|:---:|:---:|:--- |
-| [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |  | a fast solver for bitvector logic, misses formula introspection |
-| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: |  |  |  |
-| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: |  |  | new! |
-| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: |  |  |
-| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: |  |  | new! |
-| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: |  |  | based on MathSAT5, with support for optimization |
-| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :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: | Java-based SMT solver |
-| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | [soon](https://github.com/sosy-lab/java-smt/pull/215) |  |  |
-| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
+| SMT Solver                                                              | Linux64 | Windows64 | MacOS | Description                                                                  |
+|-------------------------------------------------------------------------|:---:|:---:|:---:|:-----------------------------------------------------------------------------|
+| [Bitwuzla](https://boolector.github.io/)                                | :heavy_check_mark: |  |  | a fast solver for bitvector and floating-point logic, successor of Boolector |
+| [Boolector](https://boolector.github.io/)                               | :heavy_check_mark: |  |  | a fast solver for bitvector logic, misses formula introspection              |
+| [CVC4](https://cvc4.github.io/)                                         | :heavy_check_mark: |  |  |                                                                              |
+| [CVC5](https://cvc5.github.io/)                                         | :heavy_check_mark: |  |  | new!                                                                         |
+| [MathSAT5](http://mathsat.fbk.eu/)                                      | :heavy_check_mark: | :heavy_check_mark: |  |                                                                              |
+| [OpenSMT](https://verify.inf.usi.ch/opensmt)                            | :heavy_check_mark: |  |  | new!                                                                         |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/)                        | :heavy_check_mark: |  |  | based on MathSAT5, with support for optimization                             |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml)               | :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: | Java-based SMT solver                                                        |
+| [Yices2](https://yices.csl.sri.com/)                                    | :heavy_check_mark: | [soon](https://github.com/sosy-lab/java-smt/pull/215) |  |                                                                              |
+| [Z3](https://github.com/Z3Prover/z3)                                    | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver                                                 |
 
 The following features are supported (depending on the used SMT solver):
 

build.xml

@@ -22,6 +22,7 @@ SPDX-License-Identifier: Apache-2.0
 
     <!-- one configuration per solver -->
     <property name="ivy.solver.configurations" value="
+        runtime-bitwuzla,
         runtime-boolector,
         runtime-cvc4,
         runtime-cvc5,
@@ -90,7 +91,8 @@ SPDX-License-Identifier: Apache-2.0
 
     <target name="tests" depends="unit-tests-coverage" description="Run all tests"/>
 
-    <target name="publish" depends="tests, dist, publish-artifacts" description="Publish current version of JavaSMT to Ivy repository" />
+    <target name="publish" depends="dist, publish-artifacts"
+            description="Publish current version of JavaSMT to Ivy repository"/>
 
     <target name="documentation" depends="collect-options, javadoc" description="Build documentation"/>
 

build/build-publish-solvers.xml

@@ -11,8 +11,9 @@ SPDX-License-Identifier: Apache-2.0
 -->
 
 <!-- vim: set tabstop=8 shiftwidth=4 expandtab sts=4 filetype=ant fdm=marker: -->
-<project name="publish-solvers" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
+<project name="publish-solvers" basedir=".">
 
+    <import file="build-publish-solvers/solver-bitwuzla.xml"/>
     <import file="build-publish-solvers/solver-boolector.xml"/>
     <import file="build-publish-solvers/solver-cvc4.xml"/>
     <import file="build-publish-solvers/solver-cvc5.xml"/>

build/build-publish-solvers/build-jar-yices2.xml

@@ -25,7 +25,9 @@ SPDX-License-Identifier: Apache-2.0
     <target name="jar-yices2" depends="determine-version, build"
               description="Create a runnable JAR file of all classes related to Yices2">
         <property name="yices2jar.file" value="javasmt-yices2-${version}.jar"/>
-        <copy todir="${class.dir}"><fileset dir=".." includes="META-INF/**"/></copy>
+        <copy todir="${class.dir}">
+            <fileset dir=".." includes="META-INF/**"/>
+        </copy>
         <manifestclasspath property="yices2Classpath.jar" jarfile="${ivy.lib.dir}/runtime-yices2/${jar.file}" maxParentLevels="0">
             <classpath><fileset dir="${ivy.lib.dir}/runtime-yices2" includes="checker-qual.jar common.jar guava.jar"/></classpath>
         </manifestclasspath>

build/build-publish-solvers/macros.xml

@@ -32,9 +32,10 @@ SPDX-License-Identifier: Apache-2.0
         <attribute name="solverName"/>
         <attribute name="solverVersion"/>
         <sequential>
-            <available property="ivy.hasrepository" file="repository/${ivy.organisation}/${ivy.module}" />
+            <available property="ivy.hasrepository"
+                       file="repository/${ivy.organisation}/${ivy.module}"/>
             <fail unless="ivy.hasrepository"
-                  message="Cannot publish without 'repository' dir, please run 'svn co https://svn.sosy-lab.org/software/ivy/repository/${ivy.organisation}/${ivy.module} repository/${ivy.organisation}/${ivy.module}'." />
+                  message="Cannot publish without 'repository' dir, please run 'svn co https://svn.sosy-lab.org/software/ivy/repository/${ivy.organisation}/${ivy.module} repository/${ivy.organisation}/${ivy.module}'."/>
             <ivy:publish
                     pubrevision="@{solverVersion}"
                     resolver="Sosy-Lab-Publish"
@@ -44,8 +45,10 @@ SPDX-License-Identifier: Apache-2.0
             <echo>
                 You now want to run
                 svn add repository/${ivy.organisation}/${ivy.module}/*-@{solverVersion}*
-                svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version @{solverVersion} of @{solverName} Solver"
-                to make the new version publicly available.</echo>
+                svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version
+                @{solverVersion} of @{solverName} Solver"
+                to make the new version publicly available.
+            </echo>
         </sequential>
     </macrodef>
 </project>

build/build-publish-solvers/solver-bitwuzla.xml

@@ -0,0 +1,136 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+
+<!--
+  ~  JavaSMT is an API wrapper for a collection of SMT solvers.
+  ~  This file is part of JavaSMT.
+  ~
+  ~  Copyright (C) 2007-2016  Dirk Beyer
+  ~  All rights reserved.
+  ~
+  ~  Licensed under the Apache License, Version 2.0 (the "License");
+  ~  you may not use this file except in compliance with the License.
+  ~  You may obtain a copy of the License at
+  ~
+  ~      http://www.apache.org/licenses/LICENSE-2.0
+  ~
+  ~  Unless required by applicable law or agreed to in writing, software
+  ~  distributed under the License is distributed on an "AS IS" BASIS,
+  ~  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+  ~  See the License for the specific language governing permissions and
+  ~  limitations under the License.
+  -->
+
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab sts=4 filetype=ant fdm=marker: -->
+<project name="publish-solvers-cvc5" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
+
+    <import file="macros.xml"/>
+
+    <!-- SECTION: Publishing Bitwuzla {{{1
+         ==================================================================
+    -->
+    <target name="package-bitwuzla" depends="">
+        <fail unless="bitwuzla.path">
+            Please specify the path to Bitwuzla with the flag -Dbitwuzla.path=/path/to/bitwuzla.
+            The path has to point to the root Bitwuzla folder, i.e.,
+            a checkout of the official git repositoy from 'https://github.com/bitwuzla/bitwuzla'.
+            Note that shell substitutions do not work and a full absolute path has to be specified.
+        </fail>
+        <echo>
+            The path is ${bitwuzla.path}
+        </echo>
+
+        <fail unless="bitwuzla.customRev">
+            Please specify a custom revision with the flag -Dbitwuzla.customRev=XXX.
+            The custom revision has to be unique amongst the already known version
+            numbers from the ivy repository. The script will append the git revision.
+        </fail>
+
+        <fail unless="gmp.path">
+            Please specify the path to GMP with the flag -Dgmp.path=/path/to/gmp.
+            The path has to point to the root GMP folder with version equal to or larger than 6.1.
+            Note that shell substitutions do not work and a full absolute path has to be specified.
+        </fail>
+
+        <!-- get a naive version -->
+        <exec executable="git" dir="${bitwuzla.path}" outputproperty="bitwuzla.revision"
+              failonerror="true">
+            <arg value="show"/>
+            <arg value="-s"/>
+            <arg value="--format=%h"/>
+        </exec>
+        <property name="bitwuzla.version" value="${bitwuzla.customRev}-g${bitwuzla.revision}"/>
+        <echo message="Building Bitwuzla in version '${bitwuzla.version}'"/>
+
+        <!-- add JNI wrapper before compiling Bitwuzla -->
+        <copy file="lib/native/source/libbitwuzla/bitwuzla_wrap.c"
+              tofile="${bitwuzla.path}/src/bitwuzla_wrap.c"/>
+
+        <exec executable="./configure.py" dir="${bitwuzla.path}" failonerror="true">
+            <arg value="--shared"/>
+            <arg value="--wipe"/>
+        </exec>
+        <exec executable="meson" dir="${bitwuzla.path}/build/" failonerror="true">
+            <arg value="compile"/>
+        </exec>
+
+        <!-- unneeded symbols are removed by Meson automatically -->
+
+        <exec executable="lib/native/source/libbitwuzla/compile.sh" failonerror="true">
+            <arg value="${bitwuzla.path}"/>
+        </exec>
+
+        <!-- fix RPATH and library dependencies -->
+        <exec executable="patchelf" dir="lib/native/source/libbitwuzla/" failonerror="true">
+            <arg value="--set-rpath"/>
+            <arg value="$ORIGIN"/>
+            <arg value="--replace-needed"/>
+            <arg value="libbitwuzla.so.0"/>
+            <arg value="libbitwuzla.so"/>
+            <arg value="libbitwuzlaJNI.so"/>
+        </exec>
+        <exec executable="patchelf" dir="${bitwuzla.path}/build/src/" failonerror="true">
+            <arg value="--set-rpath"/>
+            <arg value="$ORIGIN"/>
+            <arg value="libbitwuzla.so.0"/>
+        </exec>
+        <exec executable="patchelf" dir="${bitwuzla.path}/build/src/lib/" failonerror="true">
+            <arg value="--set-rpath"/>
+            <arg value="$ORIGIN"/>
+            <arg value="libbitwuzlals.so"/>
+        </exec>
+        <exec executable="patchelf" dir="${bitwuzla.path}/build/src/lib/" failonerror="true">
+            <arg value="--set-rpath"/>
+            <arg value="$ORIGIN"/>
+            <arg value="libbitwuzlabv.so"/>
+        </exec>
+        <exec executable="patchelf" dir="${bitwuzla.path}/build/src/lib/" failonerror="true">
+            <arg value="--set-rpath"/>
+            <arg value="$ORIGIN"/>
+            <arg value="libbitwuzlabb.so"/>
+        </exec>
+        <exec executable="patchelf" dir="${gmp.path}/.libs/" failonerror="true">
+            <arg value="--set-rpath"/>
+            <arg value="$ORIGIN"/>
+            <arg value="libgmp.so.10.5.0"/>
+        </exec>
+
+        <!-- copy library files into directory to be published for IVY -->
+        <copy file="lib/native/source/libbitwuzla/libbitwuzlaJNI.so"
+              tofile="libbitwuzlaJNI-${bitwuzla.version}.so"/>
+        <copy file="${bitwuzla.path}/build/src/lib/libbitwuzlals.so"
+              tofile="libbitwuzlals-${bitwuzla.version}.so"/>
+        <copy file="${bitwuzla.path}/build/src/lib/libbitwuzlabv.so"
+              tofile="libbitwuzlabv-${bitwuzla.version}.so"/>
+        <copy file="${bitwuzla.path}/build/src/lib/libbitwuzlabb.so"
+              tofile="libbitwuzlabb-${bitwuzla.version}.so"/>
+        <copy file="${gmp.path}/.libs/libgmp.so.10.5.0" tofile="libgmp-${bitwuzla.version}.so"/>
+        <copy file="${bitwuzla.path}/build/src/libbitwuzla.so.0"
+              tofile="libbitwuzla-${bitwuzla.version}.so"/>
+    </target>
+
+    <target name="publish-bitwuzla" depends="package-bitwuzla, load-ivy"
+            description="Publish Bitwuzla binaries to Ivy repository.">
+        <ivy:resolve conf="solver-bitwuzla" file="solvers_ivy_conf/ivy_bitwuzla.xml"/>
+        <publishToRepository solverName="Bitwuzla" solverVersion="${bitwuzla.version}"/>
+    </target>
+</project>

build/build-publish-solvers/solver-boolector.xml

@@ -30,7 +30,8 @@ SPDX-License-Identifier: Apache-2.0
         </fail>
 
         <!-- get a nive version -->
-        <exec executable="git" dir="${boolector.path}" outputproperty="boolector.revision" failonerror="true">
+        <exec executable="git" dir="${boolector.path}" outputproperty="boolector.revision"
+              failonerror="true">
             <arg value="show"/>
             <arg value="-s"/>
             <arg value="--format=%h"/>
@@ -39,56 +40,65 @@ SPDX-License-Identifier: Apache-2.0
         <echo message="Building Boolector in version '${boolector.version}'"/>
 
         <!-- add JNI wrapper before compiling Boolector -->
-        <copy file="lib/native/source/libboolector/interface_wrap.c"                tofile="${boolector.path}/src/interface_wrap.c"/>
-        <copy file="lib/native/source/libboolector/include_interface_and_jni.patch" tofile="${boolector.path}/src/include_interface_and_jni.patch"/>
+        <copy file="lib/native/source/libboolector/interface_wrap.c"
+              tofile="${boolector.path}/src/interface_wrap.c"/>
+        <copy file="lib/native/source/libboolector/include_interface_and_jni.patch"
+              tofile="${boolector.path}/src/include_interface_and_jni.patch"/>
         <exec executable="git" dir="${boolector.path}" failonerror="true">
             <arg value="apply"/>
             <arg value="src/include_interface_and_jni.patch"/>
         </exec>
 
         <!-- build Boolector -->
-        <exec executable="./contrib/setup-picosat.sh"    dir="${boolector.path}" failonerror="true"/>
-        <exec executable="./contrib/setup-minisat.sh"    dir="${boolector.path}" failonerror="true"/>
-    	<exec executable="./contrib/setup-cms.sh"    	 dir="${boolector.path}" failonerror="true"/>
-        <exec executable="./contrib/setup-lingeling.sh"  dir="${boolector.path}" failonerror="true"/>
-        <exec executable="./contrib/setup-cadical.sh"    dir="${boolector.path}" failonerror="true"/>
-        <exec executable="./contrib/setup-btor2tools.sh" dir="${boolector.path}" failonerror="true"/>
+        <exec executable="./contrib/setup-picosat.sh" dir="${boolector.path}" failonerror="true"/>
+        <exec executable="./contrib/setup-minisat.sh" dir="${boolector.path}" failonerror="true"/>
+        <exec executable="./contrib/setup-cms.sh" dir="${boolector.path}" failonerror="true"/>
+        <exec executable="./contrib/setup-lingeling.sh" dir="${boolector.path}" failonerror="true"/>
+        <exec executable="./contrib/setup-cadical.sh" dir="${boolector.path}" failonerror="true"/>
+        <exec executable="./contrib/setup-btor2tools.sh" dir="${boolector.path}"
+              failonerror="true"/>
         <exec executable="./configure.sh" dir="${boolector.path}" failonerror="true">
             <arg value="-fno-strict-aliasing"/>
             <arg value="-fpic"/>
             <arg value="--shared"/>
         </exec>
         <exec executable="make" dir="${boolector.path}/build/" failonerror="true">
-            <arg value="-j4" />
+            <arg value="-j4"/>
         </exec>
 
         <!-- remove unneeded symbols -->
         <exec executable="strip" dir="${boolector.path}/deps/install/lib/" failonerror="true">
-            <arg value="libpicosat.so" />
+            <arg value="libpicosat.so"/>
         </exec>
         <exec executable="strip" dir="${boolector.path}/deps/install/lib/" failonerror="true">
-            <arg value="libminisat.so" />
+            <arg value="libminisat.so"/>
         </exec>
         <exec executable="strip" dir="${boolector.path}/build/lib/" failonerror="true">
-            <arg value="libboolector.so" />
+            <arg value="libboolector.so"/>
         </exec>
 
         <!-- fix RPATH and library dependencies -->
         <exec executable="patchelf" dir="${boolector.path}/build/lib/" failonerror="true">
-            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
-            <arg value="--replace-needed"/><arg value="libminisat.so.2"/><arg value="libminisat.so"/>
+            <arg value="--set-rpath"/>
+            <arg value="$ORIGIN"/>
+            <arg value="--replace-needed"/>
+            <arg value="libminisat.so.2"/>
+            <arg value="libminisat.so"/>
             <arg value="libboolector.so"/>
         </exec>
 
         <!-- copy library files into directory to be published for IVY -->
-        <copy file="${boolector.path}/deps/install/lib/libminisat.so" tofile="libminisat-${boolector.version}.so"/>
-        <copy file="${boolector.path}/deps/install/lib/libpicosat.so" tofile="libpicosat-${boolector.version}.so"/>
-        <copy file="${boolector.path}/build/lib/libboolector.so"      tofile="libboolector-${boolector.version}.so"/>
+        <copy file="${boolector.path}/deps/install/lib/libminisat.so"
+              tofile="libminisat-${boolector.version}.so"/>
+        <copy file="${boolector.path}/deps/install/lib/libpicosat.so"
+              tofile="libpicosat-${boolector.version}.so"/>
+        <copy file="${boolector.path}/build/lib/libboolector.so"
+              tofile="libboolector-${boolector.version}.so"/>
     </target>
 
     <target name="publish-boolector" depends="package-boolector, load-ivy"
-        description="Publish Boolector binaries to Ivy repository.">
-        <ivy:resolve conf="solver-boolector" file="solvers_ivy_conf/ivy_boolector.xml" />
+            description="Publish Boolector binaries to Ivy repository.">
+        <ivy:resolve conf="solver-boolector" file="solvers_ivy_conf/ivy_boolector.xml"/>
         <publishToRepository solverName="Boolector" solverVersion="${boolector.version}"/>
     </target>
 </project>