From 1bc10cebc54d2a53ccf9ee5fb0b66530310780d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Jul 2021 12:53:00 +0200 Subject: [PATCH] add ubv2s step 1 --- src/ast/rewriter/seq_rewriter.cpp | 14 ++++++++++++++ src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 18 +++++++++++++++--- src/ast/seq_decl_plugin.h | 4 ++++ 4 files changed, 34 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6e0d0f7b7..8745326b0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -714,6 +714,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 1); st = mk_str_stoi(args[0], result); break; + case OP_STRING_UBVTOS: + SASSERT(num_args == 1); + st = mk_str_ubv2s(args[0], result); + break; case _OP_STRING_CONCAT: case _OP_STRING_PREFIX: case _OP_STRING_SUFFIX: @@ -2204,6 +2208,11 @@ br_status seq_rewriter::mk_str_is_digit(expr* a, expr_ref& result) { } +br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) { + return BR_FAILED; +} + + br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; if (m_autil.is_numeral(a, r)) { @@ -2265,6 +2274,11 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one()); return BR_DONE; } + if (str().is_ubv2s(a, b)) { + bv_util bv(m()); + result = bv.mk_bv2int(b); + return BR_DONE; + } expr* c = nullptr, *t = nullptr, *e = nullptr; if (m().is_ite(a, c, t, e)) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 60e4cf031..7d102a5fb 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -228,6 +228,7 @@ class seq_rewriter { br_status mk_str_units(func_decl* f, expr_ref& result); 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_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 7c76b3f64..111b567da 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -350,6 +350,17 @@ 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) { + ast_manager& m = *m_manager; + if (arity != 1) + m.raise_exception("Invalid str.from_ubv expects one bit-vector argument"); + bv_util bv(m); + if (!bv.is_bv_sort(domain[0])) + m.raise_exception("Invalid str.from_ubv expects one bit-vector argument"); + sort* rng = m_string; + 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_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); @@ -400,14 +411,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_STRING_STOI: case OP_STRING_LT: case OP_STRING_LE: - 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_IS_DIGIT: case OP_STRING_TO_CODE: 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: + NOT_IMPLEMENTED_YET(); + case _OP_REGEXP_FULL_CHAR: m_has_re = true; if (!range) range = mk_reglan(); @@ -615,6 +626,7 @@ void seq_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("int.to.str", OP_STRING_ITOS)); 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)); } 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 8ce0f7a4e..afb823284 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -79,6 +79,7 @@ enum seq_op_kind { OP_STRING_CONST, OP_STRING_ITOS, OP_STRING_STOI, + OP_STRING_UBVTOS, OP_STRING_LT, OP_STRING_LE, OP_STRING_IS_DIGIT, @@ -149,6 +150,7 @@ 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); void init(); @@ -332,6 +334,7 @@ public: bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); } 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_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); } @@ -369,6 +372,7 @@ public: MATCH_BINARY(is_le); MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); + MATCH_UNARY(is_ubv2s); MATCH_UNARY(is_is_digit); MATCH_UNARY(is_from_code); MATCH_UNARY(is_to_code);