From 667080710366eab733cbf9ce404a7e7b9cb455b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=EA=B6=8C=EC=8A=B9=EC=99=84?=
 <36997987+Hhro@users.noreply.github.com>
Date: Wed, 29 Mar 2023 21:49:33 +0900
Subject: [PATCH] update ocaml binding to support more string apis (#6656)

---
 .gitignore        |  3 +++
 src/api/ml/z3.ml  | 12 ++++++++++++
 src/api/ml/z3.mli | 37 +++++++++++++++++++++++++++++++++++++
 3 files changed, 52 insertions(+)

diff --git a/.gitignore b/.gitignore
index b0c19a43260..710ce4b7ee4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,9 +9,12 @@ callgrind.out.*
 .z3-trace
 # OCaml generated files
 *.a
+*.o
 *.cma
 *.cmo
 *.cmi
+*.cmx
+*.byte
 *.cmxa
 ocamlz3
 # Java generated files
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 4c8b0322a95..98807bedd6f 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -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 =
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 27b0992ca62..53e92b491e4 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -1881,9 +1881,15 @@ sig
   (** create string sort *)
   val mk_string_sort : context -> Sort.sort
 
+  (** create char sort *)
+  val mk_char_sort : context -> Sort.sort
+
   (** test if sort is a string sort (a sequence of 8-bit bit-vectors) *)
   val is_string_sort : context -> Sort.sort -> bool 
 
+  (** test if sort is a char sort *)
+  val is_char_sort : context -> Sort.sort -> bool
+
   (** create a string literal *)
   val mk_string : context -> string -> Expr.expr
 
@@ -1936,6 +1942,7 @@ 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
 
@@ -1945,6 +1952,18 @@ sig
   (** convert an integer expression to a string *)
   val mk_int_to_str : context -> Expr.expr -> Expr.expr 
 
+  (** [mk_string_to_code ctx s] convert a unit length string [s] to integer code *)
+  val mk_string_to_code : context -> Expr.expr -> Expr.expr
+
+  (** [mk_string_from_code ctx c] convert code [c] to a string *)
+  val mk_string_from_code : context -> Expr.expr -> Expr.expr
+
+  (** [mk_ubv_to_str ctx ubv] convert a unsigned bitvector [ubv] to a string  *)
+  val mk_ubv_to_str : context -> Expr.expr -> Expr.expr
+
+  (** [mk_sbv_to_str ctx sbv] convert a signed bitvector [sbv] to a string  *)
+  val mk_sbv_to_str : context -> Expr.expr -> Expr.expr
+
   (** create regular expression that accepts the argument sequence *)
   val mk_seq_to_re : context -> Expr.expr -> Expr.expr 
 
@@ -1984,6 +2003,24 @@ sig
   (** the regular expression that accepts all sequences *)
   val mk_re_full : context -> Sort.sort -> Expr.expr 
 
+  (** [mk_char ctx i] converts an integer to a character *)
+  val mk_char : context -> int -> Expr.expr
+
+  (** [mk_char_le ctx lc rc] compares two characters *)
+  val mk_char_le : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** [mk_char_to_int ctx c] converts the character [c] to an integer *)
+  val mk_char_to_int : context -> Expr.expr -> Expr.expr
+
+  (** [mk_char_to_bv ctx c] converts the character [c] to a bitvector *)
+  val mk_char_to_bv : context -> Expr.expr -> Expr.expr
+
+  (** [mk_char_from_bv ctx bv] converts the bitvector [bv] to a character *)
+  val mk_char_from_bv : context -> Expr.expr -> Expr.expr
+
+  (** [mk_char_is_digit ctx c] checks if the character [c] is a digit *)
+  val mk_char_is_digit: context -> Expr.expr -> Expr.expr
+
 end
 
 (** Floating-Point Arithmetic *)