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