Module SolverResponse

module SolverResponse: sig .. end

Solver commands and responses



type error_response = [ `Error of string ] 
Type of reponses for errors
type no_response = [ `NoResponse ] 
type decl_response = [ `Error of string | `NoResponse | `Success | `Unsupported ] 
Type of reponses for declaration and definition commands
type check_sat_response = [ `Error of string | `Sat | `Unknown | `Unsat ] 
Type of reponses for check-sat commands
type get_value_response = [ `Error of string | `Values of (Term.t * Term.t) list ] 
Type of reponses for get-value commands. It carries the model.
type get_model_response = [ `Error of string | `Model of (UfSymbol.t * Model.value) list ] 
Type of reponses for get-model commands. It carries the model.
type get_unsat_core_response = [ `Error of string | `Unsat_core of string list ] 
Type of reponses for get-unsat-core commands. It carries the unsat core.
type custom_response = [ `Custom of HStringSExpr.t list | `Error of string ] 
Type of reponses for custom commands
type response = [ `Custom of HStringSExpr.t list
| `Error of string
| `Model of (UfSymbol.t * Model.value) list
| `NoResponse
| `Sat
| `Success
| `Unknown
| `Unsat
| `Unsat_core of string list
| `Unsupported
| `Values of (Term.t * Term.t) list ]
Type of all possible responses of a solver
val pp_print_response : Format.formatter -> response -> unit
Pretty-print a response to a command