Module Smtlib2print

module Smtlib2print: sig .. end
Smtlib2 printer


This module aim at generating well formatted smtlib2 formulas, taking in account some solvers differences (e.g: boolector not supporting function have arrays in parameters). All the strings generated by this module are smtlib 2 compliant.
val pp_smt_result : Format.formatter -> Smtlib2.smt_result -> unit
pretty print the smt_result with a given color
val smtres_to_string : Smtlib2.smt_result -> string
Returns the string associated with a smt_result
val smtbvunary_to_string : Smtlib2.smt_bv_unary -> string
Returns the string of an unary bitvector expression
val smtbvbinary_to_string : Smtlib2.smt_bv_binary -> string
Returns the string of a binary bitvector expression
val smtbvexpr_to_string : ?inline:bool -> Smtlib2.smt_bv_expr -> string
Returns the string of a bitvector expression. ~inline defines if SmtABvLoad32, SmtABvStore32 functions should be inlined or not. (used for solvers not supporting this functions)
val smtabvexpr_to_string : ?inline:bool -> Smtlib2.smt_abv_expr -> string
see smtbvexpr_to_string
val smtexpr_to_string : ?inline:bool -> Smtlib2.smt_expr -> string
see smtbvexpr_to_string
val smtvarset_to_string : Smtlib2.SmtVarSet.t -> string
Returns the string formatting every input variable on a new line
val smt_header : unit -> string
Returns the preformatted header
val smt_functions : unit -> string
Returns or not the functions used in the formula. It uses internally the solver selected and the option -nat-cond to include or not array related functions