mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-01 11:16:54 +00:00
Code Activity

Expose mk_re_allchar in OCaml API

Browse source
This commit is contained in:
Filipe Marques 2026-02-26 16:22:55 +00:00
parent 070f760501
commit f0421879bb
No known key found for this signature in database
GPG key ID: 74A869792DE9DF80
2 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/ml/z3.ml
View file

@ -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

3
src/api/ml/z3.mli
View file

@ -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