SMTInterpol

an Interpolating SMT Solver

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 |

See the JavaDOC Documentation for details.

SMTInterpol supports Craig interpolation via an extension of the SMTLIB language. Names of terms asserted in the form *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.

(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`

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) |

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.