Build scripts and Ivy configuration.

build.xml

@@ -0,0 +1,72 @@
+
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab : -->
+<project name="JavaSMT Solver Library" basedir="." default="build">
+    <!-- Include a file in which all properties can be overridden.
+         This file won't get checked in and can be used to change properties
+         locally for one machine if necessary. -->
+    <property file="build.properties"/>
+    <property environment="env"/>
+
+    <property name="ivy.configurations" value="build, runtime, test, checkstyle, findbugs"/>
+
+    <import file="build/build-version.xml"/>
+    <import file="build/build-ivy.xml"/>
+    <import file="build/build-compile.xml"/>
+    <import file="build/build-jar.xml"/>
+    <import file="build/build-junit.xml"/>
+    <import file="build/build-checkstyle.xml"/>
+    <import file="build/build-findbugs.xml"/>
+    <import file="build/build-publish.xml"/>
+    <import file="build/build-publish-solvers.xml"/>
+    <import file="build/build-format-source.xml"/>
+
+    <path id="classpath">
+        <pathelement location="${class.dir}"/>
+        <fileset dir="${ivy.lib.dir}" includes="runtime/*.jar test/*.jar build/annotations.jar build/auto-service.jar build/auto-common.jar build/error_prone_annotations.jar"/>
+    </path>
+
+
+    <!-- Main targets -->
+
+    <target name="clean" description="Clean">
+        <delete includeEmptyDirs="true">
+            <fileset dir="." includes="${class.dir}/** ${ivy.module}-*.jar ivy-*.xml *.so *.jar"/>
+        </delete>
+    </target>
+
+    <target name="build" depends="build-project, build-documentation" description="Build"/>
+
+    <target name="dist" depends="jar, sources" description="Make a distributable release"/>
+
+    <target name="tests" depends="unit-tests-coverage" description="Run all tests"/>
+
+    <target name="publish" depends="tests, dist, publish-artifacts" description="Publish current version to Ivy repository"/>
+
+    <!-- Auxiliary targets -->
+
+    <target name="init" depends="determine-version">
+        <echo message="Building ${ant.project.name} ${version}"/>
+        <mkdir dir="${class.dir}"/>
+    </target>
+
+    <target name="build-dependencies" depends="init, resolve-dependencies"/>
+
+    <target name="build-documentation" depends="build-project">
+        <echo message="running OptionCollector..." level="info"/>
+
+        <!-- the output of OptionCollector is written into "doc/ConfigurationOptions.txt" -->
+        <java classname="org.sosy_lab.common.configuration.OptionCollector"
+            fork="true"
+            output="${class.dir}/org/sosy_lab/solver/ConfigurationOptions.txt" append="false"
+            failonerror="true"
+            logError="true">
+
+            <classpath refid="classpath"/>
+
+            <!-- "-v" is a optional param for verbose output of OptionCollector -->
+            <!-- <arg value="-v"/> -->
+        </java>
+        <echo message="Options collected." level="info"/>
+    </target>
+
+</project>

build/build-checkstyle.xml

@@ -0,0 +1,28 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab filetype=ant : -->
+<project name="checkstyle" basedir="."
+        xmlns:cs="antlib:com.puppycrawl.tools.checkstyle">
+
+    <!-- Targets for running Checkstyle. -->
+
+    <!-- Keep this file synchronized between SoSy-Lab Common, CPAchecker and VerifierCloud. -->
+
+    <target name="checkstyle" depends="resolve-dependencies">
+        <path id="checkstyle.lib.path">
+            <fileset dir="${ivy.lib.dir}/checkstyle" includes="*.jar"/>
+        </path>
+        <taskdef resource="checkstyletask.properties" uri="antlib:com.puppycrawl.tools.checkstyle" classpathref="checkstyle.lib.path"/>
+
+        <cs:checkstyle config=".settings/checkstyle.xml">
+            <fileset dir="${source.dir}" includes="**/*.java" excludes="**/*Test.java"/>
+            <formatter type="xml" toFile="Checkstyle.xml"/>
+        </cs:checkstyle>
+        <xslt in="Checkstyle.xml" out="Checkstyle.html" style="build/checkstyle.xsl"/>
+
+        <cs:checkstyle config=".settings/checkstyle.test.xml">
+            <fileset dir="${source.dir}" includes="**/*Test.java"/>
+            <formatter type="xml" toFile="Checkstyle.Test.xml"/>
+        </cs:checkstyle>
+        <xslt in="Checkstyle.Test.xml" out="Checkstyle.Test.html" style="build/checkstyle.xsl"/>
+    </target>
+</project>

