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 predicates or terms in many logics. 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).
- 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.
- support for 'get-declarations' command (this is not part of SMTLIB2)
- 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) 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.
Finally, we use the expect-for-scala package to programmatically interact with the solvers. You can clone the master branch of the expect-for-scala package. The version of the package used in this build is 1.0-SNAPSHOT available from https://bitbucket.org/franck44/expect-for-scala. You can issue the 'sbt publishLocal' command to build and make Expect-for-scala available locally.
- 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)