sig
  type qbf_raw =
      QVar of int
    | QNot of QBF.qbf
    | QAnd of QBF.qbf list
    | QOr of QBF.qbf list
    | QEx of int list * QBF.qbf
    | QAll of int list * QBF.qbf
  and qbf = QBF.qbf_raw HashCons.hc
  module QBFCons :
    sig
      type data = qbf_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 = int 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 qbf_hc : QBF.qbf_raw -> QBF.qbf
  val clear_qbf_consing : unit -> unit
  val read_ppm : ?xd:int -> ?yd:int -> string -> QBF.qbf array array list
  val read_qdimacs : string -> QBF.qbf
  val qbf_str : ?names:(int, string) Hashtbl.t -> QBF.qbf -> string
  val dag_str : ?names:(int, string) Hashtbl.t -> QBF.qbf -> string
  val size : QBF.qbf -> int * int
  val nnf : ?neg:bool -> QBF.qbf -> QBF.qbf
  val has_quantifiers : QBF.qbf -> bool
  val free_vars : QBF.qbf -> int list
  val free_vars_hash : QBF.qbf -> (int, unit) Hashtbl.t -> unit
  val max_var : QBF.qbf -> int
  val iter_vars : (int -> unit) -> QBF.qbf -> unit
  val flatten_qbf : ?unit_prop:bool -> QBF.qbf -> QBF.qbf
  val unique : QBF.qbf list -> QBF.qbf list
  val to_array : int -> QBF.qbf list -> QBF.qbf array * QBF.qbf list
  val binary_add :
    ?carry:QBF.qbf ->
    QBF.qbf array -> QBF.qbf array -> QBF.qbf array * QBF.qbf
  val unary_add : QBF.qbf array -> QBF.qbf array -> QBF.qbf array
  val binary_sub : QBF.qbf array -> QBF.qbf array -> QBF.qbf array
  val binary_minus : QBF.qbf array -> QBF.qbf array
  val binary_abs : QBF.qbf array -> QBF.qbf array
  val unsigned_gt : QBF.qbf array -> QBF.qbf array -> QBF.qbf
  val sum_gt0 :
    ?unary:bool -> ?bits:QBF.qbf list -> QBF.qbf array list -> QBF.qbf
  val use_sum_gates : bool Pervasives.ref
  val convolve :
    ?unary:bool ->
    int ->
    QBF.qbf array list -> QBF.qbf array array list -> QBF.qbf array array
  val maxpool : QBF.qbf array array -> QBF.qbf array array
  val nbits : int Pervasives.ref
  val make_layer :
    int ->
    ?unary:bool ->
    ?weights:QBF.qbf array list list ->
    ?minvar:int ->
    ?maxpool:bool ->
    int ->
    QBF.qbf array array list ->
    QBF.qbf array array list * QBF.qbf array list list * int * QBF.qbf
  val subst : (int, QBF.qbf) Hashtbl.t -> QBF.qbf -> QBF.qbf
  val no_external : int Pervasives.ref
  val find_model_qbf :
    ?maximize:bool ->
    ?logtime:float -> ?logprefix:string -> QBF.qbf -> int list option
  val find_model_qbf_qf :
    ?maximize:bool ->
    ?logtime:float -> ?logprefix:string -> QBF.qbf -> int list option
  val force_order : QBF.qbf -> int array
  val simplify : QBF.qbf -> QBF.qbf
  val convert : ?disc_vars:int list -> QBF.qbf -> int list list
  val formula_to_cnf : Formula.formula -> Formula.formula
  val simplify_formula : Formula.formula -> Formula.formula
  val print_dimacs : int list list -> unit
  val print_qdimacs : QBF.qbf -> string
  val print_qiscas : ?prenex:bool -> QBF.qbf -> string
  val print_cqbf : QBF.qbf -> string
  val print_qpro : QBF.qbf -> string
  val print_lparse : ?universal_vars:int list -> QBF.qbf -> string
  type bool_formula =
      BVar of int
    | BNot of QBF.bool_formula
    | BAnd of QBF.bool_formula list
    | BOr of QBF.bool_formula list
  val bf_str : ?names:(int, string) Hashtbl.t -> QBF.bool_formula -> string
  val qbf_of_bf : QBF.bool_formula -> QBF.qbf
  val sat_of_qbf : QBF.qbf -> QBF.bool_formula
end