Institute for Computer Languages
Compilers and Languages Group
Vinter is a Vampire-based tool for interpolation, whose aim is to generate minimal interpolants.
Vinter translates arbitraty proofs into interpolating ones (local proofs), extracts interpolants from local proofs, and minimises interpolants using various measures, such as for example the size of the interpolants or the number of quantifiers used in the interpolants.
Vinter takes an input problem written in either SMT-LIB or TPTP syntax. Proofs are found using either Z3 or Vampire, solving pseudo-boolean optimisation is delegated to Yices, while localising proofs and generating minimal interpolants is done by Vampire.
The latest release of Vinter is: vinter-2012-02-01.tar.gz
Note: To run Vinter, you also need to have the Z3 and Yices executables.
See the examples to try Vinter.
Vinter is based on the technique of playing in the grey area of proofs to find interpolants minimal with respect to various measures.