sig
  type expr
  val ast_of_expr : Z3.Expr.expr -> Z3.AST.ast
  val expr_of_ast : Z3.AST.ast -> Z3.Expr.expr
  val simplify : Z3.Expr.expr -> Z3.Params.params option -> Z3.Expr.expr
  val get_simplify_help : Z3.context -> string
  val get_simplify_parameter_descrs :
    Z3.context -> Z3.Params.ParamDescrs.param_descrs
  val get_func_decl : Z3.Expr.expr -> Z3.FuncDecl.func_decl
  val get_num_args : Z3.Expr.expr -> int
  val get_args : Z3.Expr.expr -> Z3.Expr.expr list
  val update : Z3.Expr.expr -> Z3.Expr.expr list -> Z3.Expr.expr
  val substitute :
    Z3.Expr.expr -> Z3.Expr.expr list -> Z3.Expr.expr list -> Z3.Expr.expr
  val substitute_one :
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val substitute_vars : Z3.Expr.expr -> Z3.Expr.expr list -> Z3.Expr.expr
  val translate : Z3.Expr.expr -> Z3.context -> Z3.Expr.expr
  val to_string : Z3.Expr.expr -> string
  val is_numeral : Z3.Expr.expr -> bool
  val is_well_sorted : Z3.Expr.expr -> bool
  val get_sort : Z3.Expr.expr -> Z3.Sort.sort
  val is_const : Z3.Expr.expr -> bool
  val mk_const :
    Z3.context -> Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_const_s : Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_const_f : Z3.context -> Z3.FuncDecl.func_decl -> Z3.Expr.expr
  val mk_fresh_const : Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_app :
    Z3.context -> Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_numeral_string :
    Z3.context -> string -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_numeral_int : Z3.context -> int -> Z3.Sort.sort -> Z3.Expr.expr
  val equal : Z3.Expr.expr -> Z3.Expr.expr -> bool
  val compare : Z3.Expr.expr -> Z3.Expr.expr -> int
end