Adding dReal to JavaSMT #313

build.xml

@@ -31,7 +31,8 @@ SPDX-License-Identifier: Apache-2.0
         runtime-princess,
         runtime-smtinterpol,
         runtime-yices2,
-        runtime-z3
+        runtime-z3,
+        runtime-dreal
     "/>
     <property name="ivy.configuration.main" value="core"/>
     <property name="ivy.configurations" value="build, ${ivy.configuration.main}, ${ivy.solver.configurations}, test, format-source, checkstyle, spotbugs"/>
@@ -81,6 +82,7 @@ SPDX-License-Identifier: Apache-2.0
         <delete includeEmptyDirs="true">
             <fileset dir="." includes="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.so *.dll *.dylib *.jar"/>
             <fileset dir="lib/native/source/libmathsat5j" includes="*.so *.dll *.o"/>
+            <fileset dir="build-deps"/> <!-- remove dReal build files -->
         </delete>
     </target>
 

build/build-publish-solvers.xml

@@ -11,7 +11,7 @@ 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-boolector.xml"/>
     <import file="build-publish-solvers/solver-cvc4.xml"/>
@@ -20,5 +20,6 @@ SPDX-License-Identifier: Apache-2.0
     <import file="build-publish-solvers/solver-opensmt.xml"/>
     <import file="build-publish-solvers/solvers-yices.xml"/>
     <import file="build-publish-solvers/solver-z3.xml"/>
+    <import file="build-publish-solvers/solver-dreal.xml"/>
 
 </project>

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

@@ -0,0 +1,110 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab sts=4 filetype=ant fdm=marker: -->
+<project name="publish-solvers-dreal" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
+
+    <import file="macros.xml"/>
+
+    <!-- SECTION: Publishing dReal
+         ==================================================================
+    -->
+    <target name="package-dreal" depends="">
+        <fail unless="dreal.customRev">
+            Please specify a custom revision with the flag -Ddreal.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>
+
+        <!-- build a version string for dreal -->
+        <property name="dreal.version" value="${dreal.customRev}-g4067225"/>
+        <echo message="Building dReal in version '${dreal.version}'"/>
+
+        <!-- fetch and install libibex and dreal -->
+        <mkdir dir="build-deps"/>
+        <exec executable="curl" dir="build-deps" failonerror="true">
+            <arg value="-O"/>
+            <arg value="-L"/>
+            <arg value="https://launchpad.net/~dreal/+archive/ubuntu/dreal/+files/libibex-dev_2.7.4.20220710184652.git352eeeb2345fb2b7a7ec248b44770d8cdc4a5d67~22.04_amd64.deb"/>
+        </exec>
+        <exec executable="dpkg" dir="build-deps" failonerror="true">
+            <arg value="-x"/>
+            <arg value="libibex-dev_2.7.4.20220710184652.git352eeeb2345fb2b7a7ec248b44770d8cdc4a5d67~22.04_amd64.deb"/>
+            <arg value="."/>
+        </exec>
+        <exec executable="curl" dir="build-deps" failonerror="true">
+            <arg value="-O"/>
+            <arg value="-L"/>
+            <arg value="https://github.com/dreal/dreal4/releases/download/4.21.06.2/dreal_4.21.06.2_amd64.deb"/>
+        </exec>
+        <exec executable="dpkg" dir="build-deps" failonerror="true">
+            <arg value="-x"/>
+            <arg value="dreal_4.21.06.2_amd64.deb"/>
+            <arg value="."/>
+        </exec>
+
+        <property name="path.source" value="${user.dir}/lib/native/source/dreal"/>
+
+        <property name="dreal.install" value="${user.dir}/build-deps/opt/dreal/4.21.06.2"/>
+        <property name="ibex.install" value="${user.dir}/build-deps/opt/libibex/2.7.4"/>
+
+        <!-- compile the JNI code -->
+        <exec executable="g++" dir="${path.source}" failonerror="true">
+            <arg value="-fpic"/>
+            <arg value="-c"/>
+            <arg value="dreal_wrap.cxx"/>
+            <arg value="-I${java.home}/include"/>
+            <arg value="-I${java.home}/include/linux"/>
+            <arg value="-I${ibex.install}/include"/>
+            <arg value="-I${ibex.install}/include/ibex"/>
+            <arg value="-I${ibex.install}/include/ibex/3rd"/>
+            <arg value="-I${dreal.install}/include/"/>
+        </exec>
+
+        <!-- link the JNI code as a new library -->
+        <exec executable="g++" dir="${path.source}" failonerror="true">
+            <arg value="-shared"/>
+            <arg value="dreal_wrap.o"/>
+            <arg value="-ldreal"/>
+            <arg value="-libex"/>
+            <arg value="-o"/>
+            <arg value="libdrealjava.so"/>
+            <arg value="-L${ibex.install}/lib"/>
+            <arg value="-L${dreal.install}/lib/"/>
+        </exec>
+
+        <!-- copy library files to the main directory -->
+        <copy file="${ibex.install}/lib/libibex.so" tofile="libibex-${dreal.version}.so"/>
+        <copy file="${dreal.install}/lib/libdreal.so" tofile="libdreal-${dreal.version}.so"/>
+        <copy file="${path.source}/libdrealjava.so" tofile="libdrealjava-${dreal.version}.so"/>
+
+        <!-- patch dependencies -->
+        <exec executable="patchelf" failonerror="true">
+            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+            <arg value="libibex-${dreal.version}.so"/>
+        </exec>
+        <exec executable="patchelf" failonerror="true">
+            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+            <arg value="libdreal-${dreal.version}.so"/>
+        </exec>
+        <exec executable="patchelf" failonerror="true">
+            <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+            <arg value="libdrealjava-${dreal.version}.so"/>
+        </exec>
+    </target>
+
+    <target name="publish-dreal" depends="package-dreal, load-ivy"
+            description="Publish dReal binaries to Ivy repository.">
+        <ivy:resolve conf="solver-dreal" file="solvers_ivy_conf/ivy_dreal.xml" />
+        <publishToRepository solverName="dReal" solverVersion="${dreal.version}"/>
+    </target>
+</project>

lib/ivy.xml

@@ -41,6 +41,7 @@ SPDX-License-Identifier: Apache-2.0
         <conf name="runtime-cvc5" extends="core" description="only one solver included"/>
         <conf name="runtime-boolector" extends="core" description="only one solver included"/>
         <conf name="runtime-yices2" extends="core" description="only one solver included"/>
+        <conf name="runtime-dreal" extends="core" description="only one solver included"/>
 
         <!-- The normal dependencies with all solvers included. -->
         <conf name="runtime"
@@ -49,7 +50,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- The normal dependencies with all solvers included, except those unter GPL. -->
         <conf name="runtime-without-gpl"
-              extends="runtime-mathsat,runtime-opensmt,runtime-optimathsat,runtime-smtinterpol,runtime-princess,runtime-z3,runtime-cvc4,runtime-cvc5,runtime-boolector"
+              extends="runtime-mathsat,runtime-opensmt,runtime-optimathsat,runtime-smtinterpol,runtime-princess,runtime-z3,runtime-cvc4,runtime-cvc5,runtime-boolector, runtime-dreal"
               description="all solvers included, except those unter GPL"/>
 
         <!-- Dependencies needed for building or running tests. -->
@@ -165,6 +166,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />
         <dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-dreal" rev="4.21.06.2-gf93bdcc" conf="runtime-dreal->solver-dreal" />
 
         <!-- additional JavaSMT components with Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-yices2" rev="4.1.1-59-gaf9c0520c" conf="runtime-yices2->runtime; contrib->sources" />