Tags: epfl-lara/scala-smtlib
Tags
SMT-LIB version 0.2 * Constructors and extractors for the standard theories (except Floating point) of SMT-LIB 2.5 * Experimental support for non-standardized theories such as Strings and Sets. * More robust parser and printers. * Bug fixes, mostly small edge cases and weird symbol names.
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.