Module type `SMTLIBSolver.SMTLIBSolverDriver`

include SolverDriver.S

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

val s_define_fun : HString.t
val expr_of_string_sexpr : HStringSExpr.t -> Term.t
val expr_or_lambda_of_string_sexpr : HStringSExpr.t -> HString.t * Model.value