sig
  val nnf :
    ?neg:bool -> ?rev:string list -> Formula.formula -> Formula.formula
  val make_fp_inductive : int -> Formula.formula -> Formula.formula
  val del_vars_quant : Formula.var list -> Formula.formula -> Formula.formula
  val rename_quant_avoiding :
    Formula.var list -> Formula.formula -> Formula.formula
  val rels_signs : Formula.formula -> Aux.Strings.t * Aux.Strings.t
  val rels_signs_expr : Formula.real_expr -> Aux.Strings.t * Aux.Strings.t
  val atoms :
    ?repetitions:bool ->
    (string * int) list -> string list -> Formula.formula list
  val atp : (string * int) list -> string list -> Formula.formula list
  val mintp :
    (Formula.formula -> bool) ->
    (string * int) list -> string list -> Formula.formula list
  val simplify :
    ?do_pnf:bool ->
    ?do_re:bool -> ?ni:int -> Formula.formula -> Formula.formula
  val simplify_re :
    ?do_pnf:bool ->
    ?do_formula:bool -> ?ni:int -> Formula.real_expr -> Formula.real_expr
  val pnf : Formula.formula -> Formula.formula
  val as_conjuncts : Formula.formula -> Formula.formula list
  val remove_subformulas :
    (Formula.formula -> bool) -> Formula.formula -> Formula.formula
  val prune_unused_quants : Formula.formula -> Formula.formula
  val remove_redundant :
    ?implies:(Formula.formula -> Formula.formula -> bool) ->
    Formula.formula -> Formula.formula
  val tnf : Formula.formula -> Formula.formula
  val tnf_re : Formula.real_expr -> Formula.real_expr
  val tnf_fv :
    ?sizes:(string * int) list -> Formula.formula -> Formula.formula
  val to_dnf : Formula.formula -> Formula.formula list
  val to_cnf : Formula.formula -> Formula.formula list
  val dimension_vars : int -> string list -> string list
  val dimension : int -> size:int -> Formula.formula -> Formula.formula
  val piecewise_linear :
    Formula.real_expr -> (float * float) list -> Formula.real_expr
  val rk4_step_symb :
    string ->
    Formula.real_expr ->
    Formula.real_expr ->
    Formula.eq_sys -> Formula.real_expr list -> Formula.real_expr list
end