Package org.smtlib.solvers

package 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. The available solvers are not necessarily SMT-LIB compliant; the wrappers implemented in this package translate to and from the given SMT solvers, so as to present an SMT-LIB-compliant interface to the user, while using the solving capability of the solver itself.
  • Classes
    Class
    Description
    Printer
     
    Solver_altergo
    The adapter for Alt-Ergo (developed against 2.6.3 on Linux), run as alt-ergo --input smtlib2 --output smtlib2, reading the script from standard input.
    Solver_bitwuzla
    This class is an adapter for Bitwuzla (bit-vectors, floating-point, arrays and uninterpreted functions -- no arithmetic logics, no datatypes).
    Solver_cvc5
    This class is an adapter for cvc5, on the assumption that it is (or should be) a fully SMT-LIB compliant solver: it is a concrete, silent inheritor of AbstractSolver — only the startup command line (cvc5 needs --incremental to accept push/pop at all, and --quiet to suppress informational stderr chatter that would otherwise fool SolverProcess's stdout/stderr-preference heuristic) and Solver_cvc5.start() (process lifecycle) are overridden.
    Solver_simplify
    The adapter that drives the Simplify solver.
    Solver_simplify.Translator
     
    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_smtinterpol
    This class is an adapter for SMTInterpol (a Java SMT solver launched as java -jar smtinterpol-VERSION.jar, not a native executable): it is a concrete, silent inheritor of AbstractSolver -- the base launch command is declared in jsmtlib.properties via org.smtlib.solver_smtinterpol-2.5.command (see SMT.startSolver's %exec% placeholder substitution), so only the conditional timeout flag and Solver_smtinterpol.start()/AbstractSolver.exit() (process lifecycle) are handled here, besides the get- command checks below.
    Solver_test
    This class is a Solver implementation that simply type-checks formulae and checks that commands are used correctly; it does not do any proving.
    Solver_yices2
    This class is an adapter that takes the SMT-LIB ASTs and translates them into yices2 commands
    Solver_yices2_2_6
    yices2 2.6.5: by default it answers get-model in yices's own model format, not SMT-LIB's; with --smt2-model-format it answers (model (define-fun ...) ...), whose wrapper AbstractSolver#modelResponse removes.
    Solver_z3_4_3
    This class is an adapter that takes the SMT-LIB ASTs and translates them into Z3 commands
    Solver_z3_4_3_2
    This is a special handler for Z3 4.3.2, as opposed to other revisions of Z3 4.3.
    Solver_z3_4_5
    z3 4.5.0: as recent z3, except that it writes echo's text unquoted even with SMTLIB2_COMPLIANT (4.6 and later quote it), so where it ends cannot be found (#136), the response to echo is its argument; and it rejects every check-sat-assuming (see translate)
    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.