From 0fa4b63d2699c791e2882c9586186dd53266d871 Mon Sep 17 00:00:00 2001 From: CEisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Fri, 16 Jul 2021 17:58:28 +0200 Subject: [PATCH] Added sbv2s (#5413) * Added sbv2s * Fixed indention Co-authored-by: Clemens Eisenhofer --- src/api/api_ast.cpp | 3 ++- src/api/api_seq.cpp | 1 + src/api/c++/z3++.h | 5 ++++ src/api/dotnet/Context.cs | 41 +++++++++++++++++++------------ src/api/java/Context.java | 10 +++++++- src/api/z3_api.h | 7 ++++++ src/ast/bv_decl_plugin.h | 1 + src/ast/rewriter/seq_rewriter.cpp | 28 +++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 22 ++++++++++++++--- src/ast/seq_decl_plugin.h | 7 +++++- 11 files changed, 104 insertions(+), 22 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 648e3cd97..50a02d262 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1202,7 +1202,8 @@ extern "C" { case OP_STRING_STOI: return Z3_OP_STR_TO_INT; case OP_STRING_ITOS: return Z3_OP_INT_TO_STR; - case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR; + case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR; + case OP_STRING_SBVTOS: return Z3_OP_SBV_TO_STR; case OP_STRING_LT: return Z3_OP_STRING_LT; case OP_STRING_LE: return Z3_OP_STRING_LE; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index fc336da74..9ce3ded09 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -245,6 +245,7 @@ extern "C" { 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); MK_UNARY(Z3_mk_ubv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_UBVTOS, SKIP); + MK_UNARY(Z3_mk_sbv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_SBVTOS, SKIP); Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) { diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 792b038e9..28e8aa052 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1447,6 +1447,11 @@ namespace z3 { check_error(); return expr(ctx(), r); } + expr sbvtos() const { + Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this); + check_error(); + return expr(ctx(), r); + } friend expr range(expr const& lo, expr const& hi); /** diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index d40281a81..7279fe847 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -556,18 +556,18 @@ namespace Microsoft.Z3 /// /// Bind a definition to a recursive function declaration. - /// The function must have previously been created using - /// MkRecFuncDecl. The body may contain recursive uses of the function or - /// other mutually recursive functions. + /// The function must have previously been created using + /// MkRecFuncDecl. The body may contain recursive uses of the function or + /// other mutually recursive functions. /// - public void AddRecDef(FuncDecl f, Expr[] args, Expr body) - { - CheckContextMatch(f); - CheckContextMatch(args); - CheckContextMatch(body); + public void AddRecDef(FuncDecl f, Expr[] args, Expr body) + { + CheckContextMatch(f); + CheckContextMatch(args); + CheckContextMatch(body); IntPtr[] argsNative = AST.ArrayToNative(args); - Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); - } + Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); + } /// /// Creates a new function declaration. @@ -2405,6 +2405,15 @@ namespace Microsoft.Z3 return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject)); } + /// + /// Convert a bit-vector expression, represented as an signed number, to a string. + /// + public SeqExpr SbvToString(Expr e) { + Debug.Assert(e != null); + Debug.Assert(e is ArithExpr); + return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject)); + } + /// /// Convert an integer expression to a string. /// @@ -2474,7 +2483,7 @@ namespace Microsoft.Z3 /// /// Check if the string s1 is lexicographically strictly less than s2. /// - public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) + public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2485,7 +2494,7 @@ namespace Microsoft.Z3 /// /// Check if the string s1 is lexicographically strictly less than s2. /// - public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) + public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2655,7 +2664,7 @@ namespace Microsoft.Z3 /// /// Create the empty regular expression. - /// The sort s should be a regular expression. + /// The sort s should be a regular expression. /// public ReExpr MkEmptyRe(Sort s) { @@ -2665,7 +2674,7 @@ namespace Microsoft.Z3 /// /// Create the full regular expression. - /// The sort s should be a regular expression. + /// The sort s should be a regular expression. /// public ReExpr MkFullRe(Sort s) { @@ -3399,7 +3408,7 @@ namespace Microsoft.Z3 { Debug.Assert(t1 != null); Debug.Assert(t2 != null); - // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); + // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); return AndThen(t1, t2, ts); } @@ -4696,7 +4705,7 @@ namespace Microsoft.Z3 { foreach (Z3Object a in arr) { - Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert + Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert CheckContextMatch(a); } } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index a6b867eb8..1e581c482 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2035,7 +2035,15 @@ public class Context implements AutoCloseable { { return (SeqExpr) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject())); } - + + /** + * Convert an signed bitvector expression to a string. + */ + public SeqExpr sbvToString(Expr e) + { + return (SeqExpr) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject())); + } + /** * Convert an integer expression to a string. */ diff --git a/src/api/z3_api.h b/src/api/z3_api.h index f636e7caa..79f7ca25d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1203,6 +1203,7 @@ typedef enum { Z3_OP_STR_TO_INT, Z3_OP_INT_TO_STR, Z3_OP_UBV_TO_STR, + Z3_OP_SBV_TO_STR, Z3_OP_STRING_LT, Z3_OP_STRING_LE, @@ -3655,6 +3656,12 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s); + /** + \brief Signed bit-vector to string conversion. + + def_API('Z3_mk_sbv_to_str' ,AST ,(_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s); /** \brief Create a regular expression that accepts the sequence \c seq. diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index e780ad7a7..25c68819a 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -406,6 +406,7 @@ public: app * mk_ule(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULEQ, arg1, arg2); } app * mk_sle(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLEQ, arg1, arg2); } + app * mk_slt(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLT, arg1, arg2); } app * mk_extract(unsigned high, unsigned low, expr * n) { parameter params[2] = { parameter(high), parameter(low) }; return m_manager.mk_app(get_fid(), OP_EXTRACT, 2, params, 1, &n); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index dcea166cd..312bab3bb 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -718,6 +718,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 1); st = mk_str_ubv2s(args[0], result); break; + case OP_STRING_SBVTOS: + SASSERT(num_args == 1); + st = mk_str_sbv2s(args[0], result); + break; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: case _OP_STRING_SUFFIX: @@ -2218,6 +2222,30 @@ br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) { return BR_FAILED; } +br_status seq_rewriter::mk_str_sbv2s(expr *a, expr_ref &result) { + bv_util bv(m()); + rational val; + unsigned bv_size = 0; + if (bv.is_numeral(a, val, bv_size)) { + rational r = mod(val, rational::power_of_two(bv_size)); + SASSERT(!r.is_neg()); + if (r >= rational::power_of_two(bv_size - 1)) { + r -= rational::power_of_two(bv_size); + } + result = str().mk_string(zstring(r)); + return BR_DONE; + } + + bv_size = bv.get_bv_size(a); + result = m().mk_ite( + bv.mk_slt(a,bv.mk_numeral(0, bv_size)), + str().mk_concat( + str().mk_string(zstring("-")), + str().mk_ubv2s(bv.mk_bv_neg(a)) + ), + str().mk_ubv2s(a)); + return BR_REWRITE_FULL; +} br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 7d102a5fb..c779a5f73 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -229,6 +229,7 @@ class seq_rewriter { br_status mk_str_itos(expr* a, expr_ref& result); br_status mk_str_stoi(expr* a, expr_ref& result); br_status mk_str_ubv2s(expr* a, expr_ref& result); + br_status mk_str_sbv2s(expr* a, expr_ref& result); br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result); br_status mk_str_to_regexp(expr* a, expr_ref& result); br_status mk_str_le(expr* a, expr* b, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index ea073f23f..6695d9497 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -350,7 +350,7 @@ func_decl* seq_decl_plugin::mk_left_assoc_fun(decl_kind k, unsigned arity, sort* return mk_assoc_fun(k, arity, domain, range, k_seq, k_string, false); } -func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) { +func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) const { ast_manager& m = *m_manager; if (arity != 1) m.raise_exception("Invalid str.from_ubv expects one bit-vector argument"); @@ -361,6 +361,17 @@ func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) { return m.mk_func_decl(symbol("str.from_ubv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_UBVTOS)); } +func_decl* seq_decl_plugin::mk_sbv2s(unsigned arity, sort* const* domain) const { + ast_manager &m = *m_manager; + if (arity != 1) + m.raise_exception("Invalid str.from_sbv expects one bit-vector argument"); + bv_util bv(m); + if (!bv.is_bv_sort(domain[0])) + m.raise_exception("Invalid str.from_sbv expects one bit-vector argument"); + sort *rng = m_string; + return m.mk_func_decl(symbol("str.from_sbv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_SBVTOS)); +} + func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string, bool is_right) { ast_manager& m = *m_manager; sort_ref rng(m); @@ -376,7 +387,7 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons } -func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { init(); m_has_seq = true; @@ -416,8 +427,12 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_STRING_FROM_CODE: match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + case OP_STRING_UBVTOS: - return mk_ubv2s(arity, domain); + return mk_ubv2s(arity, domain); + + case OP_STRING_SBVTOS: + return mk_sbv2s(arity, domain); case _OP_REGEXP_FULL_CHAR: m_has_re = true; @@ -627,6 +642,7 @@ void seq_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("re.nostr", _OP_REGEXP_EMPTY)); op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT)); op_names.push_back(builtin_name("str.from_ubv", OP_STRING_UBVTOS)); + op_names.push_back(builtin_name("str.from_sbv", OP_STRING_SBVTOS)); } void seq_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 61bbf7ba1..3c0f28ca6 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -80,6 +80,7 @@ enum seq_op_kind { OP_STRING_ITOS, OP_STRING_STOI, OP_STRING_UBVTOS, + OP_STRING_SBVTOS, OP_STRING_LT, OP_STRING_LE, OP_STRING_IS_DIGIT, @@ -150,7 +151,8 @@ class seq_decl_plugin : public decl_plugin { func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq); func_decl* mk_left_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq); func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq, bool is_right); - func_decl* mk_ubv2s(unsigned arity, sort* const* domain); + func_decl* mk_ubv2s(unsigned arity, sort* const* domain) const; + func_decl* mk_sbv2s(unsigned arity, sort* const* domain) const; void init(); @@ -297,6 +299,7 @@ public: app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); } app* mk_stoi(expr* s) const { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); } app* mk_ubv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_UBVTOS, 1, &b); } + app* mk_sbv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_SBVTOS, 1, &b); } app* mk_is_empty(expr* s) const; app* mk_lex_lt(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LT, 2, es); } app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); } @@ -336,6 +339,7 @@ public: bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); } bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); } bool is_ubv2s(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_UBVTOS); } + bool is_sbv2s(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_SBVTOS); } bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } bool is_lt(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LT); } @@ -374,6 +378,7 @@ public: MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); MATCH_UNARY(is_ubv2s); + MATCH_UNARY(is_sbv2s); MATCH_UNARY(is_is_digit); MATCH_UNARY(is_from_code); MATCH_UNARY(is_to_code);