JavaSMT

Unified Java API for SMT solvers.

Project Description & Philosophy

JavaSMT is a common API layer for accessing various SMT solvers.

It was created out of our experience integrating and using different SMT solvers in the CPAchecker project. The library is developed for medium to large software projects which require access to 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.

Supported Solvers

Currently, we support the following SMT solvers:

• Z3
• MathSAT
• OptiMathSAT
• SMTInterpol
• Princess

Support for CVC4 is planned in the near future (cf. #2).

Supported Features

JavaSMT can express formulas in the following theories:

• Integer
• Rational
• Bitvector
• Floating point
• Array
• Uninterpreted Function
• Bitvectors

The following features are supported:

• Satisfiability checking
• Quantifiers and quantifier elimination
• Incremental solving with assumptions
• Incremental solving with push/pop
• Multiple independent contexts
• Model generation
• Interpolation, including tree and sequential
• Formula transformation using built-in tactics
• Formula introspection using visitors

Multithreading Support

All solvers except for MathSAT5 fully support multithreading, provided that different threads use different contexts, and all operations on a single context are performed from a single thread. Interruption using ShutdownNotifier may be used to interrupt a a solver from any 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 due to the hash consing usage inside the solvers, 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.

Z3

The parameter solver.z3.usePhantomReferences may be used to control whether JavaSMT will attempt to decrease references on Z3 formula objects once they are no longer referenced.

MathSAT5

Currently we do not support performing garbage collection for MathSAT5.

Installation

Automatic Installation from Maven Central

If you use Maven/Gradle/SBT/etc to build your project, a dependency to JavaSMT can be added using a single configuration item.

For Maven:

<dependency>
  <groupId>org.sosy-lab</groupId>
  <artifactId>java-smt</artifactId>
  <version>1.0.1</version>
</dependency>

Currently, only SMTInterpol is automatically fetched from Maven Central, and shared object for other solvers would have to be installed manually: see the section "Manual Installation" below.

Automatic Installation using Ivy

If your build tool supports fetching packages from Apache Ivy, you can point it to Sosy-Lab Ivy repository, which would automatically fetch JavaSMT and all of its dependencies.

After the repository URL is configured, you only need to add the following dependency:

<dependency org="org.sosy_lab" name="javasmt" rev="0.60" />

Manual Installation

JARs for JavaSMT and its dependencies can be downloaded from our Ivy repository manually. In order to perform the manual installation, the following steps should be followed:

• The desired version has to be chosen. Latest version can be found by looking at the Ivy index.
• Suppose the version 1.0.1 was chosen. Ivy description file ivy-1.0.1.xml can be consulted in order to determine all the files which should be fetched.
• The artifacts tag specifies what files the release depends on. In the example case, those are javasmt-1.0.1.jar and (optionally) javasmt-1.0.1-sources.jar, located in the same directory.
• Finally, the dependencies can be manually followed and resolved. E.g. in the example, Z3 version z3-4.4.1-1394-gd12efb6 is specified, which is described by the corresponding XML file, specifying what binaries should be fetched from the corresponding directory.

Binaries for Native Solvers (MathSAT and Z3)

When using Ivy for installation on a 64-bit Linux platform, solver binaries for native solvers are downloaded automatically. Everything should work as is after installation.

Without Ivy you need to download and install the binaries manually as described above under Manual Installation. You can either copy them into the directory of the JavaSMT JAR file, or in a directory ../native/<arch>-<os>/ relative to the directory of the JAR file. See NativeLibraries documentation for more details on which path is searched.

For systems other than 64-bit Linux (e.g., Windows, or 32-bit systems) we do not provide binaries so you need to compile them for yourself. For Z3, download it and build it with the flags --staticlib --java --git-describe according to its documentation. Then install the files libz3.(so|dll) and libz3java.(so|dll) as described above. You might also experiment with using its latest binary release, though we recommend the latest git version of Z3 due to its large number of fixes and improvements. In order to compile MathSAT binaries, see the comments in the lib/native/source/libmathsat5j/compile.sh script.

Solvers which run directly on JDK (currently Princess and SMTInterpol) do not require any configuration and work out of the box.

Quickstart Guide

Initialization

Below is a small example showing how to initialize the library using the entry point SolverContextFactory:

package org.sosy_lab.solver.test;

import org.sosy_lab.common.ShutdownManager;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.BasicLogManager;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.solver.SolverContextFactory;
import org.sosy_lab.solver.SolverContextFactory.Solvers;
import org.sosy_lab.solver.api.SolverContext;

public class TestApp {
  public static void main(String[] args) throws InvalidConfigurationException {
    Configuration config = Configuration.fromCmdLineArguments(args);
    LogManager logger = BasicLogManager.create(config);
    ShutdownManager shutdown = ShutdownManager.create();

    // SolverContext is a class wrapping a solver context.
    // Solver can be selected either using an argument or a configuration option
    // inside `config`.
    SolverContext context = SolverContextFactory.createSolverContext(
        config, logger, shutdown.getNotifier(), Solvers.SMTINTERPOL);
  }
}

JavaSMT relies on three dependencies from the SoSy-Lab Common library. These dependencies are:

• Configuration: SMT solvers expose many different configuration options, and using the configuration object they can be easily populated by the client, either from the command line or from .properties file.
• LogManager: JavaSMT can be configured to provide extensive logging for the operations related to all SMT queries. If you already use your own logging framework, you just have to create a wrapper implementing LogManager interface. BasicLogManager is an implementation that delegates to the standard JDK logging API.
• ShutdownNotifier from a ShutdownManager: Many SMT queries can take a very long time, potentially more than the user is willing to wait. What's more, for a solver implemented in the native code usual ways of interrupting a Java process (e.g. interrupt signal) would not work. Shutdown manager provides a solution to gracefully request termination, and JavaSMT and the solvers will try to respond to such requests as soon as possible.

Solving Constraints

Once the SolverContext is initialized, we can start posing queries to the solver. In this example, we want to find a satisfying example for a constraint over integers a, b and c:

a + b = c \/ a + c = 2 * b

Creating the required constraint is straightforward:

    // Assume we have a SolverContext instance.
    FormulaManager fmgr = context.getFormulaManager();

    BooleanFormulaManager bmgr = fmgr.getBooleanFormulaManager();
    IntegerFormulaManager imgr = fmgr.getIntegerFormulaManager();

    IntegerFormula a = imgr.makeVariable("a"),
                   b = imgr.makeVariable("b"),
                   c = imgr.makeVariable("c");
    BooleanFormula constraint = bmgr.or(
        imgr.equal(
            imgr.add(a, b), c
        ),
        imgr.equal(
            imgr.add(a, c), imgr.multiply(imgr.makeNumber(2), b)
        )
    );

Note the types of the formulas: IntegerFormula and BooleanFormula. Using different classes for different types of formulas adds additional guarantees at compile-time: unless and unsafe cast is used, it is impossible to e.g. add an integer to a boolean using JavaSMT API.

Once the constraint is generated, we can solve it and get the model:

    try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
      prover.addConstraint(constraint);
      boolean isUnsat = prover.isUnsat();
      if (!isUnsat) {
        Model model = prover.getModel();
      }
    }

Try-with-resources syntax will dispose of the prover once solving is finished.

Once the model is obtained we can get values from it either by iterating through all of the returned data, or by querying for the variables we need:

    BigInteger value = model.evaluate(a);

For further information, look at our full example HoudiniApp, or at the JavaDoc.

Further Documentation

• JavaDoc
• Changelog
• Documentation For Developers
• Known Issues

Authors

• Project maintainer: George Karpenkov
• Initial codebase, many design decisions: Philipp Wendler
• Contributions: Thomas Stieglmaier, Karlheinz Friedberger, and others.

Additional Acknowledgements

• Profiled with jProfiler Java Profiler.