sig
  type var = int
  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