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.