ScalaSMT: Satisfiability Modulo Theory in Scala
ScalaSMT provides an abstraction over SMTLIB standard for Satisfiability Modulo Theory (SMT) solvers.
Main features of ScalaSMT
- support for SMTLIB2 compliant solvers: Z3, CVC4, SMTInterpol, Yices and MathSAT (OSX and Linux).
- safe resource management using the Scala-ARM library. Resources (solvers and pipes) that are spawned by the library are properly released after usage.
- a Domain Specific Language (DSL) to write logical formulas or terms in many predefined logics (e.g. Integer Arithmetic, Fixed-Sized BitVector, Floating-Point BitVector). This provides some type safety e.g. prevents the user from writing an addition between two boolean terms.
- the ability to extract results produced by the solvers as DSL objects (e.g. values, interpolants and in some cases constant arrays).
- the parsing/pretty printing part of ScalaSMT is developped using the sbt-rats plugin for SBT. This provides a compact and maintainable grammar for SMTLIB syntax and considerably reduces the source code.
- generic interaction with the solvers provided by an Expect-like package (see Expect-for-scala).
- support for 'get-interpolants' commands (in Z3 'get-interpolant' ).
- support for 'get-declarations' command (this is not part of SMTLIB2 but very useful to keep track of what variables are currently declared). Notice that this command keeps tracn of the
push/popcommands issued to the solver.
- support for parsing SMTLIB2 compliant files.
A short tool paper describing ScalaSMT was published at Scala 17 and is available here.
To use ScalaSMT you need:
- a recent version (>= 0.13, >= 1.x) of SBT.
- an SMT-solver (e.g. Z3, CVC4, MathSat, Yices, SMTInterpol)
Add to your
build.sbt file the following dependencies:
libraryDependencies ++= Seq ( ... "org.bitbucket.franck44.scalasmt" %% "scalasmt" % "2.0.9-SNAPSHOT" )
The User Manual provides some guidelines how to use the library.
We use our ScalaSMT abstract SMT-solver in our static analysis tool Skink.
ScalaSMT was orginally forked off Scala SMTLIB (thanks Regis Blanc) in September 2015, but has since evolved to a brand new and redesigned library (including parsing, interaction with the solvers).
ScalaSMT's design was greatly simplified thanks to the following Sbt/Scala plugins/packages:
- the SBT plugin sbt-rats to generate a parser
for the expression grammar smtlib2.syntax.
sbt-rats enables the Rats! parser generator to be used in Scala projects.
- the Kiama library to process the Abstract Syntax Trees (AST) generated by the parser.
Kiama is a Scala library for language processing.
- the expect-for-scala package to programmatically interact with the solvers.
- the Scala-ARM safe resource management library. Resources (solvers and pipes) that are spawned by the library are properly released after usage.
- Add RoundingMode sorts and variables
- Add support for Floating Point Bit Vectors (supported by Z3 and MathSat5)
- Minor improvements
- bug fixes in BitVectors
- 2.0.2 Update documentation and Wiki
- 2.0.1 Move to bitbucket url
- 2.0.0 Add configuration file to configure the solvers and provide a list of enabled solvers (can be used in tests to enable/disable solvers)
- Support for the SMTLIB standard version 2.5
- SMTLIB2 expressions represented with a Scala AST
- Parser turn input stream into AST representation
- Printer turn AST representation into an SMTLIB2 compliant string output
- abstraction layer to communicate with solver processes over their textual input
- Support for Z3, CVC4, SMTInterpol, MathSAT5
- get-interpolants (Z3 and SMTInterpol tested)