This repository contains tools for working with the TIP suite of benchmarks for inductive theorem provers. The tools are currently rough around the edges but include:
tip
- transform a TIP file or translate it to various formatstip-ghc
- translate a Haskell file to TIP formattip-spec
- invent conjectures about a TIP file
With Haskell installed and this repository cloned:
stack setup
stack install
The tools will be put in your ~/.local/bin
directory.
If you are modifying the TIP parser, you will also need to have BNFC installed, and to run ./make_parser.sh whenever you change the parser.
You can find a large collection of problems in TIP format in
the benchmarks repository
under the directory benchmarks
. You can use the tip
tool
to run transformations on these problems or translate them to another format.
To translate a TIP file to some other format, run:
tip name-of-file.smt2 --why
to convert it to WhyML format;tip name-of-file.smt2 --smtlib
to convert it to a CVC4-compatible version of SMTLIB;tip name-of-file.smt2 --isabelle
to convert it to Isabelle;tip name-of-file.smt2 --haskell
to convert it to Haskell (plus scaffolding for running QuickSpec).
You can also use tip
to run various transformations on the input problem.
For example, tip name-of-file.smt2 --commute-match --simplify-aggressively
will first simplify the structure of match
expressions in the problem
and then run a general simplification pass. For a list of all passes
run tip --help
.
To translate a Haskell file to TIP, run tip-ghc name-of-file.hs
.
Properties to be proved must be written in a special syntax; to
see some examples, look at
the benchmarks repository
under the directory originals
.