build/build-compile.xml

@@ -0,0 +1,38 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab filetype=ant : -->
+<project name="compile" basedir=".">
+
+    <!-- Targets for compilation. -->
+
+    <!-- Keep this file synchronized between SoSy-Lab Common, CPAchecker and VerifierCloud. -->
+
+    <!-- These properties can be overridden from including file. -->
+    <property name="source.format" value="1.7"/>
+    <property name="source.dir" value="src"/>
+    <property name="class.format" value="1.7"/>
+    <property name="class.dir" value="bin"/>
+
+    <path id="errorprone">
+        <pathelement location="${ivy.lib.dir}/build/error_prone_ant.jar"/>
+    </path>
+
+    <!-- We use error-prone as the compiler, cf. http://errorprone.info/ -->
+    <target name="build-project" depends="build-dependencies">
+        <depend srcdir="${source.dir}" destdir="${class.dir}"/>
+        <javac debug="true"
+               debuglevel="source,lines,vars"
+               destdir="${class.dir}"
+               source="${source.format}"
+               target="${class.format}"
+               includeAntRuntime="false"
+               compiler="com.google.errorprone.ErrorProneAntCompilerAdapter"
+               encoding="UTF-8">
+            <src path="${source.dir}"/>
+            <classpath refid="classpath"/>
+            <compilerarg value="-Xlint"/>
+            <compilerarg value="-Xlint:-processing"/>
+            <compilerarg value="-Werror"/>
+            <compilerclasspath refid="errorprone"/>
+        </javac>
+    </target>
+</project>

build/build-findbugs.xml

@@ -0,0 +1,62 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab filetype=ant : -->
+<project name="findbugs" basedir=".">
+
+    <!-- Targets for running FindBugs. -->
+
+    <!-- Keep this file synchronized between SoSy-Lab Common, CPAchecker and VerifierCloud. -->
+    <path id="findbugs.classpath">
+        <fileset dir="${ivy.lib.dir}/findbugs" includes="*.jar"/>
+    </path>
+
+    <target name="run-findbugs" depends="jar">
+        <delete file="FindBugs.html"/>
+        <taskdef name="findbugs" classname="edu.umd.cs.findbugs.anttask.FindBugsTask" classpathref="findbugs.classpath"/>
+        <findbugs
+                output="xml:withMessages"
+                outputFile="FindBugs.xml"
+                excludeFilter=".settings/FindBugs.exclude.xml"
+                warningsProperty="findbugs.warnings">
+            <auxClasspath refid="classpath" />
+            <sourcePath path="${source.dir}" />
+            <class location="${jar.file}" />
+            <classpath refid="findbugs.classpath" />
+        </findbugs>
+    </target>
+
+    <target name="findbugs-report" if="findbugs.warnings">
+        <echo>FindBugs found warnings, generating report.</echo>
+        <xslt in="FindBugs.xml" out="FindBugs.html">
+            <style><javaresource classpathref="findbugs.classpath" name="fancy.xsl"/></style>
+        </xslt>
+    </target>
+
+    <target name="findbugs" depends="run-findbugs, findbugs-report" description="Run FindBugs and generate report."/>
+
+    <target name="run-findbugs-diff" depends="jar">
+        <delete file="FindBugs.diff.html"/>
+        <taskdef name="findbugs" classname="edu.umd.cs.findbugs.anttask.FindBugsTask" classpathref="findbugs.classpath"/>
+        <findbugs
+                output="xml:withMessages"
+                outputFile="FindBugs.diff.xml"
+                excludeFilter=".settings/FindBugs.exclude.xml"
+                warningsProperty="findbugs.newwarnings"
+                baselineBugs="FindBugs.known.xml">
+            <auxClasspath refid="classpath" />
+            <sourcePath path="${source.dir}" />
+            <class location="${jar.file}" />
+            <classpath refid="findbugs.classpath" />
+        </findbugs>
+    </target>
+
+    <target name="findbugs-diff-report" if="findbugs.newwarnings">
+        <echo>FindBugs found new warnings, generating report.</echo>
+        <xslt in="FindBugs.diff.xml" out="FindBugs.diff.html">
+            <style><javaresource classpathref="findbugs.classpath" name="fancy.xsl"/></style>
+        </xslt>
+    </target>
+
+    <target name="findbugs-diff" depends="run-findbugs-diff, findbugs-diff-report" description="Run FindBugs and generate report with newly found warnings."/>
+
+    <target name="findbugs-full" depends="findbugs, findbugs-diff" description="Run FindBugs and generate full report and report with newly found warnings."/>
+</project>

