JavaSMT Solver Library
JavaSMT is a generic API allowing unified access to different SMT solvers.
All the interaction with a solver is performed through the
SolverContext interface, which encapsulates a
single context.
SolverContext instances are created using
SolverContextFactory.
| Package | Description |
|---|---|
| org.sosy_lab.java_smt |
JavaSMT: a generic SMT solver API.
|
| org.sosy_lab.java_smt.api |
The core interfaces for abstracting from SMT solvers and providing a common API for all solvers.
|
| org.sosy_lab.java_smt.api.visitors |
The visitors of this package allow for efficient traversal, manipulation and transformation of
formulas.
|
| org.sosy_lab.java_smt.basicimpl |
Abstract base classes for easier implementation of a solver backend.
|
| org.sosy_lab.java_smt.basicimpl.tactics |
Default tactics implementations (formula-to-formula transformations).
|
| org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper |
Wrapper-classes to guarantee identical behavior for all solvers.
|
| org.sosy_lab.java_smt.delegate.debugging | |
| org.sosy_lab.java_smt.delegate.logging |
Wraps the proving environment with loggers.
|
| org.sosy_lab.java_smt.delegate.statistics |
The classes of this package wrap the whole proving environment and measure all accesses to it.
|
| org.sosy_lab.java_smt.delegate.synchronize |
The classes of this package wrap the whole solver context and all corresponding proving
environment and synchronize all accesses to it.
|
| org.sosy_lab.java_smt.example |
Some basic examples for using Java-SMT.
|
| org.sosy_lab.java_smt.example.nqueens_user_propagator |
Some basic examples for using Java-SMT.
|
| org.sosy_lab.java_smt.test |
Solver-independent tests and test utilities for the solver API.
|
| org.sosy_lab.java_smt.utils |
Utility classes implementing algorithms based on the API of JavaSMT.
|