This repository contains benchmarks and challenge problems for inductive
theorem provers. The benchmarks are written in a superset of SMTLIB
under the benchmarks/
directory and its subdirectories. Each file contains exactly one problem.
The benchmarks under the
false/
subdirectory are false properties, meant as benchmarks for
counterexample-finding tools.
The original directory contains the original Haskell source
files for many of the problems.
The benchmarks are also available to download in Why3 format, and a CVC4-compatible version of SMTLIB:
- Why3: http://tip-org.github.io/tip-benchmarks-0.2-why3.tar.gz
- CVC4: http://tip-org.github.io/tip-benchmarks-0.2-cvc4.tar.gz
- TIP format: http://tip-org.github.io/tip-benchmarks-0.2.tar.gz
After installing the
TIP tools you can generate the
whole problem set in TIP, Why3 and CVC4 format yourself from the
Haskell sources. To do this run omake.
This may be useful if you want to add your own problems,
but it is not a requirement that they come from a Haskell source file.
Contributions are most encouraged! Any inductive problem, big or small, simple or difficult is welcome.
The simplest method to add new benchmarks is via a github
pull request
to this git repo, adding the problems to the originals/ directory
in either Haskell or TIP format. We can take care of updating the build scripts
to include your new problems.
We're also looking for non-theorem benchmarks to evaluate tools that find counterexamples to false properties.
You are also free to email the maintainers with new problems (or questions):
- Nick Smallbone
nicsma@chalmers.se - Moa Johansson
jomoa@chalmers.se