Module Smtlib_backend_builder.Make

Parameters

Signature

include Backend_sig.DESCRIPTION
val name : string
val supports_smtlib_options : bool
val supports_get_info : bool
val supports_sets : bool
val supports_quantifiers : bool
type formula

Internal representation of a formula.

type model

Internal representation of a model.

val is_available : unit -> bool

Check whether given solver is correctly installed.

val init : ?timeout:int -> unit -> unit
  • raises Not_available

    if the solver is not available.

val translate : SMT.t -> formula

Translate formula to solver's internal representation.

val solve : (_, _) Translation_context.t -> SMT.t -> bool -> string list -> (formula, model) Backend_sig.status

Translate formula to solver's internal representation and check its satisfiability.

TODO: producing models can be included in options?

val simplify : formula -> formula
val show_formula : formula -> string
val to_smtlib : SMT.t -> bool -> string list -> string
val show_model : model -> string

Incremental solving

val push : SMT.t -> unit
val pop : int -> unit
val check_sat : SMT.t -> (formula, model) Backend_sig.status