Outline

Prerequisites

Build Z3 for Java

  • Packages may be required

    $ sudo apt-get install g++
    $ sudo apt-get install automake

  • Get Z3 for Java and follow the instructions

Build CVC4

  • Packages may be required

    $ sudo apt-get install libgmp3-dev
    $ sudo apt-get install autoconf
    $ sudo apt-get install swig
    $ sudo apt-get install libboost-all-dev
    $ sudo apt-get install gcj-4.7
    $ sudo apt-get install libtool

  • Get CVC4 source and build

    $ cd /contrib
    $ ./get-antlr-3.4
    $ cd ..
    $ ./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3 --enable-language-bindings=java --prefix=/your/path/to/cvc4/
    $ make
    $ make install
    $ cd /your/path/tocvc4/
    $ cd lib/jni
    $ ln -s libcvc4jni.so libcvc4java.so

Build Cascade

  • Checkout Cascade from svn repository

    $ svn co https://subversive.cims.nyu.edu/cascade/branches/wwang1109/trunk cascade

  • Configure maven via ~/.m2/settings

  • Set LD_LIBRARY_PATH in ~/.profile to the paths of lib of z3, lib and lib/jni of cvc4

  • Build core

    $ cd core
    $ mvn clean install

  • Build cvc4-plugin

    $ cd cvc4-plugin
    $ mvn clean install

  • Build z3-plugin

    $ cd z3-plugin
    $ mvn clean install

  • Build c

    $ cd c
    $ mvn clean install

Run Cascade in command line

  • First, be sure you are in the c/ directory, otherwise, when run following instructions, you may get warnings like:

    Can't read plugins directory: ../z3-plugin/target
    Can't read plugins directory: ../cvc4-plugin/target

  • Cascade can be run using "c/target/cascade.sh". Use "--help" to determine options.

    $ sh target/cascade.sh --help

  • As an alternative to cascade.sh, you can run java directly. For example:

    $ java -ea -cp /our/path/to/z3/build/com.microsoft.z3.jar: /your/path/to/cvc4/share/java/ CVC4.jar: /your/path/to/cascade/c/target/cascade-c-0.0.2-SNAPSHOT-rbuildNumber.jar edu.nyu.cascade.c.Main --help

Run Cascade in Eclipse

  • In the Package Explorer, Select c > src/main/java > edu.nyu.cascade.c > Main.java

  • Right-click Main.java. Select Run As > Run Configurations...

  • Add "-ea" to the VM arguments

  • Set the Program arguments tab as the arguments to cascade.sh. For example: "--help" or "/your/path/to/cascade/c/src/test/resources/c/test/minicase_bug/funcCall_test.ctrl"

  • If there's a link error to cvc4java, change the line 467 in TheoremProverImpl.java in cvc4-plugin/src/main/java/edu/nyu/cascade/cvc4 from "System.loadLibrary("cvc4java")" to "System.loadLibrary("cvc4jni")"