Uses of Class
org.smtlib.AbstractSolver

Packages that use AbstractSolver

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.

Uses of AbstractSolver in org.smtlib.solvers

Subclasses of AbstractSolver in org.smtlib.solvers

Modifier and Type	Class	Description
class	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.
class	Solver_bitwuzla	This class is an adapter for Bitwuzla (bit-vectors, floating-point, arrays and uninterpreted functions -- no arithmetic logics, no datatypes).
class	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.
class	Solver_simplify	The adapter that drives the Simplify solver.
class	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.
class	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()/exit() (process lifecycle) are handled here, besides the get- command checks below.
class	Solver_yices2	This class is an adapter that takes the SMT-LIB ASTs and translates them into yices2 commands
class	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.
class	Solver_z3_4_3	This class is an adapter that takes the SMT-LIB ASTs and translates them into Z3 commands
class	Solver_z3_4_3_2	This is a special handler for Z3 4.3.2, as opposed to other revisions of Z3 4.3.
class	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)
class	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()/exit() (process lifecycle) are overridden.