Module type SMTExpr.Conv

Conversions between SMT expressions and terms

val smtsort_of_type : Type.t -> sort

Convert a variable to an SMT expression

val smtexpr_of_var : Var.t -> Term.t list -> t

Convert a variable to an SMT expression

Pretty-printing and String Conversions

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_sort : Stdlib.Format.formatter -> sort -> unit

Pretty-print a sort in SMTLIB format

val string_of_sort : sort -> string

Return an SMTLIB string expression of a sort

val pp_print_expr : Stdlib.Format.formatter -> t -> unit

Pretty-print a term in SMTLIB format

val print_expr : t -> unit

Pretty-print a term in SMTLIB format to the standard formatter

val string_of_expr : t -> string

Return an SMTLIB string expression of a term

val smtexpr_of_term : t -> t

Convert a term to an SMT expression

val quantified_smtexpr_of_term : bool -> Var.t list -> t -> t

Convert a term to an SMT expression, quantifying over the given variables quantified_smtexpr_of_term q v t returns the SMT expression exists (v) t or forall (v) t if q is true or false, respectively, where all variables in t except those in v are converted to uninterpreted functions.

val var_term_of_smtexpr : t -> t

Convert an SMT expression to a variable

val term_of_smtexpr : t -> t

Convert an SMT expression to a term

val pp_print_custom_arg : Stdlib.Format.formatter -> custom_arg -> unit

Pretty-print a custom argument

val string_of_custom_arg : custom_arg -> string

Return an string representation of a custom argument