add itos/stoi conversion to API. Issue #895

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_ast.cpp

@@ -1110,29 +1110,32 @@ extern "C" {
 
         if (mk_c(c)->get_seq_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
-            case Z3_OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
+            case OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
-            case Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
+            case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
-            case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
+            case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
-            case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
+            case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
-            case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
+            case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
-            case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
+            case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
-            case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
+            case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
-            case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
+            case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
-            case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT;
+            case OP_SEQ_AT: return Z3_OP_SEQ_AT;
-            case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
+            case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
-            case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
+            case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
-            case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
+            case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
-            case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
+            case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
 
-            case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS;
+            case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
-            case Z3_OP_RE_STAR: return Z3_OP_RE_STAR;
+            case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
-            case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION;
+
-            case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
+            case OP_RE_PLUS: return Z3_OP_RE_PLUS;
-            case Z3_OP_RE_UNION: return Z3_OP_RE_UNION;
+            case OP_RE_STAR: return Z3_OP_RE_STAR;
-            case Z3_OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
+            case OP_RE_OPTION: return Z3_OP_RE_OPTION;
-            case Z3_OP_RE_LOOP: return Z3_OP_RE_LOOP;
+            case OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
-            case Z3_OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET;
+            case OP_RE_UNION: return Z3_OP_RE_UNION;
-            case Z3_OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
+            case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
+            case OP_RE_LOOP: return Z3_OP_RE_LOOP;
+            case OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET;
+            case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
             default:
                 return Z3_OP_INTERNAL;
             }

src/api/api_seq.cpp

@@ -141,6 +141,10 @@ extern "C" {
     MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);
     MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP);
 
+    MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP);
+    MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP);
+
+
     Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {
         Z3_TRY;
         LOG_Z3_mk_re_loop(c, r, lo, hi);

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

@@ -964,6 +964,17 @@ namespace z3 {
             check_error();
             return expr(ctx(), r);
         }
+        expr stoi() const {
+            Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr itos() const {
+            Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+
         friend expr range(expr const& lo, expr const& hi);       
         /**
            \brief create a looping regular expression.

src/api/dotnet/Context.cs

@@ -2420,6 +2420,29 @@ namespace Microsoft.Z3
             return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
         }
 
+        /// <summary>
+        /// Convert an integer expression to a string.
+        /// </summary>
+        public SeqExpr IntToString(Expr e) 
+        {
+            Contract.Requires(e != null);
+	    Contract.Requires(e is ArithExpr);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
+        }
+
+        /// <summary>
+        /// Convert an integer expression to a string.
+        /// </summary>
+        public IntExpr StringToInt(Expr e) 
+        {
+            Contract.Requires(e != null);
+            Contract.Requires(e is SeqExpr);
+            Contract.Ensures(Contract.Result<IntExpr>() != null);
+            return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
+        }
+
+
         /// <summary>
         /// Concatentate sequences.
         /// </summary>

src/api/python/z3/z3.py

@@ -1011,6 +1011,7 @@ def _coerce_exprs(a, b, ctx=None):
     b = s.cast(b)
     return (a, b)
 
+
 def _reduce(f, l, a):
     r = a
     for e in l:
@@ -1296,7 +1297,7 @@ class BoolSortRef(SortRef):
         if isinstance(val, bool):
             return BoolVal(val, self.ctx)
         if __debug__:
-            _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected")
+            _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
             _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
         return val
 
@@ -2012,7 +2013,7 @@ class ArithSortRef(SortRef):
             if self.is_real():
                 return RealVal(val, self.ctx)
             if __debug__:
-                _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
+                _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self)
 
 def is_arith_sort(s):
     """Return `True` if s is an arithmetical sort (type).
@@ -9660,6 +9661,29 @@ def Length(s):
     s = _coerce_seq(s)
     return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
 
+def StrToInt(s):
+    """Convert string expression to integer
+    >>> a = StrToInt("1")
+    >>> simplify(1 == a)
+    True
+    >>> b = StrToInt("2")
+    >>> simplify(1 == b)
+    False
+    >>> c = StrToInt(IntToStr(2))
+    >>> simplify(1 == c)
+    False
+    """
+    s = _coerce_seq(s)
+    return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx)
+
+
+def IntToStr(s):
+    """Convert integer expression to string"""
+    if not is_expr(s):
+        s = _py2expr(s)
+    return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
+
+
 def Re(s, ctx=None):
     """The regular expression that accepts sequence 's'
     >>> s1 = Re("ab")

src/api/z3_api.h

@@ -1152,6 +1152,10 @@ typedef enum {
     Z3_OP_SEQ_TO_RE,
     Z3_OP_SEQ_IN_RE,
 
+    // strings
+    Z3_OP_STR_TO_INT,
+    Z3_OP_INT_TO_STR,
+
     // regular expressions
     Z3_OP_RE_PLUS,
     Z3_OP_RE_STAR,
@@ -3325,6 +3329,21 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
 
+    /**
+       \brief Convert string to integer.
+
+       def_API('Z3_mk_str_to_int' ,AST ,(_in(CONTEXT), _in(AST)))
+     */    
+    Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
+
+
+    /**
+       \brief Integer to string conversion.
+
+       def_API('Z3_mk_int_to_str' ,AST ,(_in(CONTEXT), _in(AST)))
+     */    
+    Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
+
     /**
        \brief Create a regular expression that accepts the sequence \c seq.