From f0421879bb04751b1656856c170f558aec172e91 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 26 Feb 2026 16:22:55 +0000 Subject: [PATCH] Expose `mk_re_allchar` in OCaml API --- 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 96e4ab1b6..1e974c904 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1298,6 +1298,7 @@ struct 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_allchar = Z3native.mk_re_allchar 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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index f9c0de47c..430ec29f6 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -2023,6 +2023,9 @@ sig (** regular expression for the range between two characters *) val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr + (** the regular expression matching any single character of the given sort *) + val mk_re_allchar : context -> Sort.sort -> Expr.expr + (** bounded loop regular expression *) val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr