diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index fd2776079..c9cdc6ab3 100644
--- a/src/api/api_ast.cpp
+++ b/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 Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
- case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
- case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
- case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
- case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
- case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
- case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
- case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT;
- case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
- case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
- case Z3_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_UNIT: return Z3_OP_SEQ_UNIT;
+ case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
+ case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
+ case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
+ case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
+ case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
+ case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
+ case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
+ case OP_SEQ_AT: return Z3_OP_SEQ_AT;
+ case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
+ case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
+ case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
+ case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
- case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS;
- case Z3_OP_RE_STAR: return Z3_OP_RE_STAR;
- case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION;
- case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
- case Z3_OP_RE_UNION: return Z3_OP_RE_UNION;
- case Z3_OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
- case Z3_OP_RE_LOOP: return Z3_OP_RE_LOOP;
- case Z3_OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET;
- case Z3_OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
+ case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
+ case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
+
+ case OP_RE_PLUS: return Z3_OP_RE_PLUS;
+ case OP_RE_STAR: return Z3_OP_RE_STAR;
+ case OP_RE_OPTION: return Z3_OP_RE_OPTION;
+ case OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
+ case OP_RE_UNION: return Z3_OP_RE_UNION;
+ 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;
}
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index 478ee6274..986e6f497 100644
--- a/src/api/api_seq.cpp
+++ b/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);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 979d9aed7..e5d0acaab 100644
--- a/src/api/c++/z3++.h
+++ b/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.
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index f5c4dc99d..a656be3eb 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2420,6 +2420,29 @@ namespace Microsoft.Z3
return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
}
+ ///
+ /// Convert an integer expression to a string.
+ ///
+ public SeqExpr IntToString(Expr e)
+ {
+ Contract.Requires(e != null);
+ Contract.Requires(e is ArithExpr);
+ Contract.Ensures(Contract.Result() != null);
+ return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
+ }
+
+ ///
+ /// Convert an integer expression to a string.
+ ///
+ public IntExpr StringToInt(Expr e)
+ {
+ Contract.Requires(e != null);
+ Contract.Requires(e is SeqExpr);
+ Contract.Ensures(Contract.Result() != null);
+ return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
+ }
+
+
///
/// Concatentate sequences.
///
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 77b74336e..f1fde1720 100644
--- a/src/api/python/z3/z3.py
+++ b/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")
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 65c155d63..ee35c002e 100644
--- a/src/api/z3_api.h
+++ b/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.