# ScalaSMT: Satisfiability Modulo Theory in Scala
[![License: LGPL v3](https://img.shields.io/badge/License-LGPL%20v3-blue.svg)](http://www.gnu.org/licenses/lgpl-3.0)
[![Sonatype Nexus (Releases)](https://img.shields.io/nexus/r/https/oss.sonatype.org/org.bitbucket.franck44.scalasmt/scalasmt_2.12.svg?label=Sonatype%20Nexus%20Latest)]()
[![Sonatype Nexus (Snapshots)](https://img.shields.io/nexus/s/https/oss.sonatype.org/org.bitbucket.franck44.scalasmt/scalasmt_2.12.svg?label=Sonatype%20Nexus%20Current)]()
ScalaSMT provides an abstraction over [SMTLIB](http://smtlib.cs.uiowa.edu) 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](https://github.com/jsuereth/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](https://bitbucket.org/inkytonik/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](https://bitbucket.org/franck44/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](http://science.mq.edu.au/~fcassez/publications.html).
To use ScalaSMT you need:
* a recent version (>= 0.13) of [SBT](http://www.scala-sbt.org/).
* an SMT-solver (e.g. Z3, CVC4)
Add to your `build.sbt` file the following dependencies:
"org.bitbucket.franck44.scalasmt" %% "scalasmt" % "2.0.9-SNAPSHOT"
The `2.0.9-SNAPSHOT` uses the SNAPSHOT version of the repository.
Change this field to the version you want to use.
You can browse the [SNAPSHOT versions](https://oss.sonatype.org/content/repositories/snapshots/org/bitbucket/franck44/scalasmt/scalasmt_2.12/) and the [released versions](https://repo.maven.apache.org/maven2/org/bitbucket/franck44/scalasmt/).
The [User Manual](./wiki/user-manual.md) provides some guidelines how to use the library.
### Related projects
- [Scala SMTLIB](https://github.com/regb/scala-smtlib) by Regis Blanc
- [Scala SMTLIB Interface](https://github.com/dzufferey/scala-smtlib-interface) by Damien Zufferey
We use our ScalaSMT abstract SMT-solver in our static analysis tool [Skink](http://science.mq.edu.au/~fcassez/software-verif.html).
ScalaSMT was orginally forked off [Scala SMTLIB](https://github.com/regb/scala-smtlib) (thanks Regis Blanc) in September 2015, but has since evolved to a brand new and redesigned library.
We use the SBT plugin [sbt-rats](https://bitbucket.org/inkytonik/sbt-rats) to generate a parser
for the expression grammar [smtlib2.syntax](src/main/scala/smtlib/parser/smtlib2.syntax).
[sbt-rats](https://bitbucket.org/inkytonik/sbt-rats) enables the Rats! parser generator to be used in Scala projects.
We use the [Kiama](https://bitbucket.org/inkytonik/kiama) library to process the Abstract Syntax Trees (AST) generated by the parser.
[Kiama](https://bitbucket.org/inkytonik/kiama) is a Scala library for language processing.
Finally, we use the [expect-for-scala](https://bitbucket.org/franck44/expect-for-scala) package to programmatically interact with the solvers.
You can clone the master branch of the [expect-for-scala](https://bitbucket.org/franck44/expect-for-scala) package.
The version of the package used in this build is *1.0-SNAPSHOT* available from
You can issue the 'sbt publishLocal' command to build and make Expect-for-scala available locally.
- 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)