sig
  type bool_formula =
      BVar of int
    | BNot of BoolFormula.bool_formula
    | BAnd of BoolFormula.bool_formula list
    | BOr of BoolFormula.bool_formula list
  val var_str : int -> string
  val str :
    ?names:(int, string) Hashtbl.t -> BoolFormula.bool_formula -> string
  val flatten_sort : BoolFormula.bool_formula -> BoolFormula.bool_formula
  val bool_formula_of_formula : Formula.formula -> BoolFormula.bool_formula
  val formula_of_bool_formula_arg :
    BoolFormula.bool_formula ->
    (Formula.formula, int) Hashtbl.t * (int, Formula.formula) Hashtbl.t *
    int Pervasives.ref -> Formula.formula
  val bool_formula_of_formula_arg :
    Formula.formula ->
    (Formula.formula, int) Hashtbl.t * (int, Formula.formula) Hashtbl.t *
    int Pervasives.ref -> BoolFormula.bool_formula
  val simplify : BoolFormula.bool_formula -> BoolFormula.bool_formula
  val full_simplify : BoolFormula.bool_formula -> BoolFormula.bool_formula
  val sort : BoolFormula.bool_formula -> BoolFormula.bool_formula
  val auxcnf_of_bool_formula :
    BoolFormula.bool_formula -> int * BoolFormula.bool_formula
  val pg_auxcnf_of_bool_formula :
    ?setmax:int -> BoolFormula.bool_formula -> int * BoolFormula.bool_formula
  val to_reduced_form :
    ?neg:bool -> BoolFormula.bool_formula -> BoolFormula.bool_formula
  val to_nnf :
    ?neg:bool -> BoolFormula.bool_formula -> BoolFormula.bool_formula
  val cnf_of_bool_formula :
    ?use_pg:bool ->
    ?setmax:int -> BoolFormula.bool_formula -> int * int list list
  val print_dimacs : int list list -> unit
  val find_model :
    ?logtime:float ->
    ?logprefix:string -> BoolFormula.bool_formula -> int list option
  val convert :
    ?disc_vars:int list -> BoolFormula.bool_formula -> int list list
  val formula_to_cnf : Formula.formula -> Formula.formula
  val to_cnf :
    ?disc_vars:int list ->
    ?tm:float -> BoolFormula.bool_formula -> BoolFormula.bool_formula option
  val to_dnf :
    ?disc_vars:int list ->
    ?tm:float -> BoolFormula.bool_formula -> BoolFormula.bool_formula option
  val to_sat :
    ?tm:float -> BoolFormula.bool_formula -> BoolFormula.bool_formula option
  val elim_all :
    int list -> BoolFormula.bool_formula -> BoolFormula.bool_formula
  val elim_ex :
    int list -> BoolFormula.bool_formula -> BoolFormula.bool_formula
  type qbf_raw =
      QVar of int
    | QNot of BoolFormula.qbf
    | QAnd of BoolFormula.qbf list
    | QOr of BoolFormula.qbf list
    | QEx of int list * BoolFormula.qbf
    | QAll of int list * BoolFormula.qbf
  and qbf = BoolFormula.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 : BoolFormula.qbf_raw -> BoolFormula.qbf
  val clear_qbf_consing : unit -> unit
  val qbf_of_bf : BoolFormula.bool_formula -> BoolFormula.qbf
  val qbf_str : ?names:(int, string) Hashtbl.t -> BoolFormula.qbf -> string
  val nnf : ?neg:bool -> BoolFormula.qbf -> BoolFormula.qbf
  val has_quantifiers : BoolFormula.qbf -> bool
  val read_qdimacs : string -> BoolFormula.qbf
  val elim_quant : BoolFormula.qbf -> BoolFormula.bool_formula
  val sat_of_qbf : BoolFormula.qbf -> BoolFormula.bool_formula
  val free_vars : BoolFormula.qbf -> int list
  val max_var : BoolFormula.qbf -> int
  val iter_vars : (int -> unit) -> BoolFormula.qbf -> unit
  val flatten_qbf : ?unit_prop:bool -> BoolFormula.qbf -> BoolFormula.qbf
  val unique : BoolFormula.qbf list -> BoolFormula.qbf list
  val subst :
    (int, BoolFormula.qbf) Hashtbl.t -> BoolFormula.qbf -> BoolFormula.qbf
  val find_model_qbf :
    ?maximize:bool ->
    ?logtime:float -> ?logprefix:string -> BoolFormula.qbf -> int list option
  val force_order : BoolFormula.qbf -> int array
  val print_qdimacs : ?negate:bool -> BoolFormula.qbf -> string
  val print_qpro : BoolFormula.qbf -> string
  val print_lparse : ?universal_vars:int list -> BoolFormula.qbf -> string
end