sig
  val get_atoms : Formula.formula -> Formula.formula list
  val get_relations_constants :
    Formula.formula -> (string * int) list * string list
  val map_to_literals :
    ?save_rels:string list ->
    ?save_rvars:string list ->
    (Formula.formula -> Formula.formula) ->
    (Formula.real_expr -> Formula.real_expr) ->
    (Formula.formula -> Formula.formula) ->
    Formula.formula -> Formula.formula
  val map_to_literals_expr :
    ?save_rels:string list ->
    ?save_rvars:string list ->
    (Formula.formula -> Formula.formula) ->
    (Formula.real_expr -> Formula.real_expr) ->
    (Formula.formula -> Formula.formula) ->
    Formula.real_expr -> Formula.real_expr
  val map_to_atoms_full :
    (Formula.formula -> Formula.formula) ->
    (Formula.real_expr -> Formula.real_expr) ->
    (Formula.formula -> Formula.formula) ->
    Formula.formula -> Formula.formula
  val map_to_atoms_full_re :
    (Formula.formula -> Formula.formula) ->
    (Formula.real_expr -> Formula.real_expr) ->
    (Formula.formula -> Formula.formula) ->
    Formula.real_expr -> Formula.real_expr
  val map_to_atoms :
    (Formula.formula -> Formula.formula) ->
    Formula.formula -> Formula.formula
  val map_to_atoms_expr :
    (Formula.formula -> Formula.formula) ->
    Formula.real_expr -> Formula.real_expr
  type formula_and_expr_map = {
    map_Rel : string -> Formula.const_or_fo_var array -> Formula.formula;
    map_Eq :
      Formula.const_or_fo_var -> Formula.const_or_fo_var -> Formula.formula;
    map_SO :
      Formula.so_var -> Formula.const_or_fo_var array -> Formula.formula;
    map_RealExpr : Formula.real_expr -> Formula.sign_op -> Formula.formula;
    map_Not : Formula.formula -> Formula.formula;
    map_And : Formula.formula list -> Formula.formula;
    map_Or : Formula.formula list -> Formula.formula;
    map_Ex : Formula.var list -> Formula.formula -> Formula.formula;
    map_All : Formula.var list -> Formula.formula -> Formula.formula;
    map_Lfp :
      Formula.so_var ->
      Formula.fo_var array -> Formula.formula -> Formula.formula;
    map_Gfp :
      Formula.so_var ->
      Formula.fo_var array -> Formula.formula -> Formula.formula;
    map_Let :
      string ->
      string list -> Formula.formula -> Formula.formula -> Formula.formula;
    map_RVar : string -> Formula.real_expr;
    map_Const : float -> Formula.real_expr;
    map_Plus : Formula.real_expr -> Formula.real_expr -> Formula.real_expr;
    map_Times : Formula.real_expr -> Formula.real_expr -> Formula.real_expr;
    map_Pow : Formula.real_expr -> Formula.real_expr -> Formula.real_expr;
    map_Fun : string -> Formula.const_or_fo_var -> Formula.real_expr;
    map_Char : Formula.formula -> Formula.real_expr;
    map_Sum :
      Formula.fo_var list ->
      Formula.formula -> Formula.real_expr -> Formula.real_expr;
    map_RLet :
      string -> Formula.real_expr -> Formula.real_expr -> Formula.real_expr;
  }
  val identity_map : FormulaMap.formula_and_expr_map
  val map_formula :
    FormulaMap.formula_and_expr_map -> Formula.formula -> Formula.formula
  val map_real_expr :
    FormulaMap.formula_and_expr_map -> Formula.real_expr -> Formula.real_expr
  type 'a formula_and_expr_fold = {
    fold_Rel : string -> Formula.const_or_fo_var array -> 'a;
    fold_Eq : Formula.const_or_fo_var -> Formula.const_or_fo_var -> 'a;
    fold_SO : Formula.so_var -> Formula.const_or_fo_var array -> 'a;
    fold_RealExpr : 'a -> Formula.sign_op -> 'a;
    fold_Not : 'a -> 'a;
    fold_And : 'a -> 'a -> 'a;
    fold_Or : 'a -> 'a -> 'a;
    fold_Ex : Formula.var list -> 'a -> 'a;
    fold_All : Formula.var list -> 'a -> 'a;
    fold_Lfp : Formula.so_var -> Formula.fo_var array -> 'a -> 'a;
    fold_Gfp : Formula.so_var -> Formula.fo_var array -> 'a -> 'a;
    fold_Let : string -> string list -> 'a -> 'a -> 'a;
    fold_RVar : string -> 'a;
    fold_Const : float -> 'a;
    fold_Plus : 'a -> 'a -> 'a;
    fold_Times : 'a -> 'a -> 'a;
    fold_Pow : 'a -> 'a -> 'a;
    fold_Fun : string -> Formula.const_or_fo_var -> 'a;
    fold_Char : 'a -> 'a;
    fold_Sum : Formula.fo_var list -> 'a -> 'a -> 'a;
    fold_RLet : string -> 'a -> 'a -> 'a;
  }
  val make_fold :
    ('a -> 'a -> 'a) -> 'a -> 'a FormulaMap.formula_and_expr_fold
  val fold_formula :
    'a FormulaMap.formula_and_expr_fold -> Formula.formula -> 'a
  val fold_real_expr :
    'a FormulaMap.formula_and_expr_fold -> Formula.real_expr -> 'a
  val map_to_formulas_expr :
    (Formula.formula -> Formula.formula) ->
    Formula.real_expr -> Formula.real_expr
  val fold_over_formulas_expr :
    (Formula.formula -> 'a -> 'a) -> Formula.real_expr -> 'a -> 'a
  val fold_over_literals :
    (Formula.formula -> 'a -> 'a) -> Formula.formula -> 'a -> 'a
  val fold_over_atoms :
    (Formula.formula -> 'a -> 'a) -> Formula.formula -> 'a -> 'a
  val map_to_all_vars :
    (Formula.var -> Formula.var) -> Formula.formula -> Formula.formula
end