sig
  val mk_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort -> Z3.Sort.sort
  val is_store : Z3.Expr.expr -> bool
  val is_select : Z3.Expr.expr -> bool
  val is_constant_array : Z3.Expr.expr -> bool
  val is_default_array : Z3.Expr.expr -> bool
  val is_array_map : Z3.Expr.expr -> bool
  val is_as_array : Z3.Expr.expr -> bool
  val is_array : Z3.Expr.expr -> bool
  val get_domain : Z3.Sort.sort -> Z3.Sort.sort
  val get_range : Z3.Sort.sort -> Z3.Sort.sort
  val mk_const :
    Z3.context ->
    Z3.Symbol.symbol -> Z3.Sort.sort -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_const_s :
    Z3.context -> string -> Z3.Sort.sort -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_select : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_store :
    Z3.context ->
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_const_array :
    Z3.context -> Z3.Sort.sort -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_map :
    Z3.context -> Z3.FuncDecl.func_decl -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_term_array : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_array_ext :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
end