CVC5_native.Init
include sig ... end
type formula = |
type model = |
val name : string
val is_available : unit -> bool
val supports_smtlib_options : bool
val supports_get_info : bool
val supports_sets : bool
val supports_quantifiers : bool
val init : ?timeout:int -> 'a -> 'b
val translate : 'a -> 'b
val solve : 'a -> 'b
val simplify : 'a -> 'b
val show_formula : 'a -> 'b
val show_model : 'a -> 'b
val to_smtlib : 'a -> 'b
val push : 'a -> 'b
val pop : 'a -> 'b
val check_sat : 'a -> 'b