Lemma Synthesis

Requirements

• Python 3.5 or above
• Z3Py
• CVC4 1.9

Installation

• Clone or download the repo
• Enter top-level directory: cd lemma-synthesis
• Install the requirements: pip3 install -r requirements.txt
  • Alternatively, for Z3Py you can build z3 from source with python bindings: https://github.com/Z3Prover/z3. Use the --python flag while building.
• Dowload the latest nightly build binary of cvc4 from https://cvc4.github.io/downloads.html and add it to PATH: execute export PATH ="/path/to/cvc4binary":$PATH or add it to ~/.bashrc and then do source ~/.bashrc. Alternatively, you can build from source.
  • The specific commit used to compile all examples in the Makefile is 2faf908e
• Make sure that cvc4 --version succeeds. You may want to rename the binary or alias it to cvc4.
• Add the path to the src/ folder to PYTHONPATH: execute export PYTHONPATH ="/path/to/src":$PYTHONPATH or add it to ~/.bashrc and then do source ~/.bashrc.

Experiments

• To run all the benchmarks, simply run ./test_all.sh in the top-level directory

  • Command timeout is needed. On MacOS, run the following in order to obtain the timeout command:
    • brew install coreutils
    • sudo ln -s /usr/local/bin/gtimeout /usr/local/bin/timeout

• The benchmarks are in the experiments directory.

• To run all benchmarks first change the directory to experiments and then run make -s -i

  • NOTE: Ignoring the -i flag will cause make to abort if any of the examples fail.

• To cleanup all files generated by running examples: make clean

• To run indidvidual examples: python3 <filename>.py

• To run CVC4 files directly using SyGuS: cvc4 --lang=sygus2 <filename>.sy

  • add option --sygus-stream to print outputs indefinitely
  • add option --sygus-abort-size=<n> with previous option to print outputs up to size n

• NOTE: The project uses temporary files to store and read data during execution. Therefore, it is not advisable to run multiple instances of the same example as they will each write to the same temporary files.