Module Z3.Seq

module Seq: sig .. end

Sequences, Strings and Regular Expressions *

val mk_seq_sort : context -> Sort.sort -> Sort.sort

create a sequence sort

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

test if sort is a sequence sort

val mk_re_sort : context -> Sort.sort -> Sort.sort

create regular expression sorts over sequences of the argument sort

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

test if sort is a regular expression sort

val mk_string_sort : context -> Sort.sort

create string sort

val mk_char_sort : context -> Sort.sort

create char sort

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

test if sort is a string sort (a sequence of 8-bit bit-vectors)

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

test if sort is a char sort

val mk_string : context -> string -> Expr.expr

create a string literal

val is_string : context -> Expr.expr -> bool

test if expression is a string

val get_string : context -> Expr.expr -> string

retrieve string from string Expr.expr

val mk_seq_empty : context -> Sort.sort -> Expr.expr

the empty sequence over base sort

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

a unit sequence

val mk_seq_concat : context -> Expr.expr list -> Expr.expr

sequence concatenation

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

predicate if the first argument is a prefix of the second

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

predicate if the first argument is a suffix of the second

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

predicate if the first argument contains the second

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

extract sub-sequence starting at index given by second argument and of length provided by third argument

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

replace first occurrence of second argument by third

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

a unit sequence at index provided by second argument

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

length of a sequence

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

mk_seq_nth ctx s index retrieves from s the element at position index. The function is under-specified if the index is out of bounds.

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

index of the first occurrence of the second argument in the first

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

mk_seq_last_index ctx s substr occurence of substr in the sequence s

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

retrieve integer expression encoded in string

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

compare strings less-than-or-equal

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

compare strings less-than

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

convert an integer expression to a string

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

mk_string_to_code ctx s convert a unit length string s to integer code

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

mk_string_from_code ctx c convert code c to a string

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

mk_ubv_to_str ctx ubv convert a unsigned bitvector ubv to a string

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

mk_sbv_to_str ctx sbv convert a signed bitvector sbv to a string

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

create regular expression that accepts the argument sequence

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

regular expression membership predicate

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

regular expression plus

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

regular expression star

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

optional regular expression

val mk_re_union : context -> Expr.expr list -> Expr.expr

union of regular expressions

val mk_re_concat : context -> Expr.expr list -> Expr.expr

concatenation of regular expressions

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

regular expression for the range between two characters

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

bounded loop regular expression

val mk_re_intersect : context -> Expr.expr list -> Expr.expr

intersection of regular expressions

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

the regular expression complement

val mk_re_empty : context -> Sort.sort -> Expr.expr

the regular expression that accepts no sequences

val mk_re_full : context -> Sort.sort -> Expr.expr

the regular expression that accepts all sequences

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

mk_char ctx i converts an integer to a character

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

mk_char_le ctx lc rc compares two characters

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

mk_char_to_int ctx c converts the character c to an integer

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

mk_char_to_bv ctx c converts the character c to a bitvector

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

mk_char_from_bv ctx bv converts the bitvector bv to a character

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

mk_char_is_digit ctx c checks if the character c is a digit