sig
  type 'a context
  module Env :
    sig
      type 'a t
      val empty : 'a Syntax.Env.t
      val push : 'a -> 'a Syntax.Env.t -> 'a Syntax.Env.t
      val find : 'a Syntax.Env.t -> int -> 'a
      val enum : 'a Syntax.Env.t -> 'a BatEnum.t
    end
  type typ_arith = [ `TyInt | `TyReal ]
  type typ_fo = [ `TyBool | `TyInt | `TyReal ]
  type typ =
      [ `TyBool
      | `TyFun of Syntax.typ_fo list * Syntax.typ_fo
      | `TyInt
      | `TyReal ]
  type typ_bool = [ `TyBool ]
  type 'a typ_fun = [ `TyFun of Syntax.typ_fo list * 'a ]
  val pp_typ : Format.formatter -> [< Syntax.typ ] -> unit
  type symbol
  val mk_symbol :
    'a Syntax.context -> ?name:string -> Syntax.typ -> Syntax.symbol
  val register_named_symbol :
    'a Syntax.context -> string -> Syntax.typ -> unit
  val is_registered_name : 'a Syntax.context -> string -> bool
  val get_named_symbol : 'a Syntax.context -> string -> Syntax.symbol
  val symbol_name : 'a Syntax.context -> Syntax.symbol -> string option
  val pp_symbol :
    'a Syntax.context -> Format.formatter -> Syntax.symbol -> unit
  val typ_symbol : 'a Syntax.context -> Syntax.symbol -> Syntax.typ
  val show_symbol : 'a Syntax.context -> Syntax.symbol -> string
  val int_of_symbol : Syntax.symbol -> int
  val symbol_of_int : int -> Syntax.symbol
  val compare_symbol : Syntax.symbol -> Syntax.symbol -> int
  module Symbol :
    sig
      type t = Syntax.symbol
      val compare : Syntax.Symbol.t -> Syntax.Symbol.t -> int
      module Set :
        sig
          type elt = symbol
          type t
          val empty : t
          val is_empty : t -> bool
          val singleton : elt -> t
          val mem : elt -> t -> bool
          val find : elt -> t -> elt
          val add : elt -> t -> t
          val remove : elt -> t -> t
          val update : elt -> elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val sym_diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val disjoint : t -> t -> bool
          val compare_subset : t -> t -> int
          val iter : (elt -> unit) -> t -> unit
          val at_rank_exn : int -> t -> elt
          val map : (elt -> elt) -> t -> t
          val filter : (elt -> bool) -> t -> t
          val filter_map : (elt -> elt option) -> t -> t
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val partition : (elt -> bool) -> t -> t * t
          val split : elt -> t -> t * bool * t
          val split_opt : elt -> t -> t * elt option * t
          val split_lt : elt -> t -> t * t
          val split_le : elt -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val to_list : t -> elt list
          val to_array : t -> elt array
          val min_elt : t -> elt
          val pop_min : t -> elt * t
          val pop_max : t -> elt * t
          val max_elt : t -> elt
          val choose : t -> elt
          val pop : t -> elt * t
          val enum : t -> elt BatEnum.t
          val backwards : t -> elt BatEnum.t
          val of_enum : elt BatEnum.t -> t
          val of_list : elt list -> t
          val of_array : elt array -> t
          val print :
            ?first:string ->
            ?last:string ->
            ?sep:string ->
            ('a BatInnerIO.output -> elt -> unit) ->
            'a BatInnerIO.output -> t -> unit
          module Infix :
            sig
              val ( <-- ) : t -> elt -> t
              val ( <. ) : t -> t -> bool
              val ( >. ) : t -> t -> bool
              val ( <=. ) : t -> t -> bool
              val ( >=. ) : t -> t -> bool
              val ( -. ) : t -> t -> t
              val ( &&. ) : t -> t -> t
              val ( ||. ) : t -> t -> t
            end
          module Exceptionless :
            sig
              val min_elt : t -> elt option
              val max_elt : t -> elt option
              val choose : t -> elt option
              val find : elt -> t -> elt option
            end
          module Labels :
            sig
              val iter : f:(elt -> unit) -> t -> unit
              val fold : f:(elt -> 'a -> 'a) -> t -> init:'a -> 'a
              val for_all : f:(elt -> bool) -> t -> bool
              val exists : f:(elt -> bool) -> t -> bool
              val map : f:(elt -> elt) -> t -> t
              val filter : f:(elt -> bool) -> t -> t
              val filter_map : f:(elt -> elt option) -> t -> t
              val partition : f:(elt -> bool) -> t -> t * t
            end
        end
      module Map :
        sig
          type key = symbol
          type +'a t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val cardinal : 'a t -> int
          val add : key -> 'a -> 'a t -> 'a t
          val update : key -> key -> 'a -> 'a t -> 'a t
          val find : key -> 'a t -> 'a
          val remove : key -> 'a t -> 'a t
          val modify : key -> ('a -> 'a) -> 'a t -> 'a t
          val modify_def : 'a -> key -> ('a -> 'a) -> 'a t -> 'a t
          val modify_opt : key -> ('a option -> 'a option) -> 'a t -> 'a t
          val extract : key -> 'a t -> 'a * 'a t
          val pop : 'a t -> (key * 'a) * 'a t
          val mem : key -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val filterv : ('a -> bool) -> 'a t -> 'a t
          val filter : (key -> 'a -> bool) -> 'a t -> 'a t
          val filter_map : (key -> 'a -> 'b option) -> 'a t -> 'b t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
          val keys : 'a t -> key BatEnum.t
          val values : 'a t -> 'a BatEnum.t
          val min_binding : 'a t -> key * 'a
          val pop_min_binding : 'a t -> (key * 'a) * 'a t
          val max_binding : 'a t -> key * 'a
          val pop_max_binding : 'a t -> (key * 'a) * 'a t
          val choose : 'a t -> key * 'a
          val split : key -> 'a t -> 'a t * 'a option * 'a t
          val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
          val singleton : key -> 'a -> 'a t
          val bindings : 'a t -> (key * 'a) list
          val enum : 'a t -> (key * 'a) BatEnum.t
          val backwards : 'a t -> (key * 'a) BatEnum.t
          val of_enum : (key * 'a) BatEnum.t -> 'a t
          val for_all : (key -> 'a -> bool) -> 'a t -> bool
          val exists : (key -> 'a -> bool) -> 'a t -> bool
          val merge :
            (key -> 'a option -> 'b option -> 'c option) ->
            'a t -> 'b t -> 'c t
          val print :
            ?first:string ->
            ?last:string ->
            ?sep:string ->
            ?kvsep:string ->
            ('a BatInnerIO.output -> key -> unit) ->
            ('a BatInnerIO.output -> 'c -> unit) ->
            'a BatInnerIO.output -> 'c t -> unit
          module Exceptionless : sig val find : key -> 'a t -> 'a option end
          module Infix :
            sig
              val ( --> ) : 'a t -> key -> 'a
              val ( <-- ) : 'a t -> key * 'a -> 'a t
            end
          module Labels :
            sig
              val add : key:key -> data:'a -> 'a t -> 'a t
              val iter : f:(key:key -> data:'a -> unit) -> 'a t -> unit
              val map : f:('a -> 'b) -> 'a t -> 'b t
              val mapi : f:(key:key -> data:'a -> 'b) -> 'a t -> 'b t
              val filterv : f:('a -> bool) -> 'a t -> 'a t
              val filter : f:(key -> 'a -> bool) -> 'a t -> 'a t
              val fold :
                f:(key:key -> data:'a -> 'b -> 'b) -> 'a t -> init:'b -> 'b
              val compare : cmp:('a -> 'a -> int) -> 'a t -> 'a t -> int
              val equal : cmp:('a -> 'a -> bool) -> 'a t -> 'a t -> bool
            end
        end
    end
  type ('a, +'typ) expr
  type 'a term = ('a, Syntax.typ_arith) Syntax.expr
  type 'a formula = ('a, Syntax.typ_bool) Syntax.expr
  val compare_expr : ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr -> int
  val compare_formula : 'a Syntax.formula -> 'a Syntax.formula -> int
  val compare_term : 'a Syntax.term -> 'a Syntax.term -> int
  val destruct :
    'a Syntax.context ->
    ('a, 'b) Syntax.expr ->
    [ `Add of 'a Syntax.term list
    | `And of 'a Syntax.formula list
    | `App of Syntax.symbol * ('a, Syntax.typ_fo) Syntax.expr list
    | `Atom of [ `Eq | `Leq | `Lt ] * 'a Syntax.term * 'a Syntax.term
    | `Binop of [ `Div | `Mod ] * 'a Syntax.term * 'a Syntax.term
    | `Fls
    | `Ite of 'a Syntax.formula * ('a, 'b) Syntax.expr * ('a, 'b) Syntax.expr
    | `Mul of 'a Syntax.term list
    | `Not of 'a Syntax.formula
    | `Or of 'a Syntax.formula list
    | `Proposition of
        [ `App of Syntax.symbol * ('b, Syntax.typ_fo) Syntax.expr list
        | `Var of int ]
    | `Quantify of
        [ `Exists | `Forall ] * string * Syntax.typ_fo * 'a Syntax.formula
    | `Real of QQ.t
    | `Tru
    | `Unop of [ `Floor | `Neg ] * 'a Syntax.term
    | `Var of int * Syntax.typ_arith ]
  val expr_typ : 'a Syntax.context -> ('a, 'b) Syntax.expr -> Syntax.typ
  val free_vars : ('a, 'b) Syntax.expr -> (int, Syntax.typ_fo) BatHashtbl.t
  val size : ('a, 'b) Syntax.expr -> int
  val mk_const : 'a Syntax.context -> Syntax.symbol -> ('a, 'typ) Syntax.expr
  val mk_app :
    'a Syntax.context ->
    Syntax.symbol -> ('a, 'b) Syntax.expr list -> ('a, 'typ) Syntax.expr
  val mk_var :
    'a Syntax.context -> int -> Syntax.typ_fo -> ('a, 'typ) Syntax.expr
  val mk_ite :
    'a Syntax.context ->
    'a Syntax.formula ->
    ('a, 'typ) Syntax.expr ->
    ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr
  val mk_if :
    'a Syntax.context ->
    'a Syntax.formula -> 'a Syntax.formula -> 'a Syntax.formula
  val mk_iff :
    'a Syntax.context ->
    'a Syntax.formula -> 'a Syntax.formula -> 'a Syntax.formula
  val substitute :
    'a Syntax.context ->
    (int -> ('a, 'b) Syntax.expr) ->
    ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr
  val substitute_const :
    'a Syntax.context ->
    (Syntax.symbol -> ('a, 'b) Syntax.expr) ->
    ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr
  val substitute_map :
    'a Syntax.context ->
    ('a, 'b) Syntax.expr Syntax.Symbol.Map.t ->
    ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr
  val fold_constants :
    (Syntax.symbol -> 'a -> 'a) -> ('b, 'c) Syntax.expr -> 'a -> 'a
  val symbols : ('a, 'b) Syntax.expr -> Syntax.Symbol.Set.t
  type 'a rewriter =
      ('a, Syntax.typ_fo) Syntax.expr -> ('a, Syntax.typ_fo) Syntax.expr
  val rewrite :
    'a Syntax.context ->
    ?down:'a Syntax.rewriter ->
    ?up:'a Syntax.rewriter ->
    ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.expr
  val nnf_rewriter : 'a Syntax.context -> 'a Syntax.rewriter
  module Expr :
    sig
      val equal : ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr -> bool
      val compare : ('a, 'b) Syntax.expr -> ('a, 'b) Syntax.expr -> int
      val pp :
        ?env:string Syntax.Env.t ->
        'a Syntax.context -> Format.formatter -> ('a, 'b) Syntax.expr -> unit
      val refine :
        'a Syntax.context ->
        ('a, Syntax.typ_fo) Syntax.expr ->
        [ `Formula of 'a Syntax.formula | `Term of 'a Syntax.term ]
      module HT :
        sig
          type ('a, 'typ, 'b) t
          val create : int -> ('a, 'typ, 'b) Syntax.Expr.HT.t
          val add :
            ('a, 'typ, 'b) Syntax.Expr.HT.t ->
            ('a, 'typ) Syntax.expr -> 'b -> unit
          val replace :
            ('a, 'typ, 'b) Syntax.Expr.HT.t ->
            ('a, 'typ) Syntax.expr -> 'b -> unit
          val remove :
            ('a, 'typ, 'b) Syntax.Expr.HT.t -> ('a, 'typ) Syntax.expr -> unit
          val find :
            ('a, 'typ, 'b) Syntax.Expr.HT.t -> ('a, 'typ) Syntax.expr -> 'b
          val mem :
            ('a, 'typ, 'b) Syntax.Expr.HT.t -> ('a, 'typ) Syntax.expr -> bool
          val keys :
            ('a, 'typ, 'b) Syntax.Expr.HT.t ->
            ('a, 'typ) Syntax.expr BatEnum.t
          val values : ('a, 'typ, 'b) Syntax.Expr.HT.t -> 'b BatEnum.t
          val enum :
            ('a, 'typ, 'b) Syntax.Expr.HT.t ->
            (('a, 'typ) Syntax.expr * 'b) BatEnum.t
        end
      module Set :
        sig
          type ('a, 'typ) t
          val empty : ('a, 'typ) Syntax.Expr.Set.t
          val add :
            ('a, 'typ) Syntax.expr ->
            ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.Expr.Set.t
          val union :
            ('a, 'typ) Syntax.Expr.Set.t ->
            ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.Expr.Set.t
          val inter :
            ('a, 'typ) Syntax.Expr.Set.t ->
            ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.Expr.Set.t
          val enum :
            ('a, 'typ) Syntax.Expr.Set.t -> ('a, 'typ) Syntax.expr BatEnum.t
          val mem :
            ('a, 'typ) Syntax.expr -> ('a, 'typ) Syntax.Expr.Set.t -> bool
        end
      module Map :
        sig
          type ('a, 'typ, 'b) t
          val empty : ('a, 'typ, 'b) Syntax.Expr.Map.t
          val is_empty : ('a, 'typ, 'b) Syntax.Expr.Map.t -> bool
          val add :
            ('a, 'typ) Syntax.expr ->
            'b ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t
          val remove :
            ('a, 'typ) Syntax.expr ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t
          val filter :
            (('a, 'typ) Syntax.expr -> 'b -> bool) ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t
          val filter_map :
            (('a, 'typ) Syntax.expr -> 'b -> 'c option) ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            ('a, 'typ, 'c) Syntax.Expr.Map.t
          val map :
            ('b -> 'c) ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            ('a, 'typ, 'c) Syntax.Expr.Map.t
          val find :
            ('a, 'typ) Syntax.expr -> ('a, 'typ, 'b) Syntax.Expr.Map.t -> 'b
          val keys :
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            ('a, 'typ) Syntax.expr BatEnum.t
          val values : ('a, 'typ, 'b) Syntax.Expr.Map.t -> 'b BatEnum.t
          val enum :
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            (('a, 'typ) Syntax.expr * 'b) BatEnum.t
          val merge :
            (('a, 'typ) Syntax.expr -> 'b option -> 'c option -> 'd option) ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t ->
            ('a, 'typ, 'c) Syntax.Expr.Map.t ->
            ('a, 'typ, 'd) Syntax.Expr.Map.t
          val fold :
            (('a, 'typ) Syntax.expr -> 'b -> 'c -> 'c) ->
            ('a, 'typ, 'b) Syntax.Expr.Map.t -> 'c -> 'c
        end
    end
  type ('a, 'b) open_term =
      [ `Add of 'a list
      | `App of Syntax.symbol * ('b, Syntax.typ_fo) Syntax.expr list
      | `Binop of [ `Div | `Mod ] * 'a * 'a
      | `Ite of 'b Syntax.formula * 'a * 'a
      | `Mul of 'a list
      | `Real of QQ.t
      | `Unop of [ `Floor | `Neg ] * 'a
      | `Var of int * Syntax.typ_arith ]
  val mk_add : 'a Syntax.context -> 'a Syntax.term list -> 'a Syntax.term
  val mk_mul : 'a Syntax.context -> 'a Syntax.term list -> 'a Syntax.term
  val mk_div :
    'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term -> 'a Syntax.term
  val mk_pow : 'a Syntax.context -> 'a Syntax.term -> int -> 'a Syntax.term
  val mk_idiv :
    'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term -> 'a Syntax.term
  val mk_mod :
    'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term -> 'a Syntax.term
  val mk_real : 'a Syntax.context -> QQ.t -> 'a Syntax.term
  val mk_floor : 'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term
  val mk_ceiling : 'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term
  val mk_truncate : 'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term
  val mk_neg : 'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term
  val mk_sub :
    'a Syntax.context -> 'a Syntax.term -> 'a Syntax.term -> 'a Syntax.term
  val term_typ : 'a Syntax.context -> 'a Syntax.term -> Syntax.typ_arith
  module Term :
    sig
      type 'a t = 'a Syntax.term
      val equal : 'a Syntax.term -> 'a Syntax.term -> bool
      val compare : 'a Syntax.term -> 'a Syntax.term -> int
      val hash : 'a Syntax.term -> int
      val pp :
        ?env:string Syntax.Env.t ->
        'a Syntax.context -> Format.formatter -> 'a Syntax.term -> unit
      val show :
        ?env:string Syntax.Env.t ->
        'a Syntax.context -> 'a Syntax.term -> string
      val destruct :
        'a Syntax.context ->
        'a Syntax.term -> ('a Syntax.term, 'a) Syntax.open_term
      val eval :
        'a Syntax.context ->
        (('b, 'a) Syntax.open_term -> 'b) -> 'a Syntax.term -> 'b
      val eval_partial :
        'a Syntax.context ->
        (('b, 'a) Syntax.open_term -> 'b option) ->
        'a Syntax.term -> 'b option
    end
  type ('a, 'b) open_formula =
      [ `And of 'a list
      | `Atom of [ `Eq | `Leq | `Lt ] * 'b Syntax.term * 'b Syntax.term
      | `Fls
      | `Ite of 'a * 'a * 'a
      | `Not of 'a
      | `Or of 'a list
      | `Proposition of
          [ `App of Syntax.symbol * ('b, Syntax.typ_fo) Syntax.expr list
          | `Var of int ]
      | `Quantify of [ `Exists | `Forall ] * string * Syntax.typ_fo * 'a
      | `Tru ]
  val mk_forall :
    'a Syntax.context ->
    ?name:string -> Syntax.typ_fo -> 'a Syntax.formula -> 'a Syntax.formula
  val mk_exists :
    'a Syntax.context ->
    ?name:string -> Syntax.typ_fo -> 'a Syntax.formula -> 'a Syntax.formula
  val mk_forall_const :
    'a Syntax.context ->
    Syntax.symbol -> 'a Syntax.formula -> 'a Syntax.formula
  val mk_exists_const :
    'a Syntax.context ->
    Syntax.symbol -> 'a Syntax.formula -> 'a Syntax.formula
  val mk_and :
    'a Syntax.context -> 'a Syntax.formula list -> 'a Syntax.formula
  val mk_or :
    'a Syntax.context -> 'a Syntax.formula list -> 'a Syntax.formula
  val mk_not : 'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
  val mk_eq :
    'a Syntax.context ->
    'a Syntax.term -> 'a Syntax.term -> 'a Syntax.formula
  val mk_lt :
    'a Syntax.context ->
    'a Syntax.term -> 'a Syntax.term -> 'a Syntax.formula
  val mk_leq :
    'a Syntax.context ->
    'a Syntax.term -> 'a Syntax.term -> 'a Syntax.formula
  val mk_true : 'a Syntax.context -> 'a Syntax.formula
  val mk_false : 'a Syntax.context -> 'a Syntax.formula
  val eliminate_ite :
    'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
  val pp_smtlib2 :
    ?env:string Syntax.Env.t ->
    'a Syntax.context -> Format.formatter -> 'a Syntax.formula -> unit
  module Formula :
    sig
      type 'a t = 'a Syntax.formula
      val equal : 'a Syntax.formula -> 'a Syntax.formula -> bool
      val compare : 'a Syntax.formula -> 'a Syntax.formula -> int
      val hash : 'a Syntax.formula -> int
      val pp :
        ?env:string Syntax.Env.t ->
        'a Syntax.context -> Format.formatter -> 'a Syntax.formula -> unit
      val show :
        ?env:string Syntax.Env.t ->
        'a Syntax.context -> 'a Syntax.formula -> string
      val destruct :
        'a Syntax.context ->
        'a Syntax.formula -> ('a Syntax.formula, 'a) Syntax.open_formula
      val eval :
        'a Syntax.context ->
        (('b, 'a) Syntax.open_formula -> 'b) -> 'a Syntax.formula -> 'b
      val eval_memo :
        'a Syntax.context ->
        (('b, 'a) Syntax.open_formula -> 'b) -> 'a Syntax.formula -> 'b
      val existential_closure :
        'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
      val universal_closure :
        'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
      val skolemize_free :
        'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
      val prenex :
        'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
    end
  module type Context =
    sig
      type t
      val context : Syntax.Context.t Syntax.context
      type term = (Syntax.Context.t, Syntax.typ_arith) Syntax.expr
      type formula = (Syntax.Context.t, Syntax.typ_bool) Syntax.expr
      val mk_symbol : ?name:string -> Syntax.typ -> Syntax.symbol
      val mk_const : Syntax.symbol -> (Syntax.Context.t, 'typ) Syntax.expr
      val mk_app :
        Syntax.symbol ->
        (Syntax.Context.t, 'b) Syntax.expr list ->
        (Syntax.Context.t, 'typ) Syntax.expr
      val mk_var :
        int -> Syntax.typ_fo -> (Syntax.Context.t, 'typ) Syntax.expr
      val mk_add : Syntax.Context.term list -> Syntax.Context.term
      val mk_mul : Syntax.Context.term list -> Syntax.Context.term
      val mk_div :
        Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
      val mk_idiv :
        Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
      val mk_mod :
        Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
      val mk_real : QQ.t -> Syntax.Context.term
      val mk_floor : Syntax.Context.term -> Syntax.Context.term
      val mk_neg : Syntax.Context.term -> Syntax.Context.term
      val mk_sub :
        Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
      val mk_forall :
        ?name:string ->
        Syntax.typ_fo -> Syntax.Context.formula -> Syntax.Context.formula
      val mk_exists :
        ?name:string ->
        Syntax.typ_fo -> Syntax.Context.formula -> Syntax.Context.formula
      val mk_forall_const :
        Syntax.symbol -> Syntax.Context.formula -> Syntax.Context.formula
      val mk_exists_const :
        Syntax.symbol -> Syntax.Context.formula -> Syntax.Context.formula
      val mk_and : Syntax.Context.formula list -> Syntax.Context.formula
      val mk_or : Syntax.Context.formula list -> Syntax.Context.formula
      val mk_not : Syntax.Context.formula -> Syntax.Context.formula
      val mk_eq :
        Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.formula
      val mk_lt :
        Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.formula
      val mk_leq :
        Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.formula
      val mk_true : Syntax.Context.formula
      val mk_false : Syntax.Context.formula
      val mk_ite :
        Syntax.Context.formula ->
        (Syntax.Context.t, 'a) Syntax.expr ->
        (Syntax.Context.t, 'a) Syntax.expr ->
        (Syntax.Context.t, 'a) Syntax.expr
    end
  module MakeContext : functor () -> Context
  module MakeSimplifyingContext : functor () -> Context
  module Infix :
    functor
      (C : sig type t val context : Syntax.Infix.t Syntax.context end) ->
      sig
        val exists :
          ?name:string ->
          Syntax.typ_fo -> C.t Syntax.formula -> C.t Syntax.formula
        val forall :
          ?name:string ->
          Syntax.typ_fo -> C.t Syntax.formula -> C.t Syntax.formula
        val ( ! ) : C.t Syntax.formula -> C.t Syntax.formula
        val ( && ) :
          C.t Syntax.formula -> C.t Syntax.formula -> C.t Syntax.formula
        val ( || ) :
          C.t Syntax.formula -> C.t Syntax.formula -> C.t Syntax.formula
        val ( < ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.formula
        val ( <= ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.formula
        val ( = ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.formula
        val tru : C.t Syntax.formula
        val fls : C.t Syntax.formula
        val ( + ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
        val ( - ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
        val ( * ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
        val ( / ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
        val ( mod ) : C.t Syntax.term -> C.t Syntax.term -> C.t Syntax.term
        val const : Syntax.symbol -> (C.t, 'typ) Syntax.expr
        val var : int -> Syntax.typ_fo -> (C.t, 'typ) Syntax.expr
      end
  module ContextTable :
    sig
      type 'a t
      val create : int -> 'a Syntax.ContextTable.t
      val add : 'a Syntax.ContextTable.t -> 'b Syntax.context -> 'a -> unit
      val replace :
        'a Syntax.ContextTable.t -> 'b Syntax.context -> 'a -> unit
      val find : 'a Syntax.ContextTable.t -> 'b Syntax.context -> 'a
      val mem : 'a Syntax.ContextTable.t -> 'b Syntax.context -> bool
      val clear : 'a Syntax.ContextTable.t -> unit
    end
end