sig
  type var
  type t_raw =
      Empty
    | Unit
    | And of Diagram.S.var * Diagram.S.t * Diagram.S.t * Diagram.S.t
  and t = Diagram.S.t_raw HashCons.hc
  module DiagCons :
    sig
      type data = t_raw
      type t
      val create : int -> t
      val clear : t -> unit
      val hashcons : ?log:bool -> t -> data -> data HashCons.hc
      module H1 :
        sig
          type key = data HashCons.hc
          type 'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
        end
      module H2 :
        sig
          type key = data HashCons.hc * data HashCons.hc
          type 'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
        end
      type other_value = var list
      module HV :
        sig
          type key = data HashCons.hc * other_value
          type 'a t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val reset : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val length : 'a t -> int
          val stats : 'a t -> Hashtbl.statistics
        end
      val get_h1 : t -> data HashCons.hc H1.t
      val get_h2 : t -> data HashCons.hc H2.t
      val get_hv : t -> data HashCons.hc HV.t
      val get_h1_alpha :
        (module HashCons.Type with type t = 'a) -> t -> 'a H1.t
    end
  val get : Diagram.S.t -> Diagram.S.var Diagram.diag
  val build : Diagram.S.var Diagram.diag -> Diagram.S.t
  val clear : unit -> unit
  val cEmpty : Diagram.S.t
  val cUnit : Diagram.S.t
  val cAnd :
    Diagram.S.var * Diagram.S.t * Diagram.S.t * Diagram.S.t -> Diagram.S.t
  val diag_of_cnf : Diagram.S.var list list -> Diagram.S.t
  val diag_str : ?vars:bool -> Diagram.S.t -> string
  val log :
    string -> Diagram.S.var -> Diagram.S.t -> Diagram.S.var list -> unit
  val size : Diagram.S.t -> int * int
  val vars : Diagram.S.t -> (Diagram.S.var * int) list
  val singletons : Diagram.S.t -> Diagram.S.var list
  val mk_and : Diagram.S.t -> Diagram.S.t -> Diagram.S.t
  val mk_or : Diagram.S.t -> Diagram.S.t -> Diagram.S.t
  val propagate_once : Diagram.S.var list -> Diagram.S.t -> Diagram.S.t
  val propagate : Diagram.S.var list -> Diagram.S.t -> Diagram.S.t
  val remove : Diagram.S.var -> Diagram.S.t -> Diagram.S.t
  val elim_var :
    ?log:bool ->
    ?bound:int option ->
    ?sat:bool ->
    ?universal:bool -> Diagram.S.var -> Diagram.S.t -> Diagram.S.t
  val elim_top_until : ?log:bool -> int -> Diagram.S.t -> Diagram.S.t
  val top_reduce : ?log:bool -> int -> Diagram.S.t -> Diagram.S.t
  val top_sat : ?log:bool -> Diagram.S.t -> bool
  val elim_sat : Diagram.S.t -> bool
  val mixed_sat : ?log:bool -> Diagram.S.t -> bool
  val elim_bounded :
    ?universal:bool ->
    ?until:(Diagram.S.var -> bool) ->
    ?sat:bool -> int -> Diagram.S.t -> Diagram.S.t
  val elim_bounded_sat : Diagram.S.t -> bool
  val formula : Diagram.S.t -> QBF.bool_formula
end