JavaSMT

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

• D. Baier, D. Beyer, and K. Friedberger. JavaSMT 3: Interacting with SMT Solvers in Java. In Proc. CAV, LNCS 12760, pages 1-13, 2021. Springer.
• E. G. Karpenkov, K. Friedberger, and D. Beyer. JavaSMT: A Unified Interface for SMT Solvers in Java. In Proc. VSTTE, LNCS 9971, pages 139–148, 2016. Springer.

Feature overview

JavaSMT can express formulas in the following theories:

• Integer
• Rational
• Bitvector
• Floating Point
• Array
• Uninterpreted Function
• String and RegEx
• Separation Logic (experimental)

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.

Solver support for different Operating System and Architectures

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

SMT Solver	Linux x64	Linux arm64	Windows x64	Windows arm64	MacOS x64	MacOS arm64	Description
Bitwuzla	✔️²	✔️²	✔️				a fast solver for bitvector logic
Boolector	✔️						a fast solver for bitvector logic, misses formula introspection, deprecated
CVC4	✔️
CVC5	✔️	✔️	✔️	✔️	✔️	✔️
MathSAT5	✔️³	✔️³	✔️		maybe⁴
OpenSMT	✔️²	✔️²
OptiMathSAT	✔️						based on MathSAT5, with support for optimization queries
Princess	✔️	✔️	✔️	✔️	✔️	✔️	Java-based SMT solver
SMTInterpol	✔️	✔️	✔️	✔️	✔️	✔️	Java-based SMT solver
Yices2	✔️		maybe		maybe⁴
Z3	✔️³	✔️³	✔️	✔️	✔️	✔️	mature and well-known solver
Z3_WITH_INTERPOLATION	✔️	✔️					an older version of Z3 that still provides interpolation support

We support a reasonable list of operating systems and versions.

• Our main target is Linux (mainly Ubuntu or comparable Linux distributions). Windows 10/11 and macOS are supported for several SMT solvers.
• Our main development architecture is x64 (x86-64). We also provide some solvers for ARM64 (AArch64 for ARMv8-A), e.g., Java-based SMT solvers, Z3, and MathSAT. If a specific operating system or architecture is missing and required, please do not hesitate and open an issue!

On all operating systems and architectures, JavaSMT requires Java 11 or newer. Unless otherwise noted, the solver requires a minimum of GLIBC_2.28 on Linux, available with Ubuntu 18.04 or later.

² Solver requires at least GLIBC_2.29/GLIBCXX_3.4.26 or GLIBC_2.34/GLIBCXX_3.4.29, available with Ubuntu 22.04 or later.
³ Solver requires at least GLIBC_2.38/GLIBCXX_3.4.31, available with Ubuntu 24.04 or later.
⁴ We do not provide a signed solver library for macOS. The user needs to compile and sign it.

Solver Features

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

• 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 structure
• Unsatisfiable core generation
• Formula transformation using built-in tactics
• Formula introspection using visitors

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 Solver	Concurrent context usage⁵	Concurrent prover usage⁶
Bitwuzla	✔️
Boolector	✔️
CVC4	✔️	✔️
CVC5	❓
MathSAT5	✔️
OpenSMT	❓
OptiMathSAT	✔️
Princess	✔️
SMTInterpol	✔️
Yices2
Z3	✔️

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.

• 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.
• CVC4, CVC5, Bitwuzla, OpenSMT: Solvers using SWIG bindings do perform garbage collection.
• Other native SMT solvers: we do not perform garbage collection.

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));
    }
  }
}

You can find several example implementations in the folder org/sosy_lab/java_smt/example. These include examples for the usage of many of JavaSMTs solvers and features, for example:

• AllSatExample: showcasing the usage of the AllSat feature, returning all satisfiable assignments for an input query. JavaSMT is capable of returning AllSat for many solvers even without them directly supporting this feature.
• FormulaClassifier: showcases the usage of our formula visitor to classify the logic of an input SMT file.
• Interpolation: presents how to utilize Craig-, sequential-, and tree-interpolation.
• OptimizationFormulaWeights: shows how the weighting of constraints can be optimized in optimization solving, helping the solver in finding a result.
• OptimizationIntReal: presents optimization solving for integer and real logics.
• PrettyPrinter: showcases how to parse user-given SMT input into a pretty format.
• SimpleUserPropagator: shows an example of a user propagator, prohibiting variables and/or expressions from being set to true. This can be used to guide an SMT solver in its solving process. More examples can be found in the folder nqueens_user_propagator.
• SolverOverviewTable: prints out all available SMT solvers, including their theories and features. This can be used to determine which solvers are available on any machine executing it.

Furthermore, JavaSMT provides users with additional features available for many solvers:

• Debug-Mode: setting the option useDebugMode=true, in the configuration used to create a SolverContext, applies additional checks to catch common usage errors. The checks performed by this option are solver-sensitive and throw exceptions on operations that are disallowed by a particular solver. For example, for most solvers, adding a constraint to a ProverEnvironment may only be allowed iff the constraint has been built by the same SolverContext that also created the used ProverEnvironment. Violating this rule while in debug-mode with a solver that does not allow this throws a IllegalArgumentException with information about the problem.
• Synchronization: setting the option synchronize=true, in the configuration used to create a SolverContext, all solver actions are synchronized with the owning instance being the SolverContext. This allows concurrent access, but strictly sequentializes all operations.
• Statistics: setting the option collectStatistics=true, in the configuration used to create a SolverContext, counts all operations and interactions towards the SMT solver of this context. These statistics can be access in the SolverContext.
• Logging: setting the option useLogger=true, in the configuration used to create a SolverContext, logs all solver actions. Logging operations might slow down usage of JavaSMT though.
• Assumption solving: in case an SMT solver does not support assumption solving natively, we automatically add this feature seamlessly through a self-developed layer. No difference in usage can be observed from a users' perspective.
• AllSat: in case an SMT solver does not support assumption solving natively, we automatically add this feature seamlessly through a self-developed layer. No difference in usage can be observed from a users' perspective.
• Formula visitation: we allow the inspection, traversal, and modification of formulas through our formula-visitor, as long as the chosen SMT solver supports this feature. Users can utilize many pre-built features based on this visitor like BooleanFormulaManager.toDisjunctionArgs(), returning a set of formulas such that a disjunction over them is equivalent to the input formula, or FormulaManager. extractVariablesAndUFs(), which can be used to extract the names of all free variables and UFs in a formula. The visitor-pattern can also be used with user-defined operations.

Many more options are available to configure SMT solvers by setting them in the Configuration given to an SolverContext, including SMT solvers native configuration options.

Authors

• Project maintainers: Karlheinz Friedberger and Daniel Baier
• Former project maintainer: George Karpenkov
• Initial codebase, many design decisions: Philipp Wendler
• Contributions: Bajczi Levente, Daniel Raffler, Martin Spiessl, Thomas Stieglmaier, and many others. For a full list, see the contributors overview.