Added character functions to API (#5549)

* Added character functions to API

* Changed names of c++ functions

src/api/api_ast.cpp

@@ -1230,6 +1230,18 @@ extern "C" {
             }
         }
 
+        if (mk_c(c)->get_char_fid() == _d->get_family_id()) {
+            switch (_d->get_decl_kind()) {
+            case OP_CHAR_LE: return Z3_OP_CHAR_LE;
+            case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT;
+            case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV;
+            case OP_CHAR_FROM_BV: return Z3_OP_CHAR_FROM_BV;
+            case OP_CHAR_IS_DIGIT: return Z3_OP_CHAR_IS_DIGIT;
+            default: 
+                return Z3_OP_INTERNAL;
+            }
+        }
+
         if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
             case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;

src/api/api_seq.cpp

@@ -275,6 +275,11 @@ extern "C" {
     MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty);
     MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq);
 
+    MK_BINARY(Z3_mk_char_le, mk_c(c)->get_char_fid(), OP_CHAR_LE, SKIP);
+    MK_UNARY(Z3_mk_char_to_int, mk_c(c)->get_char_fid(), OP_CHAR_TO_INT, SKIP);
+    MK_UNARY(Z3_mk_char_to_bv, mk_c(c)->get_char_fid(), OP_CHAR_TO_BV, SKIP);
+    MK_UNARY(Z3_mk_char_from_bv, mk_c(c)->get_char_fid(), OP_CHAR_FROM_BV, SKIP);
+    MK_UNARY(Z3_mk_char_is_digit, mk_c(c)->get_char_fid(), OP_CHAR_IS_DIGIT, SKIP);
 
 
 };

src/api/c++/z3++.h

@@ -1445,6 +1445,26 @@ namespace z3 {
             check_error();
             return expr(ctx(), r);
         }
