SMTInterpol
an Interpolating SMT Solver

Command Line Interface

SMTInterpol can be used from command line using a SMTLIB input script. After downloading the JAR file, you can run SMTInterpol from command line as
java -jar smtinterpol.jar input.smt2
Without input file, SMTInterpol reads from standard input. This can be used in interactive mode. According to the standard, SMTInterpol replies to every command unless the user sets the option :print-success to false
The solver supports the following command line options:
Option Value Description Equivalent SMTLIB option
-q none Do not print debugging and info messages. :set-verbosity 3
-v none Print debugging and info messages. :set-verbosity 5
-t positive number Set the timeout for a satisfiability check. :timeout arg
-r positive number Set the random seed. :random-seed arg

API

See the JavaDOC Documentation for details.

Interpolation

SMTInterpol supports Craig interpolation via an extension of the SMTLIB language. Names of terms asserted in the form
(assert (! t :named p))
can be used to describe interpolation partitions. The syntax for generating sequence interpolants is
(get-interpolants p1 p2 .. pn)
where each pi is either the name of a term asserted in the way described above or a conjunction of such names. SMTInterpol also supports tree interpolants. Our format is described in an SMTLIB proposal.

Additional SMTLIB Commands

Besides the get-interpolants command SMTInterpol supports additional non-standard SMTLIB commands. The following table summarizes these commands and describes their effects.
Command Argument(s) Description
get-interpolants Partition description Compute an inductive sequence of interpolants
include File name Include the file in the current solver
reset None Reset the whole solver
get-model None Get a model for a satisfiable formula
simplify Term Interface to the formula simplifier (experimental)
timed command(s) Report the duration of the arguments (in seconds)

Extended SMTLIB Logics

SMTInterpol extends the integer logics (QF_LIA, QF_UFLIA) defined by the SMTLIB standard to close them under interpolation. The division-by-constant and modulo-by-constant operators are added.
Additionally, SMTInterpol supports the logic QF_UFLIRA. This logic combines uninterpreted functions with mixed linear integer and real arithmetic.
 

Last modified: Tue May 7 18:42:11 CEST 2019   Valid XHTML 1.0 TransitionalValid CSS!