Formula_transformation (p.binsec.0.5.0.doc.binsec.Binsec.Formula

val rename_bl_var : (string -> string) -> Formula.bl_var -> Formula.bl_var

val rename_bv_var : (string -> string) -> Formula.bv_var -> Formula.bv_var

val rename_ax_var : (string -> string) -> Formula.ax_var -> Formula.ax_var

val rename_bl_term : (string -> string) -> Formula.bl_term -> Formula.bl_term

val rename_bv_term : (string -> string) -> Formula.bv_term -> Formula.bv_term

val rename_ax_term : (string -> string) -> Formula.ax_term -> Formula.ax_term

val replace_bl_term : Formula.def -> Formula.bl_term -> Formula.bl_term

val replace_bv_term : Formula.def -> Formula.bv_term -> Formula.bv_term

val replace_ax_term : Formula.def -> Formula.ax_term -> Formula.ax_term

val constant_propagation : 
  ?keep:Formula.VarSet.t ->
  Formula.formula ->
  Formula.formula

val prune_and_inline : 
  ?keep:Formula.VarSet.t ->
  Formula.formula ->
  Formula.formula

val read_over_write : 
  ?lst:int ->
  ?rbs:bool ->
  ?itv:bool ->
  Formula.formula ->
  Formula.formula

val static_single_assignment : Formula.formula -> Formula.formula

val taint : (Formula.var -> bool) -> Formula.formula -> Formula.formula

val optimize : 
  ?keep:Formula.VarSet.t ->
  ?lst:int ->
  ?cst:bool ->
  ?itv:bool ->
  ?prn:bool ->
  ?rbs:bool ->
  ?row:bool ->
  ?ssa:bool ->
  ?is_controlled:(Formula.VarSet.elt -> bool) ->
  Formula.formula ->
  Formula.formula

val optimize_from_options : 
  ?keep:Formula.VarSet.t ->
  ?is_controlled:(Formula.VarSet.elt -> bool) ->
  Formula.formula ->
  Formula.formula