diff --git a/build.gradle b/build.gradle index 9b7b1ad2..2b957e19 100644 --- a/build.gradle +++ b/build.gradle @@ -13,7 +13,6 @@ ext { checkerFrameworkPath = System.getenv('CHECKERFRAMEWORK') ?: "${jsr308}/checker-framework" checkerJar = "${checkerFrameworkPath}/checker/dist/checker.jar" afu = "${jsr308}/annotation-tools/annotation-file-utilities" - z3Jar = "${projectDir}/lib/com.microsoft.z3.jar" lingelingTar = "${projectDir}/lib/lingeling.tar.gz" dljcScript = "${jsr308}/do-like-javac/dljc" @@ -67,7 +66,8 @@ dependencies { implementation 'org.ow2.sat4j:org.ow2.sat4j.core:2.3.6' implementation 'org.ow2.sat4j:org.ow2.sat4j.maxsat:2.3.6' - implementation files(z3Jar) + + implementation 'tools.aqua:z3-turnkey:4.8.17' testImplementation fileTree(dir: "${checkerFrameworkPath}/framework-test/build/libs", include: "framework-test-*.jar") // Mocking library. Used in a couple tests @@ -94,13 +94,6 @@ sourceSets { } } -task buildZ3(type: Exec) { - description 'Build Z3 solver' - onlyIf { !(new File(z3Jar).exists()) } - workingDir './scripts' - commandLine './buildZ3' -} - task buildLingeling(type: Exec) { description 'Build Lingeling solver' onlyIf { !(new File(lingelingTar).exists()) } @@ -163,7 +156,6 @@ test { } compileJava { - dependsOn(buildZ3) dependsOn(buildLingeling) dependsOn(buildDLJC) options.compilerArgs = [ diff --git a/scripts/buildZ3 b/scripts/buildZ3 deleted file mode 100755 index 595552a6..00000000 --- a/scripts/buildZ3 +++ /dev/null @@ -1,67 +0,0 @@ -#!/bin/sh - -# Fail the whole script if any command fails -set -e - -myDir="`dirname $0`" -case `uname -s` in - CYGWIN*) - myDir=`cygpath -m $mydir` - ;; -esac - -if [ "$myDir" = "" ]; -then - myDir="." -fi - -# Note: travis image uses ubuntu 14.04 and will not work with the 16.04 binaries -# 14.04 version seems to work locally on all ubuntu versions above 14.04 -UBUNTU_Z3="https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1-x64-ubuntu-14.04.zip" - -MAC_Z3="https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1-x64-osx-10.11.6.zip" - - -case `uname -s` in - 'Darwin') - Z3_ZIP=$MAC_Z3 - DY_LIB_SUFFIX=dylib - ;; - *) - # Assume it is ubuntu OS. - Z3_ZIP=$UBUNTU_Z3 - DY_LIB_SUFFIX=so - ;; -esac - -CFI=$(cd ${myDir}/../ && pwd) -ROOT=$(cd ${CFI}/../ && pwd) - -# z3 jar file and dylib files should either exist together or not exist at all, -# so just check if the jar file exists. -if [ -e $ROOT/z3/bin/com.microsoft.z3.jar ] ; then - echo "Found existing z3 in $ROOT/z3/bin/, skip downloading z3." -else - echo "Downloading Z3 from $Z3_ZIP..." - echo "Running cmd: (cd $ROOT && wget $Z3_ZIP -O z3.zip && unzip z3.zip && mv $ROOT/z3-* $ROOT/z3)" - (cd $ROOT && wget -q $Z3_ZIP -O z3.zip && unzip z3.zip && mv $ROOT/z3-* $ROOT/z3) - echo "cmd: (cd $ROOT && wget $Z3_ZIP -O z3.zip && unzip z3.zip && mv $ROOT/z3-* $ROOT/z3) Done." - echo "Downloaded z3 into directory $ROOT/z3" -fi - -if [ ! -d $CFI/lib ] ; then - mkdir $CFI/lib -fi - -# Copy build result into CFI lib dir -echo "Copying $ROOT/z3/bin/com.microsoft.z3.jar into $CFI/lib" -(cp $ROOT/z3/bin/com.microsoft.z3.jar $CFI/lib) -echo "Copy done." - -echo "Copying $ROOT/z3/bin/libz3.$DY_LIB_SUFFIX into $CFI/lib" -(cp $ROOT/z3/bin/libz3.$DY_LIB_SUFFIX $CFI/lib) -echo "Copy done." - -echo "Copying $ROOT/z3/bin/libz3java.$DY_LIB_SUFFIX into $CFI/lib" -(cp $ROOT/z3/bin/libz3java.$DY_LIB_SUFFIX $CFI/lib) -echo "Copy done."