Module SolverResponse

Solver commands and responses

type error_response = [
  1. | `Error of string
  2. | `Timeout
]

Type of reponses for errors

type no_response = [
  1. | `NoResponse
]
type decl_response = [
  1. | no_response
  2. | `Unsupported
  3. | `Success
  4. | error_response
]

Type of reponses for declaration and definition commands

type check_sat_response = [
  1. | `Sat
  2. | `Unsat
  3. | `Unknown
  4. | error_response
]

Type of reponses for check-sat commands

type get_value_response = [
  1. | `Values of (Term.t * Term.t) list
  2. | error_response
]

Type of reponses for get-value commands. It carries the model.

type get_model_response = [
  1. | `Model of (UfSymbol.t * Model.value) list
  2. | error_response
]

Type of reponses for get-model commands. It carries the model.

type get_unsat_core_response = [
  1. | `Unsat_core of string list
  2. | error_response
]

Type of reponses for get-unsat-core commands. It carries the unsat core.

type custom_response = [
  1. | `Custom of HStringSExpr.t list
  2. | error_response
]

Type of reponses for custom commands

Type of all possible responses of a solver

val pp_print_response : Stdlib.Format.formatter -> response -> unit

Pretty-print a response to a command