Module Binsec.Formula_utils

Utility functions for formula creation

type stats = {
  1. var : int;
  2. cst : int;
  3. unop : int;
  4. bnop : int;
  5. comp : int;
  6. select : int;
  7. store : int;
}
val bl_term_stats : Formula.bl_term -> stats
val bv_term_stats : Formula.bv_term -> stats
val ax_term_stats : Formula.ax_term -> stats
val bl_term_variables : Formula.bl_term -> Formula.VarSet.t
val bv_term_variables : Formula.bv_term -> Formula.VarSet.t
val ax_term_variables : Formula.ax_term -> Formula.VarSet.t
val is_symbolic_bl_term : Formula.bl_term -> bool
  • returns

    true if the expression is syntactically symbolic meaning there is at least one variable

val is_symbolic_bv_term : Formula.bv_term -> bool
val is_symbolic_ax_term : Formula.ax_term -> bool
val bv_size : Formula.bv_term -> int
val ax_size : Formula.ax_term -> int * int
val bv_desc_size : Formula.bv_term_desc -> int
val ax_desc_size : Formula.ax_term_desc -> int * int
val is_bl_desc_cst : Formula.bl_term_desc -> bool option
val is_bv_desc_cst : Formula.bv_term_desc -> Bitvector.t option
val is_bl_cst : Formula.bl_term -> bool option
val is_bv_cst : Formula.bv_term -> Bitvector.t option
val is_bl_desc_var : Formula.bl_term_desc -> Formula.bl_var option
val is_bv_desc_var : Formula.bv_term_desc -> Formula.bv_var option
val is_ax_desc_var : Formula.ax_term_desc -> Formula.ax_var option
val is_bl_var : Formula.bl_term -> Formula.bl_var option
val is_bv_var : Formula.bv_term -> Formula.bv_var option
val is_ax_var : Formula.ax_term -> Formula.ax_var option
val is_select : Formula.bv_term -> (int * Formula.ax_term * Formula.bv_term) option
val is_store : Formula.ax_term -> (int * Formula.ax_term * Formula.bv_term * Formula.bv_term) option
val var_hash : Formula.var -> int
val bl_var_hash : Formula.bl_var -> int
val bv_var_hash : Formula.bv_var -> int
val ax_var_hash : Formula.ax_var -> int
val var_name : Formula.var -> string
val bl_var_name : Formula.bl_var -> string
val bv_var_name : Formula.bv_var -> string
val ax_var_name : Formula.ax_var -> string
val bl_term_desc_name : Formula.bl_term_desc -> string option
val bv_term_desc_name : Formula.bv_term_desc -> string option
val ax_term_desc_name : Formula.ax_term_desc -> string option
val bl_term_name : Formula.bl_term -> string option
val bv_term_name : Formula.bv_term -> string option
val ax_term_name : Formula.ax_term -> string option
val decl_desc_name : Formula.decl_desc -> string
val def_desc_name : Formula.def_desc -> string
val decl_name : Formula.decl -> string
val def_name : Formula.def -> string
module BindEnv : sig ... end