package binsec

  1. Overview
  2. Docs
package binsec
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct