Module Binsec.Formula_pp

Formula 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_status : Format.formatter -> Formula.status -> unit

pretty print the smt_result with a given color

val print_status : Formula.status -> string
  • returns

    the string associated with a smt_result

val print_bv_unop : Formula.bv_unop -> string
  • returns

    the string of an unary bitvector expression

val print_bv_bnop : Formula.bv_bnop -> string
  • returns

    the string of a binary bitvector expression

val print_bv_comp : Formula.bv_comp -> string
  • returns

    the string of a binary bitvector expression

val print_bv_term : Formula.bv_term -> string
  • returns

    the string of a bitvector expression.

val print_ax_term : Formula.ax_term -> string

see print_bv_term

val print_bl_term : Formula.bl_term -> string

see print_bv_term

val print_varset : Formula.VarSet.t -> string
  • returns

    the string formatting every input variable on a new line

val pp_varset : Format.formatter -> Formula.VarSet.t -> unit
val print_header : unit -> string
  • returns

    the preformatted header

val pp_header : Format.formatter -> unit -> unit
val pp_as_comment : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
val pp_bl_term : Format.formatter -> Formula.bl_term -> unit
val pp_bv_term : Format.formatter -> Formula.bv_term -> unit
val pp_ax_term : Format.formatter -> Formula.ax_term -> unit
val pp_term : Format.formatter -> Formula.term -> unit
val pp_entry : Format.formatter -> Formula.entry -> unit
val pp_formula : Format.formatter -> Formula.formula -> unit