Uses of Interface
org.smtlib.ISolver

Packages that use ISolver

Package	Description
org.smtlib	This package contains the main classes and abstract interfaces for this SMT-LIB tool; the tool provides a stand-alone SMT-LIB-compliant command-line application, an application that responds to SMT-LIB commands over a network port, and an SMT-LIB Java API.
org.smtlib.command	This package contains implementations of the SMT-LIB commands, implementing the interfaces defined in ICommand; these implementations are independent of the concrete syntax that might be used, except that each command object has methods that can parse or print representations of the command in the standard (or potentially other) concrete syntaxes.
org.smtlib.ext	This package contains commands that are extensions to SMT-LIB.
org.smtlib.impl	This package is an implementation of the interfaces defined in org.smtlib.
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 ISolver in org.smtlib

Classes in org.smtlib that implement ISolver

Modifier and Type	Class	Description
class	AbstractSolver	This class implements the operations of the org.smtlib.ISolver interface that map directly onto a single translated command sent to the solver process, with the expected response of a fully SMT-LIB compliant solver (a flat success/error/sat/unsat/ unknown/unsupported, or a bare value/attribute-pair for get-option/get-info): the command is translated with AbstractSolver.translate(INode) and sent via AbstractSolver.sendCommand(ICommand).

Fields in org.smtlib declared as ISolver

Modifier and Type	Field	Description
protected ISolver	SMT.solver

Methods in org.smtlib that return ISolver

Modifier and Type	Method	Description
ISolver	SMT.Configuration.createSolver(String solvername, String executable)	Resolves the given solver name and executable to a concrete ISolver adapter instance, applying the same name/executable/adapter resolution jsmtlib.properties supports as SMT.startSolver(org.smtlib.SMT.Configuration, java.lang.String, java.lang.String) -- platform-specific .adapter/.exec overrides checked before their bare counterparts, the Solver_<name> naming convention, the z3-specific Solver_z3_recent fallback for an unrecognized z3 variant, the generic Solver_smt fallback, the "test" pseudo-solver special case, and %exec% command-array placeholder substitution -- but, unlike startSolver, this method does not start the solver and does not do any CLI-flavored error()/usage() reporting: any resolution or construction failure is reported as a thrown ISolver.CreationException instead, leaving it to the caller to start the returned solver (via start()) and decide how to report a creation failure.
ISolver	SMT.startSolver(SMT.Configuration smtConfig, String solvername, String executable)	Starts the solver with the given name and executable, preset according to the given configuration.

Methods in org.smtlib with parameters of type ISolver

Modifier and Type	Method	Description
IResponse	ICommand.execute(ISolver solver)	Executes the command on the given solver; presumes that the command type-checked successfully.
IResponse	ICommand.IScript.execute(ISolver solver)

Uses of ISolver in org.smtlib.command

Methods in org.smtlib.command with parameters of type ISolver

Modifier and Type	Method	Description
IResponse	C_assert.execute(ISolver solver)
IResponse	C_check_sat_assuming.execute(ISolver solver)
IResponse	C_check_sat.execute(ISolver solver)
IResponse	C_comment.execute(ISolver solver)
IResponse	C_declare_const.execute(ISolver solver)
IResponse	C_declare_datatype.execute(ISolver solver)
IResponse	C_declare_datatypes.execute(ISolver solver)
IResponse	C_declare_fun.execute(ISolver solver)
IResponse	C_declare_sort_parameter.execute(ISolver solver)
IResponse	C_declare_sort.execute(ISolver solver)
IResponse	C_define_const.execute(ISolver solver)
IResponse	C_define_fun_rec.execute(ISolver solver)
IResponse	C_define_fun.execute(ISolver solver)
IResponse	C_define_funs_rec.execute(ISolver solver)
IResponse	C_define_sort.execute(ISolver solver)
IResponse	C_echo.execute(ISolver solver)
IResponse	C_exit.execute(ISolver solver)
IResponse	C_get_assertions.execute(ISolver solver)
IResponse	C_get_assignment.execute(ISolver solver)
IResponse	C_get_info.execute(ISolver solver)
IResponse	C_get_model.execute(ISolver solver)
IResponse	C_get_option.execute(ISolver solver)
IResponse	C_get_proof.execute(ISolver solver)
IResponse	C_get_unsat_assumptions.execute(ISolver solver)
IResponse	C_get_unsat_core.execute(ISolver solver)
IResponse	C_get_value.execute(ISolver solver)
IResponse	C_pop.execute(ISolver solver)
IResponse	C_push.execute(ISolver solver)
IResponse	C_reset_assertions.execute(ISolver solver)
IResponse	C_reset.execute(ISolver solver)
IResponse	C_set_info.execute(ISolver solver)
IResponse	C_set_logic.execute(ISolver solver)
IResponse	C_set_option.execute(ISolver solver)

Uses of ISolver in org.smtlib.ext

Methods in org.smtlib.ext with parameters of type ISolver

Modifier and Type	Method	Description
IResponse	C_exec.execute(ISolver solver)	Executes the command, which executes the script
IResponse	C_what.execute(ISolver solver)

Uses of ISolver in org.smtlib.impl

Methods in org.smtlib.impl with parameters of type ISolver

Modifier and Type	Method	Description
IResponse	Script.execute(ISolver solver)	Executes the current list

Uses of ISolver in org.smtlib.solvers

Classes in org.smtlib.solvers that implement ISolver

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()/AbstractSolver.exit() (process lifecycle) are handled here, besides the get- command checks below.
class	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.
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()/AbstractSolver.exit() (process lifecycle) are overridden.