mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix #4801

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-12 20:20:00 -08:00
parent 83f4a006c6
commit 04a1d4245c
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1260,6 +1260,8 @@ struct
let mk_seq_length = Z3native.mk_seq_length
let mk_seq_index = Z3native.mk_seq_index
let mk_str_to_int = Z3native.mk_str_to_int
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_seq_to_re = Z3native.mk_seq_to_re
let mk_seq_in_re = Z3native.mk_seq_in_re

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

@ -1913,6 +1913,12 @@ sig
(* retrieve integer expression encoded in string *)
val mk_str_to_int : context -> Expr.expr -> Expr.expr
(* compare strings less-than-or-equal *)
val mk_str_le : context -> Expr.expr -> Expr.expr -> Expr.expr
(* compare strings less-than *)
val mk_str_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
(* convert an integer expression to a string *)
val mk_int_to_str : context -> Expr.expr -> Expr.expr