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.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 f)) can be used to describe interpolation partitions. The syntax for the corresponding interpolation call is (get-interpolants p*) where p is either the name of a term asserted in the way described above or a conjunction of such names. 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: Wed Mar 22 20:25:10 CET 2017   Valid XHTML 1.0 TransitionalValid CSS!