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

remove unsound axioms, fix #6115

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-29 11:16:10 -07:00
parent ff265235c1
commit 1a9122663c
2 changed files with 2 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/smt/arith_axioms.cpp
View file

@ -174,12 +174,7 @@ namespace arith {
}
else if (!a.is_numeral(q)) {
// (or (= y 0) (<= (* y (div x y)) x))
// (or (<= y 0) (>= (* (+ y 1) (div x y)) x))
// (or (>= y 0) (>= (* (+ y -1) (div x y)) x))
expr_ref one(a.mk_int(1), m);
add_clause(eqz, mk_literal(a.mk_le(a.mk_mul(q, div), p)));
add_clause(mk_literal(a.mk_le(q, zero)), mk_literal(a.mk_ge(a.mk_mul(a.mk_add(q, one), div), q)));
add_clause(mk_literal(a.mk_ge(q, zero)), mk_literal(a.mk_ge(a.mk_mul(a.mk_add(q, mone), div), q)));
}

13
src/smt/theory_arith_core.h
View file

@ -584,27 +584,18 @@ namespace smt {
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k;
if (m_util.is_zero(dividend) && false) {
if (m_util.is_zero(dividend)) {
mk_axiom(eqz, m.mk_eq(div, zero));
mk_axiom(eqz, m.mk_eq(mod, zero));
}
// (or (= y 0) (<= (* y (div x y)) x))
// (or (<= y 0) (>= (* (+ y 1) (div x y)) x))
// (or (>= y 0) (>= (* (+ y -1) (div x y)) x))
else if (!m_util.is_numeral(divisor)) {
expr_ref div_ge(m), div_le(m), ge(m), le(m);
div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero);
s(div_ge);
mk_axiom(eqz, div_ge, false);
ge = m_util.mk_ge(divisor, zero);
le = m_util.mk_le(divisor, zero);
div_le = m_util.mk_le(m_util.mk_sub(dividend, m_util.mk_mul(m_util.mk_add(divisor, one), div)), zero);
s(div_le);
mk_axiom(le, div_le, false);
div_le = m_util.mk_le(m_util.mk_sub(dividend, m_util.mk_mul(m_util.mk_sub(divisor, one), div)), zero);
s(div_le);
mk_axiom(ge, div_le, false);
TRACE("arith", tout << eqz << " " << div_ge << "\n");
}
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&