From ce6abd65db724aae3da8e489fbf80606e22de0e4 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 21 May 2026 18:28:48 +0100 Subject: [PATCH] Expose other `mk_seq_replace` variants in OCaml bindings (#9586) Also update the documentation for the base `mk_seq_replace` function to match the new inline documentation style. --- src/api/ml/z3.ml | 3 +++ src/api/ml/z3.mli | 15 ++++++++++++++- 2 files changed, 17 insertions(+), 1 deletion(-) 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