diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 41d2226c5..c4a4da00c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1215,6 +1215,44 @@ struct let mk_numeral ctx v size = Z3native.mk_numeral ctx v (mk_sort ctx size) end +module Seq = +struct + let mk_seq_sort = Z3native.mk_seq_sort + let is_seq_sort = Z3native.is_seq_sort + let mk_re_sort = Z3native.mk_re_sort + let is_re_sort = Z3native.is_re_sort + let mk_string_sort = Z3native.mk_string_sort + let is_string_sort = Z3native.is_string_sort + let mk_string = Z3native.mk_string + let is_string = Z3native.is_string + let get_string = Z3native.get_string + let mk_seq_empty = Z3native.mk_seq_empty + let mk_seq_unit = Z3native.mk_seq_unit + let mk_seq_concat ctx args = Z3native.mk_seq_concat ctx (List.length args) args + let mk_seq_prefix = Z3native.mk_seq_prefix + let mk_seq_suffix = Z3native.mk_seq_suffix + let mk_seq_contains = Z3native.mk_seq_contains + let mk_seq_extract = Z3native.mk_seq_extract + let mk_seq_replace = Z3native.mk_seq_replace + let mk_seq_at = Z3native.mk_seq_at + let mk_seq_length = Z3native.mk_seq_length + let mk_seq_index = Z3native.mk_seq_index + let mk_str_to_int = Z3native.mk_str_to_int + let mk_int_to_str = Z3native.mk_int_to_str + let mk_seq_to_re = Z3native.mk_seq_to_re + let mk_seq_in_re = Z3native.mk_seq_in_re + let mk_re_plus = Z3native.mk_re_plus + let mk_re_star = Z3native.mk_re_star + let mk_re_option = Z3native.mk_re_option + let mk_re_union ctx args = Z3native.mk_re_union ctx (List.length args) args + let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args + let mk_re_range = Z3native.mk_re_range + let mk_re_loop = Z3native.mk_re_loop + let mk_re_intersect = Z3native.mk_re_intersect + let mk_re_complement = Z3native.mk_re_complement + let mk_re_empty = Z3native.mk_re_empty + let mk_re_full = Z3native.mk_re_full +end module FloatingPoint = struct diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 818a635f7..7b561f878 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1825,6 +1825,115 @@ sig val mk_numeral : context -> string -> int -> Expr.expr end +(** Sequences, Strings and Regular Expressions **) +module Seq : +sig + val mk_seq_sort : context -> Sort.sort -> Sort.sort + + (* test if sort is a sequence sort *) + val is_seq_sort : context -> Sort.sort -> bool + + (* create regular expression sorts over sequences of the argument sort *) + val mk_re_sort : context -> Sort.sort -> Sort.sort + + (* test if sort is a regular expression sort *) + val is_re_sort : context -> Sort.sort -> bool + + (* create string sort *) + val mk_string_sort : context -> Sort.sort + + (* test if sort is a string sort (a sequence of 8-bit bit-vectors) *) + val is_string_sort : context -> Sort.sort -> bool + + (* create a string literal *) + val mk_string : context -> string -> Expr.expr + + (* test if expression is a string *) + val is_string : context -> Expr.expr -> bool + + (* retrieve string from string Expr.expr *) + val get_string : context -> Expr.expr -> string + + (* the empty sequence over base sort *) + val mk_seq_empty : context -> Sort.sort -> Expr.expr + + (* a unit sequence *) + val mk_seq_unit : context -> Expr.expr -> Expr.expr + + (* sequence concatenation *) + val mk_seq_concat : context -> Expr.expr list -> Expr.expr + + (* predicate if the first argument is a prefix of the second *) + val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* predicate if the first argument is a suffix of the second *) + val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* predicate if the first argument contains the second *) + val mk_seq_contains : context -> 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_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* replace first occurrence of second argument by third *) + val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* a unit sequence at index provided by second argument *) + val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* length of a sequence *) + val mk_seq_length : context -> Expr.expr -> Expr.expr + + (* index of the first occurrence of the second argument in the first *) + val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (* retrieve integer expression encoded in string *) + val mk_str_to_int : context -> Expr.expr -> Expr.expr + + (* convert an integer expression to a string *) + val mk_int_to_str : context -> Expr.expr -> Expr.expr + + (* create regular expression that accepts the argument sequence *) + val mk_seq_to_re : context -> Expr.expr -> Expr.expr + + (* regular expression membership predicate *) + val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* regular expression plus *) + val mk_re_plus : context -> Expr.expr -> Expr.expr + + (* regular expression star *) + val mk_re_star : context -> Expr.expr -> Expr.expr + + (* optional regular expression *) + val mk_re_option : context -> Expr.expr -> Expr.expr + + (* union of regular expressions *) + val mk_re_union : context -> Expr.expr list -> Expr.expr + + (* concatenation of regular expressions* ) + val mk_re_concat : context -> Expr.expr list -> Expr.expr + + (* regular expression for the range between two characters *) + val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr + + (* bounded loop regular expression *) + val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr + + (* intersection of regular expressions *) + val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr + + (* the regular expression complement *) + val mk_re_complement : context -> Expr.expr -> Expr.expr + + (* the regular expression that accepts no sequences *) + val mk_re_empty : context -> Sort.sort -> Expr.expr + + (* the regular expression that accepts all sequences *) + val mk_re_full : context -> Sort.sort -> Expr.expr + +end + (** Floating-Point Arithmetic *) module FloatingPoint : sig