From 1541c70b2be8bb74ddb17ea1eb2d4e7380b42e79 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Sat, 11 Mar 2023 09:50:08 +0100 Subject: [PATCH] Fix lemma_shl --- src/math/polysat/op_constraint.cpp | 33 ++++++++++++++++-------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp index 497265d0d..b8174f83f 100644 --- a/src/math/polysat/op_constraint.cpp +++ b/src/math/polysat/op_constraint.cpp @@ -258,14 +258,15 @@ namespace polysat { SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val())); // LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [>>] " << r() << " = " << (qv.val().is_unsigned() ? machine_div2k(pv.val(), qv.val().get_unsigned()) : rational::zero())); if (qv.is_val() && !rv.is_val()) { - const rational& qr = qv.val(); - if (qr >= N) - // q >= N -> r = 0 - return s.mk_clause(~lshr, ~s.ule(m.mk_val(N), q()), s.eq(r()), true); + rational const& q_val = qv.val(); + if (q_val >= N) + // q >= N ==> r = 0 + return s.mk_clause(~lshr, ~s.ule(N, q()), s.eq(r()), true); if (pv.is_val()) { - // p = pv & q = qv ==> r = rv - rational const rval = qr.is_unsigned() ? machine_div2k(pv.val(), qr.get_unsigned()) : rational::zero(); - return s.mk_clause(~lshr, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), m.mk_val(rval)), true); + SASSERT(q_val.is_unsigned()); + // p = p_val & q = q_val ==> r = p_val / 2^q_val + rational const r_val = machine_div2k(pv.val(), q_val.get_unsigned()); + return s.mk_clause(~lshr, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val), true); } } } @@ -336,15 +337,17 @@ namespace polysat { else { // forward propagation SASSERT(!(pv.is_val() && qv.is_val() && rv.is_val())); - LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [<<] " << r() << " = " << (qv.val().is_unsigned() ? rational::power_of_two(qv.val().get_unsigned()) * pv.val() : rational::zero())); + // LOG(p() << " = " << pv << " and " << q() << " = " << qv << " yields [<<] " << r() << " = " << (qv.val().is_unsigned() ? rational::power_of_two(qv.val().get_unsigned()) * pv.val() : rational::zero())); if (qv.is_val() && !rv.is_val()) { - const rational& qr = qv.val(); - if (qr >= N) - return s.mk_clause(~shl, ~s.ule(m.mk_val(m.power_of_2()), q()), s.eq(r()), true); - - if (rv.is_val()) { - const rational& pr = pv.val(); - return s.mk_clause(~shl, ~s.eq(p(), m.mk_val(pr)), ~s.eq(q(), m.mk_val(qr)), s.eq(r(), m.mk_val(rational::power_of_two(qr.get_unsigned()) * pr)), true); + rational const& q_val = qv.val(); + if (q_val >= N) + // q >= N ==> r = 0 + return s.mk_clause(~shl, ~s.ule(N, q()), s.eq(r()), true); + if (pv.is_val()) { + SASSERT(q_val.is_unsigned()); + // p = p_val & q = q_val ==> r = p_val * 2^q_val + rational const r_val = pv.val() * rational::power_of_two(q_val.get_unsigned()); + return s.mk_clause(~shl, ~s.eq(p(), pv), ~s.eq(q(), qv), s.eq(r(), r_val), true); } } }