diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index d3a2d0e74..61a027cec 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 4dd280d77..bbfed07d2 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -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