From 3a0e9e8f53de9058f1813b8c461a3cc1fcc3c06d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Feb 2017 11:31:13 -0500 Subject: [PATCH] add itos/stoi conversion to API. Issue #895 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 47 +++++++++++++++++++++------------------ src/api/api_seq.cpp | 4 ++++ src/api/c++/z3++.h | 11 +++++++++ src/api/dotnet/Context.cs | 23 +++++++++++++++++++ src/api/python/z3/z3.py | 28 +++++++++++++++++++++-- src/api/z3_api.h | 19 ++++++++++++++++ 6 files changed, 108 insertions(+), 24 deletions(-) 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.