HTTPS SSH

ScalaSMT: Satisfiability Modulo Theory in Scala

License: LGPL v3 Run Status Version Coverage

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.6-SNAPSHOT"
    )

The 2.0.6-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 provides some guidelines how to use the library.

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. 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 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)