sig
  type ('a, 'b, 'c, 'd) t = {
    symbol : 'a Env.symbol;
    compare_cond : 'c -> 'c -> int;
    negate_cond : 'b -> 'c -> 'c;
    support_cond : 'b -> 'c -> 'a PSette.t;
    mutable print_cond : 'b -> Format.formatter -> 'c -> unit;
    mutable cudd : 'd Cudd.Man.t;
    mutable bddindex0 : int;
    mutable bddsize : int;
    mutable bddindex : int;
    mutable bddincr : int;
    mutable condidb : ('c, int * bool) PDMappe.t;
    mutable supp : 'd Cudd.Bdd.t;
    mutable careset : 'd Cudd.Bdd.t;
  }
  val print : 'a -> Format.formatter -> ('b, 'a, 'c, 'd) Cond.t -> unit
  val make :
    symbol:'a Env.symbol ->
    compare_cond:('b -> 'b -> int) ->
    negate_cond:('c -> 'b -> 'b) ->
    support_cond:('c -> 'b -> 'a PSette.t) ->
    print_cond:('c -> Format.formatter -> 'b -> unit) ->
    ?bddindex0:int ->
    ?bddsize:int -> 'd Cudd.Man.t -> ('a, 'c, 'b, 'd) Cond.t
  val copy : ('a, 'b, 'c, 'd) Cond.t -> ('a, 'b, 'c, 'd) Cond.t
  val permutation : ('a, 'b, 'c, 'd) Cond.t -> int array
  val permute_with : ('a, 'b, 'c, 'd) Cond.t -> int array -> unit
  val normalize_with : ('a, 'b, 'c, 'd) Cond.t -> int array
  val reduce_with : ('a, 'b, 'c, 'd) Cond.t -> 'd Cudd.Bdd.t -> unit
  val clear : ('a, 'b, 'c, 'd) Cond.t -> unit
  val check_normalized : 'a -> ('b, 'a, 'c, 'd) Cond.t -> bool
  val cond_of_idb : ('a, 'b, 'c, 'd) Cond.t -> int * bool -> 'c
  val idb_of_cond : 'a -> ('b, 'a, 'c, 'd) Cond.t -> 'c -> int * bool
  val compute_careset : ('a, 'b, 'c, 'd) Cond.t -> normalized:bool -> unit
  val is_leq : ('a, 'b, 'c, 'd) Cond.t -> ('a, 'b, 'c, 'd) Cond.t -> bool
  val is_eq : ('a, 'b, 'c, 'd) Cond.t -> ('a, 'b, 'c, 'd) Cond.t -> bool
  val shift : ('a, 'b, 'c, 'd) Cond.t -> int -> ('a, 'b, 'c, 'd) Cond.t
  val lce :
    ('a, 'b, 'c, 'd) Cond.t ->
    ('a, 'b, 'c, 'd) Cond.t -> ('a, 'b, 'c, 'd) Cond.t
  val permutation12 :
    ('a, 'b, 'c, 'd) Cond.t -> ('a, 'b, 'c, 'd) Cond.t -> int array
  val permutation21 :
    ('a, 'b, 'c, 'd) Cond.t -> ('a, 'b, 'c, 'd) Cond.t -> int array
  type ('a, 'b) value = { cond : 'a; val1 : 'b; }
  val make_value : 'a -> 'b -> ('a, 'b) Cond.value
  val get_cond : ('a, 'b) Cond.value -> 'a
  val get_val1 : ('a, 'b) Cond.value -> 'b
  val get_env : ('a, ('b, 'c) Env.value) Cond.value -> 'b
  val get_val0 : ('a, ('b, 'c) Env.value) Cond.value -> 'c
end