From 76c18ee6e343195b47c9baa2e7c42773ea455f57 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 3 Apr 2023 16:18:01 +0200 Subject: [PATCH] Fix try_ugt_y --- src/math/polysat/saturation.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 8b4260fcc..bb5affa54 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -569,9 +569,11 @@ namespace polysat { /** * [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx - * [y] z' <= y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx - * [y] z' < y /\ yx <= zx ==> Ω*(x,y) \/ z'x < zx - * [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx TODO: could strengthen the conclusion to z'x + 1 < zx + * [y] z' <= y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx + * [y] z' < y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx + * [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ z'x < zx + * [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ z'x + 1 < zx (TODO?) + * [y] z' < y /\ yx < zx ==> Ω*(x,y) \/ (z' + 1)x < zx (TODO?) */ bool saturation::try_ugt_y(pvar v, conflict& core, inequality const& yx_l_zx) { set_rule("[y] z' <= y & yx <= zx"); @@ -605,7 +607,7 @@ namespace polysat { pdd const& z_prime = l_y.lhs(); m_lemma.reset(); m_lemma.insert_eval(~non_ovfl); - return add_conflict(v, core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict() || l_y.is_strict(), z_prime * x, z * x)); + return add_conflict(v, core, l_y, yx_l_zx, ineq(yx_l_zx.is_strict(), z_prime * x, z * x)); } /**