+        expr char_to_int() const {
+            Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr char_to_bv() const {
+            Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr char_from_bv() const {
+            Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr is_digit() const {
+            Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
  
         friend expr range(expr const& lo, expr const& hi);
         /**

src/api/dotnet/Context.cs

@@ -2694,6 +2694,52 @@ namespace Microsoft.Z3
             return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject));
         }
 
+        /// <summary>
+        /// Create less than or equal to between two characters.
+        /// </summary>
+        public BoolExpr MkCharLe(Expr ch1, Expr ch2) 
+        {
+            Debug.Assert(ch1 != null);
+            Debug.Assert(ch2 != null);
+            return new BoolExpr(this, Native.Z3_mk_char_le(nCtx, ch1.NativeObject, ch2.NativeObject));
+        }
+
+        /// <summary>
+        /// Create an integer (code point) from character.
+        /// </summary>
+        public IntExpr CharToInt(Expr ch) 
+        {
+            Debug.Assert(ch != null);
+            return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a bit-vector (code point) from character.
+        /// </summary>
+        public BitVecExpr CharToBV(Expr ch) 
+        {
+            Debug.Assert(ch != null);
+            return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a character from a bit-vector (code point).
+        /// </summary>
+        public Expr CharFromBV(BitVecExpr bv) 
+        {
+            Debug.Assert(bv != null);
+            return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a check if the character is a digit.
+        /// </summary>
+        public BoolExpr MkIsDigit(Expr ch) 
+        {
+            Debug.Assert(ch != null);
+            return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject));
+        }
+
         #endregion
 
         #region Pseudo-Boolean constraints

src/api/java/Context.java

@@ -2111,7 +2111,7 @@ public class Context implements AutoCloseable {
     /**
      *  Retrieve element at index.
      */
-    public <R extends Sort> Expr<R> MkNth(Expr<SeqSort<R>> s, Expr<IntSort> index)
+    public <R extends Sort> Expr<R> mkNth(Expr<SeqSort<R>> s, Expr<IntSort> index)
     {
         checkContextMatch(s, index);
         return (Expr<R>) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
@@ -2272,6 +2272,50 @@ public class Context implements AutoCloseable {
         return (ReExpr<R>) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));
     }
 
+    /**
+     * Create less than or equal to between two characters.
+     */
+    public BoolExpr mkCharLe(Expr<CharSort> ch1, Expr<CharSort> ch2) 
+    {
+        checkContextMatch(ch1, ch2);
+        return (BoolExpr) Expr.create(this, Native.mkCharLe(nCtx(), ch1.getNativeObject(), ch2.getNativeObject()));
+    }
+
+    /**
+     * Create an integer (code point) from character.
+     */
+    public IntExpr charToInt(Expr<CharSort> ch) 
+    {
+        checkContextMatch(ch);
+        return (IntExpr) Expr.create(this, Native.mkCharToInt(nCtx(), ch.getNativeObject()));
+    }
+
+    /**
+     * Create a bit-vector (code point) from character.
+     */
+    public BitVecExpr charToBv(Expr<CharSort> ch) 
+    {
+        checkContextMatch(ch);
+        return (BitVecExpr) Expr.create(this, Native.mkCharToBv(nCtx(), ch.getNativeObject()));
+    }
+
+    /**
+     * Create a character from a bit-vector (code point).
+     */
+    public Expr<CharSort> charFromBv(BitVecExpr bv) 
+    {
+        checkContextMatch(bv);
+        return (Expr<CharSort>) Expr.create(this, Native.mkCharFromBv(nCtx(), bv.getNativeObject()));
+    }
+
+    /**
+     * Create a check if the character is a digit.
+     */
+    public BoolExpr mkIsDigit(Expr<CharSort> ch) 
+    {
+        checkContextMatch(ch);
+        return (BoolExpr) Expr.create(this, Native.mkCharIsDigit(nCtx(), ch.getNativeObject()));
+    }
 
     /**
      * Create an at-most-k constraint.

src/api/z3_api.h

@@ -1221,6 +1221,13 @@ typedef enum {
     Z3_OP_RE_FULL_SET,
     Z3_OP_RE_COMPLEMENT,
 
+    // char
+    Z3_OP_CHAR_LE,
+    Z3_OP_CHAR_TO_INT,
+    Z3_OP_CHAR_TO_BV,
+    Z3_OP_CHAR_FROM_BV,
+    Z3_OP_CHAR_IS_DIGIT,
+
     // Auxiliary
     Z3_OP_LABEL = 0x700,
     Z3_OP_LABEL_LIT,
@@ -1533,6 +1540,7 @@ extern "C" {
             - model                      model generation for solvers, this parameter can be overwritten when creating a solver
             - model_validate             validate models produced by solvers
             - unsat_core                 unsat-core generation for solvers, this parameter can be overwritten when creating a solver
+            - encoding                   the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit)
 
         \sa Z3_set_param_value
         \sa Z3_del_config
@@ -3778,6 +3786,41 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
 
+    /**
+         \brief Create less than or equal to between two characters.
+
+         def_API('Z3_mk_char_le', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_char_le(Z3_context c, Z3_ast ch1, Z3_ast ch2);
+
+    /**
+         \brief Create an integer (code point) from character.
+
+         def_API('Z3_mk_char_to_int', AST, (_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch);
+
+    /**
+         \brief Create a bit-vector (code point) from character.
+
+         def_API('Z3_mk_char_to_bv', AST, (_in(CONTEXT), _in(AST)))
+     */
+    Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch);
+
+    /**
+         \brief Create a character from a bit-vector (code point).
+
+         def_API('Z3_mk_char_from_bv', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv);
+
+    /**
+         \brief Create a check if the character is a digit.
+
+         def_API('Z3_mk_char_is_digit', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch);
+
     /*@}*/
 
 

src/ast/char_decl_plugin.cpp

@@ -90,7 +90,7 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         else if (!b.is_bv_sort(domain[0]) || b.get_bv_size(domain[0]) != num_bits())
             msg << "expected bit-vector sort argument with " << num_bits();
         else {
-            m.mk_func_decl(symbol("char.to_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr));
+            return m.mk_func_decl(symbol("char.from_bv"), arity, domain, m_char, func_decl_info(m_family_id, k, 0, nullptr));
         }
         m.raise_exception(msg.str());
     }