Functor SMTExpr.Converter

module Converter: 
functor (D : SolverDriver.S-> Conv
Parameters:
D : SolverDriver.S


Conversions between SMT expressions and terms


val smtsort_of_type : Type.t -> SMTExpr.sort
Convert a variable to an SMT expression
val smtexpr_of_var : Var.t -> Term.t list -> SMTExpr.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 : Format.formatter -> TermLib.logic -> unit
Pretty-print a logic in SMTLIB format
val pp_print_sort : Format.formatter -> SMTExpr.sort -> unit
Pretty-print a sort in SMTLIB format
val string_of_sort : SMTExpr.sort -> string
Return an SMTLIB string expression of a sort
val pp_print_expr : Format.formatter -> SMTExpr.t -> unit
Pretty-print a term in SMTLIB format
val print_expr : SMTExpr.t -> unit
Pretty-print a term in SMTLIB format to the standard formatter
val string_of_expr : SMTExpr.t -> string
Return an SMTLIB string expression of a term
val smtexpr_of_term : SMTExpr.t -> SMTExpr.t
Convert a term to an SMT expression
val quantified_smtexpr_of_term : bool -> Var.t list -> SMTExpr.t -> SMTExpr.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 : SMTExpr.t -> SMTExpr.t
Convert an SMT expression to a variable
val term_of_smtexpr : SMTExpr.t -> SMTExpr.t
Convert an SMT expression to a term
val pp_print_custom_arg : Format.formatter -> SMTExpr.custom_arg -> unit
Pretty-print a custom argument
val string_of_custom_arg : SMTExpr.custom_arg -> string
Return an string representation of a custom argument