Tree Interpolation in Vampire
now supports the computation of tree and sequence interpolants.
Vampire reads tree interpolation problems
compatible with the SMT-LIB 1.2 format,
using the input standards introduced in iZ3.
For computing tree interpolants in Vampire,
one should simply invoke Vampire on the command line as follows:
vampire --show_interpolant tree --[vampire/z3] problem.smt
You can download the x86 Linux version of Vampire (version 1.8) here.
Store all files of the archive in the same directory.
To get the most recent updates of Vampire,
visit the Vampire page!
We evaluated tree interpolation in Vampire using two benchmark suites:
One is a collection of 4 examples where quantified reasoning over the array content is needed. These examples are available here.
The other one is a collection of 175 quantifier-free problems over arrays and linear integer arithmetic,
extracted from the bounded model checking of device drivers.
These examples are available upon request.