Deciding Local Theories via E-matching: Experiments

Download artifact: download.

README

CAV 2015 Artifact, accompanying the paper Deciding Local Theory Extensions via E-matching by Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, and Thomas Wies.

  1. Compile SMT solvers
  2. Setup Grasshopper (& generating benchmarks)
  3. Trying individual benchmarks on VM, cross-checking output
  4. Trying all benchmarks
  5. Postprocessing, putting everything together

Depending on how through an evaluation is desired, some the steps might be skipped. We have provided starting point & ending point of each step, so one may can check each individually and in any order.

Step C should help test reuse, Step E to check consistency, both of these can be done on VM. Rest of it for checking reproducibility, which is bit time consuming (esp as it can't be done on VM).

Before continuing, if using VM, please install:

    sudo apt-get install git gnuplot

A. Compile SMT solvers

To skip, use binaries provided in:

    artifact/solvers_and_configurations_forstarexec.zip

Cross-vertification with binaries provided:

cvc4 --show-config (match commit HASH, and build configuration)
z3 -h (match commit HASH)

CVC4

  1. Download source (42f269065fbb9204627a2ce483b27d3bc6fd91f4)

    git clone https://github.com/CVC4/CVC4
    cd CVC4
    git co 42f269065fbb9204627a2ce483b27d3bc6fd91f4
  2. Install build dependencies (see INSTALL file).

    sudo apt-get install automake autoconf libtool libgmp-dev libboost-dev
  3. Compile

    ./autogen.sh
    ./contrib/get-antlr-3.4
    ./configure production-staticbinary <ANTLR flags from last line of prvs command>
    make -j<num_cores>
    strip builds/bin/cvc4    #(to reduce size)
  4. Files of relevance for remaining steps: builds/bin/cvc4

Z3

  1. Download source (cee7dd39444c9060186df79c2a2c7f8845de415b)

    git clone https://github.com/Z3Prover/z3
    cd z3
    git co cee7dd39444c9060186df79c2a2c7f8845de415b
  2. Compile

    Install build dependencies
    python scripts/mk_make.py --static
    Edit builds/config.mk, add -static to LINK_FLAGS
    cd builds; make -j<num_cores>
  3. Files of relevance for remaining steps: builds/z3

B. Setup Grasshopper

To skip, use benchmarks provided in:

    artifact/benchmarks-2015-04-23-514b675-forstarexec.zip
  1. Get source (514b6754bb9cff5efb6d9baf937949719c902e3f)

    git clone https://github.com/wies/grasshopper
    cd grasshopper
    git checkout cav15
  2. Install build dependencies, if not already (see README file)
  3. Compile

    ./build.sh
  4. Run

    ./bin/cav15_generate.sh
  5. Files of relevance for remaining steps:

    out/num_insts.txt
    smtlib/benchmarks-2015-04-23-514b675-forstarexec.zip

C. Trying individual benchmarks

Use

    bash starexec_wrapper.sh <config> <benchmark>

where valid list of config are in

    configs.txt

and valid list of benchmarks are in

    benchmarks.txt

You will also find a script:

    run_all_benchmarks.sh

Using this is not recommended, but we are providing this just in case doing D is not possible. This will invoke starexec_wrapper.sh on all possible benchmarks and configurations with a time limit of 60 seconds and mem limit of 1 GB. The output will also be saved in tmp/out directory. One may extract the csv file in empirical/Job7031_info.zip to cross-check output. In order to match timing information, please follow instruction in Step D.

D. Trying all benchmarks

To skip, use:

    artifact/empirical/Job7031_info.zip
    artifact/empirical/Job7031_output.zip

We used the StarExec platform to do our experiments. This allows anyone else to reproduce the results, including the timing information. Our job can be accessed at

https://www.starexec.org/starexec/secure/details/job.jsp?id=7031

The job is public, just click on the "Guest" link on the bottom to login (or use "public" as both username & password).

To get the output used in Step E, scroll to bottom, look under actions, get the "job output" & "job information (including ids)".

To run a job for cross-checking, you need to get an account (logout of guest account, register using "new user"). Then it is a three step process:

E. Postprocessing, putting everything together

  1. If you did Step B, skip this sub-step. If not, generate num_insts.txt (number of instantiations when doing upfront instantiations -- Y-axis of scatterplots in paper).

    bash grasshopper_reproduce.sh

    Advise being bit patient if using VM, it will sort of hang a bit. It ends up needing swap to finish (but it does finish in a couple of minutes). Alternatively, increase the RAM to 4GB or so.

  2. Dump everything in empirical folder:
  1. Post process. Either step-by-step manually do what empirical/postprocess_starexec_output.sh is doing, or just run the script. Script has comments which explain what each step is about. It will generate the graphs (scatterplot in paper), and data for two tables in the paper (U.tex, P.tex).

For any questions, contact Kshitij Bansal