SMT solving
SMT-LIB
A standard language and benchmark format for SMT solvers.
Definition
SMT-LIB
SMT-LIB defines a concrete syntax, commands, logic names, and semantics used to exchange SMT problems.
A file can declare variables, assert constraints, request a satisfiability result, and ask for a model. Solver support varies across commands and logics.
01
Example
The command (assert (> x 3)) adds an integer constraint when x has sort Int.
02
Important distinction
Parsing an SMT-LIB command does not prove that the solver implements every semantic case it can parse.
After reading this article, you should be able to
- Define SMT-LIB in the sense used on this site.
- Read the declarations, assertions, and check-sat command in a short SMT-LIB file.