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.smt2Without 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
p
i 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.