sosy-lab · winnieros · Jun 26, 2023 · Jul 21, 2023 · Jul 24, 2023 · Jul 24, 2023
diff --git a/.classpath b/.classpath
@@ -28,6 +28,8 @@ SPDX-License-Identifier: Apache-2.0
  <classpathentry kind="lib" path="lib/java/runtime-princess/scala-library.jar"/>
  <classpathentry kind="lib" path="lib/java/runtime-princess/princess-smt-parser_2.13.jar"/>
  <classpathentry kind="lib" path="lib/java/runtime-princess/java-cup-runtime.jar"/>
+ <classpathentry kind="lib" path="lib/java/runtime-apron/gmp.jar"/>
+ <classpathentry kind="lib" path="lib/java/runtime-apron/apron.jar"/>
  <classpathentry kind="lib" path="lib/java/runtime-z3/com.microsoft.z3.jar" sourcepath="lib/java-contrib/com.microsoft.z3-sources.jar"/>
  <classpathentry kind="lib" path="lib/java/runtime-cvc4/CVC4.jar"/>
  <classpathentry kind="lib" path="lib/java/runtime-cvc5/cvc5.jar"/>

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
diff --git a/build.xml b/build.xml
@@ -31,7 +31,8 @@ SPDX-License-Identifier: Apache-2.0
  runtime-princess,
  runtime-smtinterpol,
  runtime-yices2,
- runtime-z3
+ runtime-z3,
+ runtime-apron
  "/>
  <property name="ivy.configuration.main" value="core"/>
  <property name="ivy.configurations" value="build, ${ivy.configuration.main}, ${ivy.solver.configurations}, test, format-source, checkstyle, spotbugs"/>

diff --git a/build/build-publish-solvers.xml b/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-apron.xml"/>
 
 </project>
