mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-27 21:48:56 +00:00
Code Activity

update ocaml binding to support more string apis (#6656)

Browse source
This commit is contained in:
권승완 2023-03-29 21:49:33 +09:00 • committed by GitHub
parent 130400d76e
commit 6670807103
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 52 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1253,7 +1253,9 @@ struct
let mk_re_sort = Z3native.mk_re_sort
let is_re_sort = Z3native.is_re_sort
let mk_string_sort = Z3native.mk_string_sort
let mk_char_sort = Z3native.mk_char_sort
let is_string_sort = Z3native.is_string_sort
let is_char_sort = Z3native.is_char_sort
let mk_string = Z3native.mk_string
let is_string = Z3native.is_string
let get_string = Z3native.get_string
@ -1274,6 +1276,10 @@ struct
let mk_str_le = Z3native.mk_str_le
let mk_str_lt = Z3native.mk_str_lt
let mk_int_to_str = Z3native.mk_int_to_str
let mk_string_to_code = Z3native.mk_string_to_code
let mk_string_from_code = Z3native.mk_string_from_code
let mk_ubv_to_str = Z3native.mk_ubv_to_str
let mk_sbv_to_str = Z3native.mk_sbv_to_str
let mk_seq_to_re = Z3native.mk_seq_to_re
let mk_seq_in_re = Z3native.mk_seq_in_re
let mk_re_plus = Z3native.mk_re_plus
@ -1287,6 +1293,12 @@ struct
let mk_re_complement = Z3native.mk_re_complement
let mk_re_empty = Z3native.mk_re_empty
let mk_re_full = Z3native.mk_re_full
let mk_char = Z3native.mk_char
let mk_char_le = Z3native.mk_char_le
let mk_char_to_int = Z3native.mk_char_to_int
let mk_char_to_bv = Z3native.mk_char_to_bv
let mk_char_from_bv = Z3native.mk_char_from_bv
let mk_char_is_digit = Z3native.mk_char_is_digit
end
module FloatingPoint =