sig
  type reduction = {
    rels : (string * string list * Formula.formula) list;
    consts : (string * (int, string) Aux.choice) list;
  }
  val str : Reduction.reduction -> string
  val parse_reduct : string -> Reduction.reduction
  val find_example :
    ?timelog:bool -> int -> Formula.formula -> Structure.structure * bool
  val check_reduct :
    ?maximize:bool ->
    ?log:bool ->
    ?xy:bool ->
    ?consts:bool ->
    Formula.formula ->
    Formula.formula ->
    Reduction.reduction ->
    size:int -> int -> Structure.structure option * bool
  val find_reduct :
    ?log:bool ->
    int ->
    Formula.formula ->
    Formula.formula ->
    size:int ->
    dim:int -> ?fp:bool -> int * int -> Reduction.reduction option
  val find_reduct_iter :
    ?log:bool ->
    int ->
    Formula.formula ->
    Formula.formula ->
    smin:int ->
    smax:int ->
    dim:int ->
    ?fp:bool -> ?stepwise:bool -> int * int -> Reduction.reduction option
  val find_reduct_iter_start :
    ?log:bool ->
    int ->
    Formula.formula ->
    Formula.formula ->
    smin:int -> smax:int -> dim:int -> ?fp:bool -> int * int -> unit
  val find_reduct_iter_step :
    ?log:bool ->
    int ->
    int ->
    Formula.formula ->
    Formula.formula -> int -> Reduction.reduction option * bool
  val find_reduct_iter_counterexample : unit -> Structure.structure
  val print_reduct_find :
    fmt:int ->
    ?fn:string ->
    ?log:bool ->
    int ->
    Formula.formula ->
    Formula.formula ->
    size:int * int ->
    dim:int -> ?fp:bool -> ?expand:int -> int * int -> string
end