diff --git a/build/build-publish-solvers/solver-apron.xml b/build/build-publish-solvers/solver-apron.xml
@@ -0,0 +1,108 @@
+<?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: -->
+<!-- SECTION: Publishing Apron {{{1
+ ==================================================================
+-->
+<project name="publish-solvers-apron" basedir="." xmlns:ivy="antlib:org.apache.ivy.ant">
+ <import file="macros.xml"/>
+
+ <target name="package-apron" depends="">
+ <!-- Copy Apron repository to the root folder along with the version postfix. -->
+ <fail unless="apron.path">
+ Please specify the path to Apron with the flag -Dapron.path=/path/to/apron.
+ The path has to point to the root Apron folder, i.e.,
+ a checkout of the official git repositoy from 'https://github.com/antoinemine/apron'.
+ Note that shell substitutions do not work and a full absolute path has to be specified.
+ </fail>
+ <fail unless="apron.customRev">
+ Please specify a custom revision with the flag -Dapron.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>
+ <!-- get a naive version -->
+ <exec executable="git" dir="${apron.path}" outputproperty="apron.revision"
+ failonerror="true">
+ <arg value="show"/>
+ <arg value="-s"/>
+ <arg value="--format=%h"/>
+ </exec>
+ <property name="apron.version" value="${apron.customRev}-g${apron.revision}"/>
+ <echo message="Building Apron in version '${apron.version}'"/>
+
+ <!-- build apron -->
+ <exec executable="./configure" dir="${apron.path}" failonerror="true">
+ <arg value="-java-prefix"/>
+ <arg value="/usr/lib/jvm/java-11-openjdk-amd64"/>
+ <arg value="--no-cxx"/>
+ <arg value="--no-ocaml"/>
+ <arg value="--no-ppl"/>
+ <arg value="--prefix"/>
+ <arg value="${apron.path}/install"/>
+ <arg value="--no-ocaml-plugins"/>
+ <arg value="--no-ocamlfind"/>
+ </exec>
+ <exec executable="make" dir="${apron.path}" failonerror="true">
+ </exec>
+
+ <!-- fix RPATH and library dependencies -->
+ <exec executable="patchelf" dir="${apron.path}/apron" failonerror="true">
+ <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+ <arg value="libapron.so"/>
+ </exec>
+ <exec executable="patchelf" dir="${apron.path}/box" failonerror="true">
+ <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+ <arg value="libboxD.so"/>
+ </exec>
+ <exec executable="patchelf" dir="${apron.path}/japron" failonerror="true">
+ <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+ <arg value="libjapron.so"/>
+ </exec>
+ <exec executable="patchelf" dir="${apron.path}/japron" failonerror="true">
+ <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+ <arg value="libjgmp.so"/>
+ </exec>
+ <exec executable="patchelf" dir="${apron.path}/octagons" failonerror="true">
+ <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+ <arg value="liboctD.so"/>
+ </exec>
+ <exec executable="patchelf" dir="${apron.path}/newpolka" failonerror="true">
+ <arg value="--set-rpath"/><arg value="$ORIGIN"/>
+ <arg value="libpolkaMPQ.so"/>
+ </exec>
+
+ <!-- copy library files into directory to be published for IVY -->
+ <copy file="${apron.path}/japron/apron.jar"
+ tofile="apron-${apron.version}.jar"/>
+ <copy file="${apron.path}/japron/gmp.jar"
+ tofile="gmp-${apron.version}.jar"/>
+ <copy file="${apron.path}/apron/libapron.so"
+ tofile="libapron-${apron.version}.so"/>
+ <copy file="${apron.path}/box/libboxD.so"
+ tofile="libboxD-${apron.version}.so"/>
+ <copy file="${apron.path}/japron/libjapron.so"
+ tofile="libjapron-${apron.version}.so"/>
+ <copy file="${apron.path}/japron/libjgmp.so"
+ tofile="libjgmp-${apron.version}.so"/>
+ <copy file="${apron.path}/octagons/liboctD.so"
+ tofile="liboctD-${apron.version}.so"/>
+ <copy file="${apron.path}/newpolka/libpolkaMPQ.so"
+ tofile="libpolkaMPQ-${apron.version}.so"/>
+ </target>
+
+ <target name="publish-apron" depends="package-apron, load-ivy"
+ description="Publish Apron binaries to Ivy repository.">
+ <ivy:resolve conf="solver-apron" file="solvers_ivy_conf/ivy_apron.xml" />
+ <publishToRepository solverName="Apron" solverVersion="${apron.version}"/>
+ </target>
+</project>
diff --git a/lib/ivy.xml b/lib/ivy.xml
@@ -18,7 +18,8 @@ SPDX-License-Identifier: Apache-2.0
  <license name="The Apache Software License, Version 2.0" url="http://www.apache.org/licenses/LICENSE-2.0.txt"/>
 
  <description homepage="https://github.com/sosy-lab/java-smt">
- Java wrapper for SMT solvers like Z3, MathSAT5, SMTInterpol, Princess, CVC4, CVC5, Boolector, and Yices2.
+ Java wrapper for SMT solvers like Z3, MathSAT5, SMTInterpol, Princess, CVC4, CVC5,
+ Boolector, Yices2, OpenSMT and Apron.
  </description>
  </info>
 
@@ -41,6 +42,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-apron" extends="core" description="only one solver included"/>
 
  <!-- The normal dependencies with all solvers included. -->
  <conf name="runtime"
@@ -49,7 +51,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-apron"
  description="all solvers included, except those unter GPL"/>
 
  <!-- Dependencies needed for building or running tests. -->
@@ -165,6 +167,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-apron" rev="0.9.14-g718470b" conf="runtime-apron->solver-apron" />
 
  <!-- 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" />

diff --git a/lib/native/x86_64-linux/libapron.so b/lib/native/x86_64-linux/libapron.so
@@ -0,0 +1 @@
+lib/java/runtime-apron/libapron.so
diff --git a/lib/native/x86_64-linux/libboxD.so b/lib/native/x86_64-linux/libboxD.so
@@ -0,0 +1 @@
+lib/java/runtime-apron/libboxD.so
diff --git a/lib/native/x86_64-linux/libjapron.so b/lib/native/x86_64-linux/libjapron.so
@@ -0,0 +1 @@
+lib/java/runtime-apron/libjapron.so
diff --git a/lib/native/x86_64-linux/libjgmp.so b/lib/native/x86_64-linux/libjgmp.so
@@ -0,0 +1 @@
+lib/java/runtime-apron/libjgmp.so
diff --git a/lib/native/x86_64-linux/liboctD.so b/lib/native/x86_64-linux/liboctD.so
@@ -0,0 +1 @@
+lib/java/runtime-apron/liboctD.so
diff --git a/lib/native/x86_64-linux/libpolkaMPQ.so b/lib/native/x86_64-linux/libpolkaMPQ.so
@@ -0,0 +1 @@
+lib/java/runtime-apron/libpolkaMPQ.so
diff --git a/solvers_ivy_conf/ivy_apron.xml b/solvers_ivy_conf/ivy_apron.xml
@@ -0,0 +1,41 @@
+<?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
+-->
+
+<ivy-module version="2.0"
+ xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+ xsi:noNamespaceSchemaLocation="http://ant.apache.org/ivy/schemas/ivy.xsd">
+ <info organisation="org.sosy_lab" module="javasmt-solver-apron">
+ <license name="GNU Lesser General Public License" url="https://github.com/antoinemine/apron/blob/master/COPYING"/>
+ <description>
+ Apron Numerical Abstract Domain library.
+ Apron provided with GNU Lesser General Public License.
+ </description>
+ </info>
+
+ <configurations>
+ <conf name="solver-apron" />
+ </configurations>
+
+ <publications defaultconf="solver-apron">
+ <artifact name="apron" conf="solver-apron"/>
+ <artifact name="gmp" conf="solver-apron"/>
+ <artifact name="libjapron" conf="solver-apron" type="shared-object" ext="so"/>
+ <artifact name="libjgmp" conf="solver-apron" type="shared-object" ext="so"/>
+ <artifact name="libapron" conf="solver-apron" type="shared-object" ext="so"/>
+ <artifact name="libboxD" conf="solver-apron" type="shared-object" ext="so"/>
+ <artifact name="liboctD" conf="solver-apron" type="shared-object" ext="so"/>
+ <artifact name="libpolkaMPQ" conf="solver-apron" type="shared-object" ext="so"/>
+ </publications>
+
+ <dependencies></dependencies>
+
+</ivy-module>
diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java
@@ -29,6 +29,7 @@
 import org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext;
 import org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext;
 import org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext;
+import org.sosy_lab.java_smt.solvers.apron.ApronSolverContext;
 import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext;
 import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext;
 import org.sosy_lab.java_smt.solvers.cvc5.CVC5SolverContext;
@@ -57,7 +58,8 @@ public enum Solvers {
  BOOLECTOR,
  CVC4,
  CVC5,
- YICES2
+ YICES2,
+ APRON
  }
 
  @Option(secure = true, description = "Export solver queries in SmtLib format into a file.")
@@ -290,6 +292,9 @@ private SolverContext generateContext0(Solvers solverToCreate)
  case BOOLECTOR:
  return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader);
 
+ case APRON:
+ return ApronSolverContext.create(nonLinearArithmetic, shutdownNotifier, logger);
+
  default:
  throw new AssertionError("no solver selected");
  }