package z3

  1. Overview
  2. Docs
val mk_seq_sort : context -> Sort.sort -> Sort.sort
val is_seq_sort : context -> Sort.sort -> bool
val mk_re_sort : context -> Sort.sort -> Sort.sort
val is_re_sort : context -> Sort.sort -> bool
val mk_string_sort : context -> Sort.sort
val is_string_sort : context -> Sort.sort -> bool
val mk_string : context -> string -> Expr.expr
val is_string : context -> Expr.expr -> bool
val get_string : context -> Expr.expr -> string
val mk_seq_empty : context -> Sort.sort -> Expr.expr
val mk_seq_unit : context -> Expr.expr -> Expr.expr
val mk_seq_concat : context -> Expr.expr list -> Expr.expr
val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_length : context -> Expr.expr -> Expr.expr
val mk_seq_nth : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr
val mk_seq_last_index : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_str_to_int : context -> Expr.expr -> Expr.expr
val mk_str_le : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_str_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_int_to_str : context -> Expr.expr -> Expr.expr
val mk_seq_to_re : context -> Expr.expr -> Expr.expr
val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_re_plus : context -> Expr.expr -> Expr.expr
val mk_re_star : context -> Expr.expr -> Expr.expr
val mk_re_option : context -> Expr.expr -> Expr.expr
val mk_re_union : context -> Expr.expr list -> Expr.expr
val mk_re_concat : context -> Expr.expr list -> Expr.expr
val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr
val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr
val mk_re_intersect : context -> Expr.expr list -> Expr.expr
val mk_re_complement : context -> Expr.expr -> Expr.expr
val mk_re_empty : context -> Sort.sort -> Expr.expr
val mk_re_full : context -> Sort.sort -> Expr.expr