Home

Awesome

<!-- This file is part of JavaSMT, an API wrapper for a collection of SMT solvers: https://github.com/sosy-lab/java-smt SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org> SPDX-License-Identifier: Apache-2.0 -->

JavaSMT

Build Status Build Status on Windows Test Coverage Apache 2.0 License Maven Central

JavaSMT is a common API layer for accessing various SMT solvers. The API is optimized for performance (using JavaSMT has very little runtime overhead compared to using the solver API directly), customizability (features and settings exposed by various solvers should be visible through the wrapping layer) and type-safety (it shouldn't be possible to add boolean terms to integer ones at compile time) sometimes at the cost of verbosity.

Quick links

Getting Started | Documentation | Known Issues | Documentation for Developers | Changelog | Configuration Options

References

Feature overview

JavaSMT can express formulas in the following theories:

The concrete support for a certain theory depends on the underlying SMT solver. Only a few SMT solvers provide support for theories like Arrays, Floating Point, String or RegEx.

Currently JavaSMT supports several SMT solvers (see Getting Started for installation):

SMT SolverLinux64Windows64MacOSDescription
Bitwuzla:heavy_check_mark::heavy_check_mark:a fast solver for bitvector logic
Boolector:heavy_check_mark:a fast solver for bitvector logic, misses formula introspection, deprecated
CVC4:heavy_check_mark:
CVC5:heavy_check_mark:
MathSAT5:heavy_check_mark::heavy_check_mark:
OpenSMT:heavy_check_mark:
OptiMathSAT:heavy_check_mark:based on MathSAT5, with support for optimization queries
Princess:heavy_check_mark::heavy_check_mark::heavy_check_mark:Java-based SMT solver
SMTInterpol:heavy_check_mark::heavy_check_mark::heavy_check_mark:Java-based SMT solver
Yices2:heavy_check_mark:maybe
Z3:heavy_check_mark::heavy_check_mark::heavy_check_mark:mature and well-known solver

We support a reasonable list of operating systems and versions. Our main target is Linux (64-bit, mainly Ubuntu 22.04 or newer, several solver libraries also work on Ubuntu 18.04, or comparable Linux distributions). Windows 10/11 and MacOS are supported for several SMT solvers (with limited hardware for testing). If a specific operating system is missing and required, please do not hesitate and open an issue!

The following features are supported (depending on the used SMT solver):

We aim for supporting more important features, more SMT solvers, and more systems. If something specific is missing, please look for or file an issue.

Multithreading Support

SMT SolverConcurrent context usage¹Concurrent prover usage²
Bitwuzla:heavy_check_mark:
Boolector:heavy_check_mark:
CVC4:heavy_check_mark::heavy_check_mark:
CVC5:question:
MathSAT5:heavy_check_mark:
OpenSMT:question:
OptiMathSAT:heavy_check_mark:
Princess:heavy_check_mark:
SMTInterpol:heavy_check_mark:
Yices2
Z3:heavy_check_mark:

Interruption using a ShutdownNotifier may be used to interrupt a solver from any thread. Formulas are translatable in between contexts/provers/threads using FormulaManager.translateFrom().

¹ Multiple contexts, but all operations on each context only from a single thread. ² Multiple provers on one or more contexts, with each prover using its own thread.

Garbage Collection in Native Solvers

JavaSMT exposes an API for performing garbage collection on solvers implemented in a native language. As a native solver has no way of knowing whether the created formula object is still referenced by the client application, this API is necessary to avoid leaking memory. Note that several solvers already support hash consing and thus, there is never more than one copy of an identical formula object in memory. Consequently, if all created formulas are later re-used (or re-created) in the application, it is not necessary to perform any garbage collection at all. Additionally, the memory for formulas created on user-side (i.e., via JavaSMT) is negligible compared to solver-internal memory-consumption when solving a hard SMT query.

Getting started

Installation is possible via Maven, Ivy, or manually. Please see our Getting Started Guide.

Usage

// Instantiate JavaSMT with SMTInterpol as backend (for dependencies cf. documentation)
try (SolverContext context = SolverContextFactory.createSolverContext(
        config, logger, shutdownNotifier, Solvers.SMTINTERPOL)) {
  IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager();

  // Create formula "a = b" with two integer variables
  IntegerFormula a = imgr.makeVariable("a");
  IntegerFormula b = imgr.makeVariable("b");
  BooleanFormula f = imgr.equal(a, b);

  // Solve formula, get model, and print variable assignment
  try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
    prover.addConstraint(f);
    boolean isUnsat = prover.isUnsat();
    assert !isUnsat;
    try (Model model = prover.getModel()) {
      System.out.printf("SAT with a = %s, b = %s", model.evaluate(a), model.evaluate(b));
    }
  }
}

Authors