HTTPS SSH

ScalaSMT: Satisfiability Modulo Theory in Scala

License: LGPL v3
Sonatype Nexus (Releases)
Sonatype Nexus (Snapshots)

Bitbucket Pipelines

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 logical formulas or terms in many predefined logics (e.g. Integer Arithmetic, Fixed-Sized BitVector, Floating-Point BitVector). 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 and in some cases constant arrays).
  • 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 (in Z3 'get-interpolant' ).
  • support for 'get-declarations' command (this is not part of SMTLIB2 but very useful to keep track of what variables are currently declared). Notice that this command keeps tracn of the push/pop commands issued to the solver.
  • 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, >= 1.x) of SBT.
  • an SMT-solver (e.g. Z3, CVC4, MathSat, Yices, SMTInterpol)

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 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 (including parsing, interaction with the solvers).

ScalaSMT's design was greatly simplified thanks to the following Sbt/Scala plugins/packages:
- 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.
- the Kiama library to process the Abstract Syntax Trees (AST) generated by the parser.
Kiama is a Scala library for language processing.
- the expect-for-scala package to programmatically interact with the solvers.
- the Scala-ARM safe resource management library. Resources (solvers and pipes) that are spawned by the library are properly released after usage.

Changelog

v2.2

  • 2.2.0-SNAPSHOT
    • refactor configuration file, options, logics (issue #23)
    • add support for CVC4 1.6 (see issue #24)

v2.1

  • 2.1.2-SNAPSHOT
    • Check that the solver supports logic and options when creating a SMTSolver with a configuration. (issue #18)
    • Add support for UnSat core (issues #16)
    • Fix minor bugs (issues #13, #15)
  • 2.1.1

    • Add RoundingMode sorts and variables
  • 2.1.0

    • Add support for Floating Point Bit Vectors (supported by Z3 and MathSat5)
    • Minor improvements
    • bug fixes in BitVectors

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)