From c33a725bd86cebfa104175725660a2d0c4730e03 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 21 May 2026 18:29:08 +0100 Subject: [PATCH] Expose `Seq.mk_re_diff` in ocaml bindings (#9584) Noticed it was missing --- src/api/ml/z3.ml | 1 + src/api/ml/z3.mli | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 523c96fc6..f64c4ddd8 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1325,6 +1325,7 @@ struct let mk_re_loop = Z3native.mk_re_loop let mk_re_intersect ctx args = Z3native.mk_re_intersect ctx (List.length args) args let mk_re_complement = Z3native.mk_re_complement + let mk_re_diff = Z3native.mk_re_diff let mk_re_empty = Z3native.mk_re_empty let mk_re_full = Z3native.mk_re_full let mk_char = Z3native.mk_char diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 2272eec8c..f5e90d845 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2080,6 +2080,9 @@ sig (** the regular expression complement *) val mk_re_complement : context -> Expr.expr -> Expr.expr + (** the regular expression difference *) + val mk_re_diff : context -> Expr.expr -> Expr.expr -> Expr.expr + (** the regular expression that accepts no sequences *) val mk_re_empty : context -> Sort.sort -> Expr.expr