sig
  val no_root_predicates : bool Pervasives.ref
  type transl_data = {
    f_paths : GDL.path_set;
    c_paths : GDL.path_set;
    all_paths : GDL.path_set;
    root_reps : GDL.term list;
    counters : string list;
    num_functions : (string * Formula.real_expr) list;
    defined_rels : string list;
    argpaths : (string * (GDL.path list array, GDL.argpaths) Aux.choice) list;
    term_arities : (string * int) list;
  }
  val blank_out : TranslateFormula.transl_data -> GDL.term -> GDL.term
  val var_of_term :
    TranslateFormula.transl_data -> GDL.term -> Formula.const_or_fo_var
  val empty_transl_data : TranslateFormula.transl_data
  val separate_disj :
    string list ->
    GDL.literal list list ->
    (GDL.literal list * GDL.literal list * GDL.literal list) list
  val translate :
    ?counter_guard:bool ->
    ?ctx_terms:GDL.term list ->
    TranslateFormula.transl_data -> GDL.literal list list -> Formula.formula
  val build_defrels :
    TranslateFormula.transl_data ->
    GDL.clause list -> (string * (string list * Formula.formula)) list
end