sig
  val var_subst : (string * string) list -> [< Formula.var ] -> Formula.var
  val subst_name_avoiding_str : string list -> string -> string * string
  val subst_name_prefix : string Pervasives.ref
  val subst_name_avoiding :
    [< Formula.var ] list -> [< Formula.var ] -> string * string
  val subst_vars :
    (string * string) list -> Formula.formula -> Formula.formula
  val subst_vars_expr :
    (string * string) list -> Formula.real_expr -> Formula.real_expr
  val subst_real :
    (string * Formula.real_expr) list ->
    Formula.real_expr -> Formula.real_expr
  val subst_once_rels :
    (string * (string list * Formula.formula)) list ->
    Formula.formula -> Formula.formula
  val subst_once_rels_expr :
    (string * (string list * Formula.formula)) list ->
    Formula.real_expr -> Formula.real_expr
  val subst_rels :
    (string * (string list * Formula.formula)) list ->
    Formula.formula -> Formula.formula
  val subst_rels_expr :
    (string * (string list * Formula.formula)) list ->
    Formula.real_expr -> Formula.real_expr
  val expand_formula :
    ?defs:(string * (string list * Formula.formula)) list ->
    Formula.formula -> Formula.formula
  val expand_real_expr :
    ?defs:(string * (string list * Formula.formula)) list ->
    Formula.real_expr -> Formula.real_expr
  val range :
    ?estimates:(string * (float * float)) list ->
    ?pred_est:((string * int) * float) list ->
    int -> Formula.real_expr -> float * float
  val assign_emptyset : string -> Formula.formula -> Formula.formula
  val all_vars : Formula.formula -> Formula.var list
  val free_vars : Formula.formula -> Formula.var list
  val quantified_vars : Formula.formula -> Formula.var list
  val push_quant : Formula.formula -> Formula.formula
  val make_lfp_tc : string -> string -> Formula.formula -> Formula.formula
  val make_mso_tc : string -> string -> Formula.formula -> Formula.formula
  val make_fo_tc_conj :
    ?reflexive:bool ->
    int -> string -> string -> Formula.formula -> Formula.formula
  val make_fo_tc_disj :
    ?reflexive:bool ->
    int -> string -> string -> Formula.formula -> Formula.formula
  val fo_tc_param : int Pervasives.ref
  val make_standard_tc :
    string -> string -> Formula.formula -> Formula.formula
end