z3 4.12.6 · OCaml Package

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 mk_char_sort : context -> Sort.sort

val is_string_sort : context -> Sort.sort -> bool

val is_char_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_string_to_code : context -> Expr.expr -> Expr.expr

val mk_string_from_code : context -> Expr.expr -> Expr.expr

val mk_ubv_to_str : context -> Expr.expr -> Expr.expr

val mk_sbv_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

val mk_char : context -> int -> Expr.expr

val mk_char_le : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_char_to_int : context -> Expr.expr -> Expr.expr

val mk_char_to_bv : context -> Expr.expr -> Expr.expr

val mk_char_from_bv : context -> Expr.expr -> Expr.expr

val mk_char_is_digit : context -> Expr.expr -> Expr.expr

package z3