mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

add direct detection for integer expressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-07 09:54:18 -07:00
parent f450bc4ae0
commit f645bcf605
1 changed files with 36 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
src/ast/rewriter/arith_rewriter.cpp
View file

@ -1569,22 +1569,49 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {
} }
br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
numeral a; numeral n;
if (m_util.is_numeral(arg, a)) {
result = a.is_int() ? m.mk_true() : m.mk_false(); if (m_util.is_numeral(arg, n)) {
result = n.is_int() ? m.mk_true() : m.mk_false();
return BR_DONE; return BR_DONE;
} }
else if (m_util.is_to_real(arg)) {
if (m_util.is_to_real(arg)) {
result = m.mk_true(); result = m.mk_true();
return BR_DONE; return BR_DONE;
} }
else {
ptr_buffer<expr> todo;
todo.push_back(arg);
expr_fast_mark1 mark;
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];
if (mark.is_marked(e))
continue;
mark.mark(e, true);
if (m_util.is_to_real(e))
continue;
if (m_util.is_numeral(e, n)) {
if (n.is_int())
continue;
goto bail;
}
if (m_util.is_mul(e) || m_util.is_add(e) || m_util.is_sub(e) || m_util.is_uminus(e)) {
for (expr* a : *to_app(e))
todo.push_back(a);
continue;
}
goto bail;
}
result = m.mk_true();
return BR_DONE;
bail:
result = m.mk_eq(m.mk_app(get_fid(), OP_TO_REAL, result = m.mk_eq(m.mk_app(get_fid(), OP_TO_REAL,
m.mk_app(get_fid(), OP_TO_INT, arg)), m.mk_app(get_fid(), OP_TO_INT, arg)),
arg); arg);
return BR_REWRITE3; return BR_REWRITE3;
} }
}
br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) { br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {
result = m.mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg)); result = m.mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg));