Repository files navigation

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

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

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

JavaSMT can express formulas in the following theories:

• Integer
• Rational
• Bitvector
• Floating Point
• Array
• Uninterpreted Function
• String and RegEx

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.

JavaSMT supports several SMT solvers (seeGetting Started for installation):

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 ofGLIBC_2.28 on Linux,available with Ubuntu 18.04 or later.

² Solver requires at leastGLIBC_2.29/GLIBCXX_3.4.26 orGLIBC_2.34/GLIBCXX_3.4.29,available with Ubuntu 22.04 or later.
³ Solver requires at leastGLIBC_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.

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
• 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, pleaselook for or file an issue.

Interruption using aShutdownNotifier may be used to interrupt a solver from any thread.Formulas are translatable in between contexts/provers/threads usingFormulaManager.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.

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 referencedby the client application, this API is necessary to avoid leaking memory.Note that several solvers already supporthash 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 negligiblecompared to solver-internal memory-consumption when solving a hard SMT query.

• Z3: The parametersolver.z3.usePhantomReferences may be used to controlwhether JavaSMT will attempt to decrease references on Z3 formula objectsonce 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.

Installation is possible viaMaven,Ivy, ormanually.Please see ourGetting Started Guide.

// Instantiate JavaSMT with SMTInterpol as backend (for dependencies cf. documentation)try (SolverContextcontext =SolverContextFactory.createSolverContext(config,logger,shutdownNotifier,Solvers.SMTINTERPOL)) {IntegerFormulaManagerimgr =context.getFormulaManager().getIntegerFormulaManager();// Create formula "a = b" with two integer variablesIntegerFormulaa =imgr.makeVariable("a");IntegerFormulab =imgr.makeVariable("b");BooleanFormulaf =imgr.equal(a,b);// Solve formula, get model, and print variable assignmenttry (ProverEnvironmentprover =context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {prover.addConstraint(f);booleanisUnsat =prover.isUnsat();assert !isUnsat;try (Modelmodel =prover.getModel()) {System.out.printf("SAT with a = %s, b = %s",model.evaluate(a),model.evaluate(b));    }  }}

• Project maintainers:Karlheinz Friedberger andDaniel 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 thecontributors overview.