diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 55adc362c..523c96fc6 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1297,6 +1297,9 @@ struct 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_replace_all = Z3native.mk_seq_replace_all + let mk_seq_replace_re = Z3native.mk_seq_replace_re + let mk_seq_replace_re_all = Z3native.mk_seq_replace_re_all let mk_seq_at = Z3native.mk_seq_at let mk_seq_length = Z3native.mk_seq_length let mk_seq_nth = Z3native.mk_seq_nth diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 572659030..2272eec8c 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1987,9 +1987,22 @@ sig (** 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 *) + (** [mk_seq_replace ctx seq target replacement] replaces the first occurrence + of [target] within [seq] with [replacement]. *) val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + (** [mk_seq_replace_all ctx seq target replacement] replaces all occurrences + of [target] within [seq] with [replacement]. *) + val mk_seq_replace_all : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (** [mk_seq_replace_re ctx seq re replacement] replaces the first occurrence + matching the regular expression [re] within [seq] with [replacement]. *) + val mk_seq_replace_re : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr + + (** [mk_seq_replace_re_all ctx seq re replacement] replaces all occurrences + matching the regular expression [re] within [seq] with [replacement]. *) + val mk_seq_replace_re_all : 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