sig
  type var =
      [ `Const of string | `FO of string | `Real of string | `SO of string ]
  type const_var = [ `Const of string ]
  type fo_var = [ `FO of string ]
  type const_or_fo_var = [ `Const of string | `FO of string ]
  type so_var = [ `SO of string ]
  type real_var = [ `Real of string ]
  val var_of_string : string -> Formula.var
  val const_var_of_string : string -> Formula.const_var
  val fo_var_of_string : string -> Formula.fo_var
  val const_or_fo_var_of_string : string -> Formula.const_or_fo_var
  val so_var_of_string : string -> Formula.so_var
  val real_var_of_string : string -> Formula.real_var
  val is_const : Formula.var -> bool
  val is_fo : Formula.var -> bool
  val is_so : Formula.var -> bool
  val is_real : Formula.var -> bool
  val to_const : Formula.var -> Formula.const_var
  val to_fo : Formula.var -> Formula.fo_var
  val to_const_or_fo : Formula.var -> Formula.const_or_fo_var
  val to_so : Formula.var -> Formula.so_var
  val to_real : Formula.var -> Formula.real_var
  val var_tup : [< Formula.var ] array -> Formula.var array
  val compare_vars : ([< Formula.var ] as 'a) -> '-> int
  val compare_var_lists : ([< Formula.var ] as 'a) list -> 'a list -> int
  val compare_var_tups : ([< Formula.var ] as 'a) array -> 'a array -> int
  type sign_op = EQZero | GZero | LZero | GEQZero | LEQZero | NEQZero
  val sign_op_str : ?unicode:bool -> Formula.sign_op -> string
  type formula =
      Rel of string * Formula.const_or_fo_var array
    | Eq of Formula.const_or_fo_var * Formula.const_or_fo_var
    | SO of Formula.so_var * Formula.const_or_fo_var array
    | RealExpr of Formula.real_expr * Formula.sign_op
    | Not of Formula.formula
    | And of Formula.formula list
    | Or of Formula.formula list
    | Ex of Formula.var list * Formula.formula
    | All of Formula.var list * Formula.formula
    | Lfp of Formula.so_var * Formula.fo_var array * Formula.formula
    | Gfp of Formula.so_var * Formula.fo_var array * Formula.formula
    | Let of string * string list * Formula.formula * Formula.formula
  and real_expr =
      RVar of string
    | Const of float
    | Plus of Formula.real_expr * Formula.real_expr
    | Times of Formula.real_expr * Formula.real_expr
    | Pow of Formula.real_expr * Formula.real_expr
    | Fun of string * Formula.const_or_fo_var
    | Char of Formula.formula
    | Sum of Formula.fo_var list * Formula.formula * Formula.real_expr
    | RLet of string * Formula.real_expr * Formula.real_expr
  val size : ?acc:int -> Formula.formula -> int
  val size_real : ?acc:int -> Formula.real_expr -> int
  val so_compare_weight : int Pervasives.ref
  val compare : Formula.formula -> Formula.formula -> int
  val compare_re : Formula.real_expr -> Formula.real_expr -> int
  val is_atom : Formula.formula -> bool
  val is_literal : Formula.formula -> bool
  type eq_sys = ((string * string) * Formula.real_expr) list
  val var_str : [< Formula.var ] -> string
  val var_list_str : [< Formula.var ] list -> string
  val str : ?unicode:bool -> Formula.formula -> string
  val mona_str : Formula.formula -> string
  val print : ?unicode:bool -> Formula.formula -> unit
  val sprint : ?unicode:bool -> Formula.formula -> string
  val fprint : ?unicode:bool -> Format.formatter -> Formula.formula -> unit
  val real_str : ?unicode:bool -> Formula.real_expr -> string
  val print_real : ?unicode:bool -> Formula.real_expr -> unit
  val sprint_real : ?unicode:bool -> Formula.real_expr -> string
  val fprint_real :
    ?unicode:bool -> Format.formatter -> Formula.real_expr -> unit
  val fprint_prec :
    bool -> int -> Format.formatter -> Formula.formula -> unit
  val fprint_real_prec :
    bool -> int -> Format.formatter -> Formula.real_expr -> unit
  val fprint_eqs :
    ?unicode:bool -> ?diff:bool -> Format.formatter -> Formula.eq_sys -> unit
  val eq_str : ?unicode:bool -> ?diff:bool -> Formula.eq_sys -> string
  val syntax_ok :
    ?sg:(string * int) list Pervasives.ref ->
    ?fp:(string * bool) list -> ?pos:bool -> Formula.formula -> bool
  val syntax_ok_re :
    ?sg:(string * int) list Pervasives.ref ->
    ?fp:(string * bool) list -> ?pos:bool -> Formula.real_expr -> bool
  val flatten : Formula.formula -> Formula.formula
  val flatten_re : Formula.real_expr -> Formula.real_expr
  val flatten_sort : Formula.formula -> Formula.formula
  val flatten_sort_re : Formula.real_expr -> Formula.real_expr
  val compile :
    string -> Formula.eq_sys -> float -> float array -> float array
  val rk4_step :
    float ->
    float ->
    (float -> float array -> float array) -> float array -> float array
  val rkCK_default_start :
    unit ->
    float Pervasives.ref * float Pervasives.ref * float Pervasives.ref *
    float Pervasives.ref
  val rkCK_step :
    ?epsilon:float ->
    float Pervasives.ref * float Pervasives.ref * float Pervasives.ref *
    float Pervasives.ref ->
    float ->
    float ->
    (float -> float array -> float array) ->
    float array -> float array * float * float
  type raw_formula =
      HRel of string * Formula.const_or_fo_var array
    | HEq of Formula.const_or_fo_var * Formula.const_or_fo_var
    | HSO of Formula.so_var * Formula.const_or_fo_var array
    | HRealExpr of Formula.hc_real_expr * Formula.sign_op
    | HNot of Formula.hc_formula
    | HAnd of Formula.hc_formula list
    | HOr of Formula.hc_formula list
    | HEx of Formula.var list * Formula.hc_formula
    | HAll of Formula.var list * Formula.hc_formula
    | HLfp of Formula.so_var * Formula.fo_var array * Formula.hc_formula
    | HGfp of Formula.so_var * Formula.fo_var array * Formula.hc_formula
    | HLet of string * string list * Formula.hc_formula * Formula.hc_formula
  and raw_real_expr =
      HRVar of string
    | HConst of float
    | HPlus of Formula.hc_real_expr * Formula.hc_real_expr
    | HTimes of Formula.hc_real_expr * Formula.hc_real_expr
    | HPow of Formula.hc_real_expr * Formula.hc_real_expr
    | HFun of string * Formula.const_or_fo_var
    | HChar of Formula.hc_formula
    | HSum of Formula.fo_var list * Formula.hc_formula * Formula.hc_real_expr
    | HRLet of string * Formula.hc_real_expr * Formula.hc_real_expr
  and hc_formula = Formula.raw_formula HashCons.hc
  and hc_real_expr = Formula.raw_real_expr HashCons.hc
  module FormulaCons :
    sig
      type data = raw_formula
      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 -> '-> 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 -> '-> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> 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 -> '-> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> 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 -> '-> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> 'H1.t
    end
  module RealExprCons :
    sig
      type data = raw_real_expr
      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 -> '-> 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 -> '-> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> 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 -> '-> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> 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 -> '-> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> '-> unit) -> 'a t -> unit
          val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> 'H1.t
    end
  val hc : Formula.formula -> Formula.hc_formula
  val hc_real : Formula.real_expr -> Formula.hc_real_expr
  val cAnd : Formula.hc_formula list -> Formula.hc_formula
  val unhc : Formula.hc_formula -> Formula.formula
  val unhc_real : Formula.hc_real_expr -> Formula.real_expr
end