From 30165ed40af81a3574da92c0abf8fdc8086f0d86 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Jun 2022 20:37:18 -0700 Subject: [PATCH] fix #6105 non-linear division axioms appear incomplete. Fixed for legacy arithmetic. Fix pending for new arithmetic solver. --- src/smt/theory_arith_core.h | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 88db34012..1610c4f53 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -574,7 +574,8 @@ namespace smt { lower = m_util.mk_ge(mod, zero); upper = m_util.mk_le(mod, abs_divisor); TRACE("div_axiom_bug", - tout << "eqz: " << eqz << " neq: " << eq << "\n"; + tout << "eqz: " << eqz << "\n"; + tout << "neq: " << eq << "\n"; tout << "lower: " << lower << "\n"; tout << "upper: " << upper << "\n";); @@ -583,14 +584,27 @@ namespace smt { mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor)); rational k; - if (!m_util.is_numeral(divisor)) { - // (=> (> y 0) (<= (* y (div x y)) x)) - // (=> (< y 0) ???) - expr_ref div_ge(m), div_non_pos(m); + if (m_util.is_zero(dividend) && false) { + 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); - div_non_pos = m_util.mk_le(divisor, zero); - mk_axiom(div_non_pos, div_ge, false); + 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); } if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&