In the context of our LPAR paper on
interpolation in Presburger arithmetic, we have implemented a version
of the open-source SMT solver OpenSMT that can extract
Craig interpolants from unsatisfiable problems in quantifier-free
Presburger arithmetic.
Note that this is not an official
version of OpenSMT, and that the implementation is not maintained
anymore. Do not call it "OpenSMT" in publications! If you are searching
for stable interpolating SMT solvers, you might rather consider tools
like Princess or MathSAT.
You can currently download binaries for Linux (on 32-bit and 64-bit x86 platforms):
Because our implementation is based on a development version of OpenSMT, we only provide the source code on request.
After unpacking any of the packages from above, you can change into the
directory opensmtint_x86_*
and start OpenSMT by calling ./opensmt
<filename>
.
Given an unsatisfiable problem in the QF_LIA
logic (that
is partitioned as demonstrated in the examples/
directory), OpenSMT will write interpolants to the file inter.smt
.
We have compared the performance of our interpolation procedure with the following tools:
Results of the experiments (as an Excel spreadsheet), which were done on an Intel Xeon X5667 4-core machine with 3.07GHz, heap-space limited to 12GB, running Linux, with a timeout of 900s.