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

add another constant folding case

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-03-10 17:39:40 -08:00
parent e839e18381
commit c51ca86203
2 changed files with 17 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/rewriter/char_rewriter.cpp
View file

@ -18,6 +18,8 @@ Author:
#include "util/debug.h" #include "util/debug.h"
#include "ast/rewriter/char_rewriter.h" #include "ast/rewriter/char_rewriter.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
char_rewriter::char_rewriter(ast_manager& m): char_rewriter::char_rewriter(ast_manager& m):
m(m) { m(m) {
@ -37,6 +39,7 @@ br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
case OP_CHAR_LE: case OP_CHAR_LE:
break; break;
case OP_CHAR_TO_INT: case OP_CHAR_TO_INT:
st = mk_char_to_int(args[0], result);
break; break;
case OP_CHAR_TO_BV: case OP_CHAR_TO_BV:
break; break;
@ -52,11 +55,19 @@ br_status char_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
br_status char_rewriter::mk_char_from_bv(expr* e, expr_ref& result) { br_status char_rewriter::mk_char_from_bv(expr* e, expr_ref& result) {
bv_util bv(m); bv_util bv(m);
rational n; rational n;
if (bv.is_numeral(e, n) && n.is_unsigned()) { if (bv.is_numeral(e, n) && n.is_unsigned() && n <= m_char->max_char()) {
if (n > m_char->max_char())
return BR_FAILED;
result = m_char->mk_char(n.get_unsigned()); result = m_char->mk_char(n.get_unsigned());
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
} }
br_status char_rewriter::mk_char_to_int(expr* e, expr_ref& result) {
unsigned n = 0;
if (m_char->is_const_char(e, n)) {
arith_util arith(m);
result = arith.mk_int(n);
return BR_DONE;
}
return BR_FAILED;
}

3
src/ast/rewriter/char_rewriter.h
View file

@ -32,6 +32,9 @@ class char_rewriter {
char_decl_plugin* m_char; char_decl_plugin* m_char;
br_status mk_char_from_bv(expr* e, expr_ref& result); br_status mk_char_from_bv(expr* e, expr_ref& result);
br_status mk_char_to_int(expr* e, expr_ref& result);
public: public:
char_rewriter(ast_manager& m); char_rewriter(ast_manager& m);