sig
  type logic = FO | ExFO | GuardedFO | ExGuardedFO
  val predicates_partition : bool Pervasives.ref
  val atoms : Structure.structure -> int array -> Formula.formula list
  val ntype :
    ?existential:bool ->
    Structure.structure -> int -> int array -> Formula.formula
  val ntypes :
    ?existential:bool ->
    Structure.structure -> qr:int -> k:int -> Formula.formula list
  val guards :
    Structure.structure ->
    int array ->
    (int list * Formula.var list * int array * int array * Formula.formula)
    list
  val guard_tuple_str :
    int list * Formula.var list * int array * int array * Formula.formula ->
    string
  val guarded_type :
    ?existential:bool ->
    Structure.structure -> int -> int array -> Formula.formula
  val guarded_types :
    ?existential:bool ->
    Structure.structure -> qr:int -> k:int -> Formula.formula list
  val tc_max :
    Structure.structure -> Formula.formula -> ?from:int -> int -> int option
  val tc_atomic :
    ?positive:bool ->
    ?repeat_vars:bool ->
    Structure.structure -> ?from:int -> int -> (int * Formula.formula) list
  val tc_atomic_distinguish :
    ?positive:bool ->
    ?repeat_vars:bool ->
    Structure.structure list ->
    Structure.structure list -> int -> Formula.formula option
  val distinguish_result_tc :
    (int * Formula.formula) list option Pervasives.ref
  val compare_types :
    (Formula.formula -> Formula.formula -> int) Pervasives.ref
  val min_type_omitting :
    ?logic:Distinguish.logic ->
    qr:int ->
    k:int ->
    Formula.formula list -> Structure.structure -> Formula.formula option
  val distinguish_upto :
    ?logic:Distinguish.logic ->
    qr:int ->
    k:int ->
    Structure.structure list ->
    Structure.structure list -> Formula.formula option
  val distinguish_guess :
    ?positive:bool ->
    d1:int ->
    d2:int ->
    k:int ->
    Structure.structure list ->
    Structure.structure list -> Formula.formula option
  val distinguish :
    ?use_tc:bool ->
    ?skip_outer_exists:bool ->
    ?ex:bool ->
    ?guess:bool ->
    Structure.structure list -> Structure.structure list -> Formula.formula
end