Package org.smtlib.solvers

Class Solver_smt

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_smt
All Implemented Interfaces:
ISolver
Direct Known Subclasses:
Solver_yices2
public class Solver_smt extends AbstractSolver implements ISolver
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. It is otherwise a concrete, silent inheritor of AbstractSolver: only translate(INode) is overridden (a real, solver- specific deviation — a Bool-quantifier workaround, see Printer), plus start()/AbstractSolver.exit() (process lifecycle, which AbstractSolver deliberately leaves unimplemented). :verbosity is just forwarded to the solver like any other option (via AbstractSolver's default set_option_impl) -- an earlier version of this class instead used a script's :verbosity value to toggle jSMTLIB's own internal --verbose debug tracing (smtConfig.verbose), which leaked "#Command to execute: ..." trace lines into the solver's own response stream. Every other ISolver command — including get_assertions/get_value/ get_assignment/get_unsat_core/get_unsat_assumptions, whose precondition checks and structured-response parsing now live in AbstractSolver — is inherited unchanged.

Subclasses of a genuinely non-compliant solver should override AbstractSolver.parseResponse(String) for their own quirks rather than assuming this class's behavior; see AbstractSolver.parseResponse(String) for an example (legacy bitvector literal syntax, multi-fragment error text) that used to live here as a blanket default for every Solver_smt subclass, which was more defensive than this fully-compliant-by-default adapter should assume.