Package org.smtlib.solvers

Class Solver_yices2

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_smt
org.smtlib.solvers.Solver_yices2
All Implemented Interfaces:
ISolver
Direct Known Subclasses:
Solver_yices2_2_6
public class Solver_yices2 extends Solver_smt implements ISolver
This class is an adapter that takes the SMT-LIB ASTs and translates them into yices2 commands

  • Constructor Details

    • Solver_yices2

      public Solver_yices2(SMT.Configuration smtConfig, String[] command)
      Creates an instance of the yices2 solver

    • Solver_yices2

      public Solver_yices2(SMT.Configuration smtConfig, String command)
      Creates an instance of the yices2 solver

  • Method Details

    • selfReportsImmediateExit

      protected boolean selfReportsImmediateExit()
      yices2 self-reports (get-info :error-behavior) as immediate-exit and its process does exit after some (not all) errors -- see AbstractSolver#sendCommand(ICommand, boolean), which uses this to pause briefly after any error response, giving a genuinely-exiting process time to finish dying before the next command's liveness check runs.
      Overrides:
      selfReportsImmediateExit in class AbstractSolver

    • lineNumberPatterns

      protected List<Pattern> lineNumberPatterns()
      Description copied from class: AbstractSolver
      Patterns matching the line numbers in this solver's messages about the command answered: group 1 is the text before the number, group 2 the number, group 3 the text after it
      Overrides:
      lineNumberPatterns in class AbstractSolver

    • cmd

      public String[] cmd(String exec)
      Overrides:
      cmd in class Solver_smt

    • echo

      public IResponse echo(IExpr.IStringLiteral arg)
      yices2 writes echo's text unquoted, so where it ends cannot be found (#136); the response to echo is its argument
      Specified by:
      echo in interface ISolver
      Overrides:
      echo in class AbstractSolver
      Returns:
      the argument as an IResponse

    • start

      public IResponse start()
      Description copied from interface: ISolver
      Starts the solver; this is not an SMT-LIB command, but it is convenient in some implementations to separate the starting and initialization from the construction of the solver instance.
      Specified by:
      start in interface ISolver
      Overrides:
      start in class Solver_smt
      Returns:
      success or an SMT error response
      See Also:

    • get_info

      public IResponse get_info(IExpr.IKeyword key)
      yices2 answers get-info :status with the last set-info :status value, but with (error "no info for :status") when none was set; SMT-LIB requires unsupported for a flag the solver does not support. Other flags are answered by yices2 itself.
      Specified by:
      get_info in interface ISolver
      Overrides:
      get_info in class AbstractSolver
      Parameters:
      key - the info keyword
      Returns:
      the info value, or unsupported, or an SMT error response
      See Also:

    • get_model

      public IResponse get_model()
      yices2 answers get-model with :produce-models off, and in assert mode after a check
      Specified by:
      get_model in interface ISolver
      Overrides:
      get_model in class AbstractSolver
      Returns:
      a model, unsupported, or an SMT error response
      See Also:

    • get_value

      public IResponse get_value(IExpr... terms)
      yices2 answers get-value with :produce-models off, and in assert mode after a check
      Specified by:
      get_value in interface ISolver
      Overrides:
      get_value in class AbstractSolver
      Parameters:
      terms - expressions to evaluate
      Returns:
      a list of term–value pairs, unsupported, or an SMT error response
      See Also:

    • get_assignment

      public IResponse get_assignment()
      yices2 answers get-assignment with :produce-assignments off, and in assert mode after a check
      Specified by:
      get_assignment in interface ISolver
      Overrides:
      get_assignment in class AbstractSolver
      Returns:
      a list of name–Boolean pairs, unsupported, or an SMT error response
      See Also:

    • get_unsat_core

      public IResponse get_unsat_core()
      yices2 answers get-unsat-core in assert mode after a check
      Specified by:
      get_unsat_core in interface ISolver
      Overrides:
      get_unsat_core in class AbstractSolver
      Returns:
      a list of formula names, unsupported, or an SMT error response
      See Also:

    • get_unsat_assumptions

      public IResponse get_unsat_assumptions()
      yices2 answers get-unsat-assumptions, wrongly, in assert mode after a check
      Specified by:
      get_unsat_assumptions in interface ISolver
      Overrides:
      get_unsat_assumptions in class AbstractSolver
      Returns:
      a list of assumption literals, unsupported, or an SMT error response
      See Also: