Parameter Converter.1-D

Solver configuration options

val cmd_line : TermLib.logic -> int -> bool -> 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 : bool -> 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 : Stdlib.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 : Stdlib.Format.formatter -> TermLib.logic -> unit

Pretty-print a logic in SMTLIB format

val pp_print_symbol : ?⁠arity:int -> Stdlib.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 : Stdlib.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