mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix #3255

Browse source 
The model is fine, but debug facility that checks the model reports a false positive.
It exposed some further opportunities for simplification
This commit is contained in:
Nikolaj Bjorner 2020-03-12 10:57:35 -07:00
parent 7a80fe20ca
commit 356a9bb9ed
2 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/arith_decl_plugin.cpp
View file

@ -647,6 +647,13 @@ bool arith_decl_plugin::are_distinct(app * a, app * b) const {
if (is_app_of(a, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) && is_app_of(b, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) {
return am().neq(aw().to_anum(a->get_decl()), aw().to_anum(b->get_decl()));
}
if (is_app_of(a, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) && is_app_of(b, m_family_id, OP_NUM)) {
std::swap(a, b);
}
if (is_app_of(a, m_family_id, OP_NUM) && is_app_of(b, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM)) {
rational val = a->get_decl()->get_parameter(0).get_rational();
return am().neq(aw().to_anum(b->get_decl()), val.to_mpq());
}
#define is_non_zero(e) is_app_of(e,m_family_id, OP_NUM) && !to_app(e)->get_decl()->get_parameter(0).get_rational().is_zero()

6
src/ast/rewriter/bool_rewriter.cpp
View file

@ -754,6 +754,12 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
if (!all_value && all_diff) {
for (unsigned j = 0; all_diff && j < i; ++j) {
all_diff = m().are_distinct(arg, args[j]);
if (!all_diff) {
if (m().are_equal(arg, args[j])) {
result = m().mk_false();
return BR_DONE;
}
}
}
}
}