Module Astral_internal.Yices_backend

module Self : sig ... end
include sig ... end
val name : string
val supports_smtlib_options : bool
val supports_get_info : bool
val supports_sets : bool
val supports_quantifiers : bool
type formula
type model
val is_available : unit -> bool
val init : ?timeout:int -> unit -> unit
val translate : SMT.t -> formula
val solve : ('a, 'b) Translation_context.t -> SMT.t -> bool -> string list -> (formula, model) Astral_internal__Backend_sig.status
val simplify : formula -> formula
val show_formula : formula -> string
val to_smtlib : SMT.t -> bool -> string list -> string
val show_model : model -> string
val push : SMT.t -> unit
val pop : int -> unit
val check_sat : SMT.t -> (formula, model) Astral_internal__Backend_sig.status