Skip to content
Initial release of Scala SMT-LIB

This release provides a very extensive support for the
SMT-LIB language version 2.5 (currently in draft mode, but
very close to being final).

SMT-LIB expressions are represented with a Scala AST corresponding
closely to the SMT-LIB grammar. A parser can turn an input stream
into an AST representation, and a printer will turn an AST representation
into a SMT-LIB complient string output.

In addition, Scala SMT-LIB provides an abstraction layer to communicate
with solver processes over their textual input (using system pipes) with
the SMT-LIB language. It comes out of the box with support for
Z3 and CVC4, but more solvers can be added easily as long as they
support SMT-LIB inputs.

Scala SMT-LIB is released under the terms of the MIT license.