Package org.smtlib.solvers

Class Solver_smtinterpol

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_smtinterpol
All Implemented Interfaces:
ISolver
public class Solver_smtinterpol extends AbstractSolver implements ISolver
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 start()/AbstractSolver.exit() (process lifecycle) are handled here, besides the get- command checks below. Otherwise empirically SMT-LIB compliant: :print-success already defaults to true (no priming command needed), errors come back as clean (error "...") s-expressions, and bitvector values print via the equally-valid (_ bvN W) indexed-literal form (not #b/#x, but standard concrete syntax that the generic parser handles without any massaging).

The -q flag is required, not cosmetic: without it, SMTInterpol writes a large volume of "INFO - ..." solver-internal logging to its own stderr for every check-sat (statistics, per-clause traces, model dumps). That's a separate stream from the stdout responses SolverProcess parses, but SolverProcess's listen() has a heuristic (see its "some cases (yices2) the prompt is on the error stream" comment) that can prefer non-empty stderr content over stdout -- so unsilenced INFO noise risks being returned as the response instead of the real one. -q suppresses it at the source rather than relying on that heuristic guessing right.

  • Field Details

    • cmds

      protected String[] cmds
      The command-line arguments for launching the solver.

  • Constructor Details

    • Solver_smtinterpol

      public Solver_smtinterpol(SMT.Configuration smtConfig, String[] command)
      Creates an instance of the solver. The base launch command ("java -jar <jar> -q") comes from the org.smtlib.solver_smtinterpol-2.5.command property; only the timeout flag, which is conditional on smtConfig and so can't be expressed in that static property, is still added here.

  • Method Details