HTTPS SSH
# 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)]() [![Run Status](https://img.shields.io/shippable/57497cfa2a8192902e21b58c/master.svg?label=Shippable)]() [![Coverage](https://api.shippable.com/projects/57497cfa2a8192902e21b58c/coverageBadge)]() [![Codacy Badge](https://api.codacy.com/project/badge/Grade/5fcaa378ace247158023c85e7968dca8)](https://www.codacy.com/app/franck.cassez/scalasmt?utm_source=franck44@bitbucket.org&utm_medium=referral&utm_content=franck44/scalasmt&utm_campaign=Badge_Grade) [![Codacy Badge](https://api.codacy.com/project/badge/Coverage/5fcaa378ace247158023c85e7968dca8)](https://www.codacy.com/app/franck.cassez/scalasmt?utm_source=franck44@bitbucket.org&utm_medium=referral&utm_content=franck44/scalasmt&utm_campaign=Badge_Coverage) 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). ### Requirements To use ScalaSMT you need: * a recent version (>= 0.13) of [SBT](http://www.scala-sbt.org/). * an SMT-solver (e.g. Z3, CVC4) ### Installation Add to your `build.sbt` file the following dependencies: ~~~ libraryDependencies ++= Seq ( ... "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/). ### Usage 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 ### Applications We use our ScalaSMT abstract SMT-solver in our static analysis tool [Skink](http://science.mq.edu.au/~fcassez/software-verif.html). ### Credits 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 [https://bitbucket.org/franck44/expect-for-scala](https://bitbucket.org/franck44/expect-for-scala). You can issue the 'sbt publishLocal' command to build and make Expect-for-scala available locally. ### Changelog #### v2.0 - 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) #### v1.0 - 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)