sig
  val mk_seq_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
  val is_seq_sort : Z3.context -> Z3.Sort.sort -> bool
  val mk_re_sort : Z3.context -> Z3.Sort.sort -> Z3.Sort.sort
  val is_re_sort : Z3.context -> Z3.Sort.sort -> bool
  val mk_string_sort : Z3.context -> Z3.Sort.sort
  val mk_char_sort : Z3.context -> Z3.Sort.sort
  val is_string_sort : Z3.context -> Z3.Sort.sort -> bool
  val is_char_sort : Z3.context -> Z3.Sort.sort -> bool
  val mk_string : Z3.context -> string -> Z3.Expr.expr
  val is_string : Z3.context -> Z3.Expr.expr -> bool
  val get_string : Z3.context -> Z3.Expr.expr -> string
  val mk_seq_empty : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_seq_unit : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_concat : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_seq_prefix :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_suffix :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_contains :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_extract :
    Z3.context ->
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_replace :
    Z3.context ->
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_at : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_length : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_nth : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_index :
    Z3.context ->
    Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_last_index :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_str_to_int : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_str_le : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_str_lt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_int_to_str : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_string_to_code : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_string_from_code : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ubv_to_str : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sbv_to_str : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_to_re : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_seq_in_re :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_re_plus : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_re_star : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_re_option : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_re_union : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_re_concat : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_re_range :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_re_loop : Z3.context -> Z3.Expr.expr -> int -> int -> Z3.Expr.expr
  val mk_re_intersect : Z3.context -> Z3.Expr.expr list -> Z3.Expr.expr
  val mk_re_complement : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_re_empty : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_re_full : Z3.context -> Z3.Sort.sort -> Z3.Expr.expr
  val mk_char : Z3.context -> int -> Z3.Expr.expr
  val mk_char_le : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_char_to_int : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_char_to_bv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_char_from_bv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_char_is_digit : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
end