sig
  val mk_sort : Z3.context -> Z3.Sort.sort
  val mk_const : Z3.context -> Z3.Symbol.symbol -> Z3.Expr.expr
  val mk_const_s : Z3.context -> string -> Z3.Expr.expr
  val mk : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_real_part : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_imag_part : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
end