functor (V : Variables) ->
  sig
    type var = V.t
    type t_raw = Empty | Unit | And of var * t * t * t
    and t = 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 : t -> var diag
    val build : var diag -> t
    val clear : unit -> unit
    val cEmpty : t
    val cUnit : t
    val cAnd : var * t * t * t -> t
    val diag_of_cnf : var list list -> t
    val diag_str : ?vars:bool -> t -> string
    val log : string -> var -> t -> var list -> unit
    val size : t -> int * int
    val vars : t -> (var * int) list
    val singletons : t -> var list
    val mk_and : t -> t -> t
    val mk_or : t -> t -> t
    val propagate_once : var list -> t -> t
    val propagate : var list -> t -> t
    val remove : var -> t -> t
    val elim_var :
      ?log:bool ->
      ?bound:int option -> ?sat:bool -> ?universal:bool -> var -> t -> t
    val elim_top_until : ?log:bool -> int -> t -> t
    val top_reduce : ?log:bool -> int -> t -> t
    val top_sat : ?log:bool -> t -> bool
    val elim_sat : t -> bool
    val mixed_sat : ?log:bool -> t -> bool
    val elim_bounded :
      ?universal:bool -> ?until:(var -> bool) -> ?sat:bool -> int -> t -> t
    val elim_bounded_sat : t -> bool
    val formula : t -> QBF.bool_formula
  end