mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Expose Seq.mk_re_diff in ocaml bindings (#9584)

Browse source 
Noticed it was missing
This commit is contained in:
Filipe Marques 2026-05-21 18:29:08 +01:00 • committed by GitHub
parent ce6abd65db
commit c33a725bd8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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

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

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

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