Module type SolverDriver.S

module type S = sig .. end


Solver configuration options


val cmd_line : TermLib.logic -> bool -> bool -> bool -> bool -> string array
Command line options
val check_sat_limited_cmd : int -> string
Internal command for check-sat with timeout in milliseconds
val check_sat_assuming_supported : unit -> bool
Returns true if check-sat-assuming functionality is supported
val check_sat_assuming_cmd : unit -> string
Special command for check-sat-assuming
val headers : unit -> string list
Solver specific headers to add at the beginning of the file
val prelude : string list
Solver specific commands to add at the beginning of the file
val trace_extension : string
File extension for traces
val comment_delims : string * string
Begin / end delimiters for comments

Sort conversions


val interpr_type : Type.t -> Type.t
Can interpret type in a supported sort. Fails on unsupported sorts.
val pp_print_sort : Format.formatter -> Type.t -> unit
Print a sort
val string_of_sort : Type.t -> string
Return an SMTLIB string expression of a sort
val string_of_logic : TermLib.logic -> string
Return an SMTLIB string expression for the logic
val pp_print_logic : Format.formatter -> TermLib.logic -> unit
Pretty-print a logic in SMTLIB format
val pp_print_symbol : ?arity:int -> Format.formatter -> Symbol.t -> unit
Pretty-print a symbol
val string_of_symbol : ?arity:int -> Symbol.t -> string
Return a string representation of a symbol
val pp_print_expr : Format.formatter -> Term.t -> unit
Pretty-print an expression
val print_expr : Term.t -> unit
Pretty-print an expression to the default formatter
val string_of_expr : Term.t -> string
Return a string representation of an expression