# ScalaSMT: Satisfiability Modulo Theory in Scala [![License: LGPL v3](]( [![Sonatype Nexus (Releases)](]() [![Sonatype Nexus (Snapshots)](]() [![Run Status](]() [![Coverage](]() [![Codacy Badge](]( [![Codacy Badge](]( 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]( ### Requirements To use ScalaSMT you need: * a recent version (>= 0.13) of [SBT]( * 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]( and the [released versions]( ### Usage The [User Manual](./wiki/ provides some guidelines how to use the library. ### Related projects - [Scala SMTLIB]( by Regis Blanc - [Scala SMTLIB Interface]( by Damien Zufferey ### Applications We use our ScalaSMT abstract SMT-solver in our static analysis tool [Skink]( ### Credits ScalaSMT was orginally forked off [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]( to generate a parser for the expression grammar [smtlib2.syntax](src/main/scala/smtlib/parser/smtlib2.syntax). [sbt-rats]( enables the Rats! parser generator to be used in Scala projects. We use the [Kiama]( library to process the Abstract Syntax Trees (AST) generated by the parser. [Kiama]( is a Scala library for language processing. 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 []( 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)