mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
rewrites for characters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f20db3e644
commit
004139b320
|
@ -37,21 +37,57 @@ br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
|
|||
case OP_CHAR_CONST:
|
||||
break;
|
||||
case OP_CHAR_LE:
|
||||
st = mk_char_le(args[0], args[1], result);
|
||||
break;
|
||||
case OP_CHAR_TO_INT:
|
||||
st = mk_char_to_int(args[0], result);
|
||||
break;
|
||||
case OP_CHAR_TO_BV:
|
||||
st = mk_char_to_bv(args[0], result);
|
||||
break;
|
||||
case OP_CHAR_FROM_BV:
|
||||
st = mk_char_from_bv(args[0], result);
|
||||
break;
|
||||
case OP_CHAR_IS_DIGIT:
|
||||
st = mk_char_is_digit(args[0], result);
|
||||
break;
|
||||
}
|
||||
return st;
|
||||
}
|
||||
|
||||
br_status char_rewriter::mk_char_is_digit(expr* a, expr_ref& result) {
|
||||
unsigned n;
|
||||
if (!m_char->is_const_char(a, n))
|
||||
return BR_FAILED;
|
||||
result = m.mk_bool_val('0' <= n && n <= '9');
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
br_status char_rewriter::mk_char_to_bv(expr* a, expr_ref& result) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status char_rewriter::mk_char_le(expr* a, expr* b, expr_ref& result) {
|
||||
unsigned na = 0, nb = 0;
|
||||
if (m_char->is_const_char(a, na)) {
|
||||
if (na == 0) {
|
||||
result = m.mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
if (m_char->is_const_char(b, nb)) {
|
||||
if (na != 0) {
|
||||
result = m.mk_bool_val(na <= nb);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (nb == m_char->max_char()) {
|
||||
result = m.mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status char_rewriter::mk_char_from_bv(expr* e, expr_ref& result) {
|
||||
bv_util bv(m);
|
||||
rational n;
|
||||
|
|
|
@ -35,6 +35,12 @@ class char_rewriter {
|
|||
|
||||
br_status mk_char_to_int(expr* e, expr_ref& result);
|
||||
|
||||
br_status mk_char_le(expr* a, expr* b, expr_ref& result);
|
||||
|
||||
br_status mk_char_is_digit(expr* a, expr_ref& result);
|
||||
|
||||
br_status mk_char_to_bv(expr* a, expr_ref& result);
|
||||
|
||||
public:
|
||||
|
||||
char_rewriter(ast_manager& m);
|
||||
|
|
|
@ -532,7 +532,12 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
|
|||
case _OP_STRING_FROM_CHAR: {
|
||||
if (!(num_parameters == 1 && parameters[0].is_int()))
|
||||
m.raise_exception("character literal expects integer parameter");
|
||||
zstring zs(parameters[0].get_int());
|
||||
int i = parameters[0].get_int();
|
||||
if (i < 0)
|
||||
m.raise_exception("character literal expects a non-negative integer parameter");
|
||||
if (i > (int)m_char_plugin->max_char())
|
||||
m.raise_exception("character literal is out of bounds");
|
||||
zstring zs(i);
|
||||
parameter p(zs);
|
||||
return m.mk_const_decl(m_stringc_sym, m_string,func_decl_info(m_family_id, OP_STRING_CONST, 1, &p));
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue