mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

add ubv2s step 1

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-12 12:53:00 +02:00
parent 805bb58289
commit 1bc10cebc5
4 changed files with 34 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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)) {

1
src/ast/rewriter/seq_rewriter.h
View file

@ -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);

18
src/ast/seq_decl_plugin.cpp
View file

@ -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<builtin_name> & 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<builtin_name> & sort_names, symbol const & logic) {

4
src/ast/seq_decl_plugin.h
View file

@ -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);