build/build-format-source.xml

@@ -0,0 +1,54 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab filetype=ant : -->
+<project name="format-source" basedir=".">
+
+    <!-- Targets for formatting source code. -->
+
+    <!-- Keep this file synchronized between SoSy-Lab Common, CPAchecker and VerifierCloud. -->
+
+    <target name="format-source" depends="resolve-dependencies"
+        description="Reormat the whole source">
+        <fileset dir="${source.dir}" id="source.files">
+            <include name="**/*.java" />
+        </fileset>
+        <pathconvert property="source.files" refid="source.files" pathsep=" "/>
+        <java fork="true" jar="${ivy.lib.dir}/build/google-java-format.jar">
+            <arg value="-i"/>
+            <arg line="${source.files}"/>
+        </java>
+    </target>
+
+    <target name="format-diff" depends="resolve-dependencies"
+        description="Reformat all lines that are currently changed but not yet committed">
+        <exec executable="git"
+                outputproperty="git.diff"
+                failonerror="false" failifexecutionfails="false"
+                logError="false" error="/dev/null">
+            <arg value="diff"/>
+            <arg value="--diff-cmd"/>
+            <arg value="diff"/>
+            <arg value="-x"/>
+            <arg value="-u0"/>
+            <arg value="${source.dir}"/>
+        </exec>
+        <exec executable="git"
+                outputproperty="git.diff"
+                failonerror="false" failifexecutionfails="false"
+                logError="false" error="/dev/null">
+            <arg value="diff"/>
+            <arg value="--cached"/>
+            <arg value="-U0"/>
+            <arg value="${source.dir}"/>
+        </exec>
+
+        <condition property="diff" value="${git.diff}" else="${git.diff}">
+            <not><equals arg1="${git.diff}" arg2=""/></not>
+        </condition>
+
+        <exec executable="build/google-java-format-diff.py"
+                inputstring="${diff}">
+            <arg value="-i"/>
+            <arg value="-p1"/>
+        </exec>
+    </target>
+</project>

build/build-ivy.xml

