Module CVC4Driver (.ml)

module CVC4Driver: sig .. end

include GenericSMTLIBDriver
val cmd_line : [> `Inferred of TermLib.FeatureSet.t ] ->
'a -> 'b -> 'c -> 'd -> string array
val check_sat_limited_cmd : 'a -> 'b
val check_sat_assuming_cmd : unit -> 'a
val check_sat_assuming_supported : unit -> bool
val s_lambda : HString.t
val cvc4_expr_or_lambda_of_string_sexpr' : expr_of_string_sexpr_conv ->
(HString.t * Var.t) list -> HStringSExpr.t -> Model.value
val lambda_of_string_sexpr : HStringSExpr.t -> HStringSExpr.atom * Model.value
val string_of_logic : TermLib.logic -> string
val pp_print_logic : Format.formatter -> TermLib.logic -> unit