Uses of Package
org.smtlib.solvers

Packages that use org.smtlib.solvers
Package
Description
org.smtlib.solvers
This package implements various instances of org.smtlib.ISolver, which are specific solvers that wrap and interact with various off-the-shelf SMT solvers currently available.
  • Classes in org.smtlib.solvers used by org.smtlib.solvers
    Class
    Description
    Printer
     
    Solver_smt
    This class is an adapter that takes the SMT-LIB ASTs and translates them into SMT commands over a solver process speaking plain SMT-LIB, for a solver assumed to be fully SMT-LIB compliant.
    Solver_yices2
    This class is an adapter that takes the SMT-LIB ASTs and translates them into yices2 commands
    Solver_z3_4_3
    This class is an adapter that takes the SMT-LIB ASTs and translates them into Z3 commands
    Solver_z3_recent
    This class is an adapter for recent z3 versions (empirically verified against 4.8.12 and 4.10.2), on the assumption that they are (or should be) fully SMT-LIB compliant: it is a concrete, silent inheritor of AbstractSolver -- only the startup command line and Solver_z3_recent.start()/AbstractSolver.exit() (process lifecycle) are overridden.