@@ -0,0 +1,65 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab filetype=ant : -->
+<project name="ivy" basedir="."
+         xmlns:ivy="antlib:org.apache.ivy.ant">
+
+    <!-- Targets for managing dependencies with Ivy. -->
+
+    <!-- Keep this file synchronized between SoSy-Lab Common, CPAchecker, JavaSMT and VerifierCloud. -->
+
+    <!-- These properties can be overridden from including file. -->
+    <property name="ivy.version" value="2.3.0"/> <!-- Change version number here to use a newer version of Ivy. -->
+    <!-- <property name="ivy.disable" value=""/> --> <!-- Disable ivy completely. -->
+    <property name="ivy.repo.url" value="http://www.sosy-lab.org/ivy"/>
+    <property name="ivy.lib.dir" value="lib/java"/>
+    <property name="ivy.configurations" value="build, runtime, test, findbugs"/>
+    <property name="ivy.settings.file" value="ivysettings.xml"/>
+
+    <property name="ivy.jar.dir" value="${ivy.lib.dir}/build"/>
+    <property name="ivy.jar.file" value="ivy.jar"/>
+    <available file="${ivy.jar.dir}/${ivy.jar.file}" property="ivy.jar.present"/>
+    <available file="${ivy.lib.dir}-contrib" property="ivy.contrib.present"/>
+
+    <property environment="env"/>
+    <condition property="tmp.ivy.cache.dir" value="${env.IVY_CACHE_DIR}" else="${user.home}/.ivy2/cache">
+        <isset property="env.IVY_CACHE_DIR" />
+    </condition>
+    <property name="ivy.cache.dir" location="${tmp.ivy.cache.dir}" />
+
+    <!-- If necessary, download Ivy from web site so that it does not need to be installed. -->
+    <target name="bootstrap-ivy" unless="ivy.jar.present">
+        <mkdir dir="${ivy.jar.dir}"/>
+        <echo message="Downloading ivy..."/>
+        <get src="${ivy.repo.url}/org.apache.ivy/ivy/ivy-${ivy.version}.jar" dest="${ivy.jar.dir}/${ivy.jar.file}" usetimestamp="true"/>
+    </target>
+
+    <!-- Load the Ivy plugin for Ant so the Ivy tasks are available. -->
+    <target name="load-ivy" depends="bootstrap-ivy">
+        <path id="ivy.lib.path">
+            <fileset dir="${ivy.jar.dir}" includes="${ivy.jar.file}"/>
+        </path>
+        <taskdef resource="org/apache/ivy/ant/antlib.xml" uri="antlib:org.apache.ivy.ant" classpathref="ivy.lib.path"/>
+        <ivy:settings file="${ivy.settings.file}"/>
+    </target>
+
+    <!-- Ask Ivy to get all the dependencies for us -->
+    <target name="resolve-dependencies" depends="load-ivy, update-contrib" unless="ivy.disable">
+        <echo message="Downloading and installing dependencies with Ivy..."/>
+        <ivy:resolve conf="${ivy.configurations}" log="download-only"/>
+        <ivy:retrieve sync="true" overwriteMode="different" pattern="${ivy.lib.dir}/[conf]/[artifact](-[classifier]).[ext]"/>
+    </target>
+
+    <target name="report-dependencies" depends="resolve-dependencies" description="Generate dependencies report">
+      <ivy:report graph="false" dot="true" conf="${ivy.configurations}, contrib"/>
+    </target>
+
+    <!-- Update additional resources if they were downloaded previously. -->
+    <target name="update-contrib" if="ivy.contrib.present">
+        <antcall target="install-contrib"/>
+    </target>
+
+    <target name="install-contrib" depends="load-ivy" unless="ivy.disable" description="Retrieve sources and docs for external libraries">
+        <ivy:resolve conf="contrib" log="download-only"/>
+        <ivy:retrieve sync="true" pattern="${ivy.lib.dir}-contrib/[artifact](-[classifier]).[ext]"/>
+    </target>
+</project>

build/build-jar.xml

@@ -0,0 +1,47 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+<!-- vim: set tabstop=8 shiftwidth=4 expandtab filetype=ant : -->
+<project name="jar" basedir=".">
+
+    <!-- Targets for generating JAR files. -->
+
+    <!-- Keep this file synchronized between SoSy-Lab Common, CPAchecker and VerifierCloud. -->
+
+    <!-- These properties can and should be overridden from including file. -->
+    <property name="class.main" value=""/>
+    <property name="project.url" value=""/>
+    <!--<property name="jar.excludes" value="**/*Test.class **/*Test$*.class"/>-->
+
+    <target name="jar" depends="determine-version,build" description="Create a runnable JAR file">
+        <property name="jar.file" value="${ivy.module}-${version}.jar"/>
+        <copy todir="${class.dir}"><fileset dir="." includes="META-INF/**"/></copy>
+        <manifestclasspath property="classpath.jar" jarfile="${ivy.lib.dir}/runtime/${jar.file}" maxParentLevels="0">
+            <classpath><fileset dir="${ivy.lib.dir}/runtime" includes="*.jar"/></classpath>
+        </manifestclasspath>
+        <jar basedir="${class.dir}/"
+                includes="**"
+                excludes="${jar.excludes}"
+                destfile="${jar.file}"
+                whenmanifestonly="fail">
+
+            <manifest>
+                <attribute name="Class-Path" value="${classpath.jar}"/>
+                <attribute name="Main-Class" value="${class.main}"/>
+                <attribute name="Implementation-Title" value="${ant.project.name}"/>
+                <attribute name="Implementation-Version" value="${version}"/>
+                <attribute name="Implementation-URL" value="${project.url}"/>
+            </manifest>
+        </jar>
+    </target>
+
+    <target name="sources" depends="determine-version, resolve-dependencies">
+        <jar basedir="${source.dir}/"
+                destfile="${ivy.module}-${version}-sources.jar"
+                includes="**/*.java"
+                whenmanifestonly="fail">
+            <manifest>
+                    <attribute name="Implementation-Title" value="${ant.project.name}"/>
+                    <attribute name="Implementation-Version" value="${version}"/>
+            </manifest>
+        </jar>
+    </target>
+</project>