From ffa12eb37c41048002e0a4ff9f4fdd91b6b614ed Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 5 Jan 2023 16:41:54 +0100 Subject: [PATCH] flip args to match description --- src/math/polysat/saturation.cpp | 10 ++++------ src/math/polysat/viable.cpp | 8 ++++---- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 7b79923c0..62b802b7c 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -1704,15 +1704,13 @@ namespace polysat { vector bounds; rational x_min, x_max; - if (!s.m_viable.has_max_forbidden(x, a_l_b.as_signed_constraint(), x_min, x_max, bounds)) + if (!s.m_viable.has_max_forbidden(x, a_l_b.as_signed_constraint(), x_max, x_min, bounds)) return false; - VERIFY(x_min != x_max); - // [x_min, x_max[ is allowed interval. + // retrieved maximal forbidden interval [x_max, x_min[. + // [x_min, x_max[ is the allowed interval. // compute [x_min, x_max - 1] - - // From forbidden interval [x_min, x_max[ compute - // allowed range: [x_max, x_min - 1] + VERIFY(x_min != x_max); SASSERT(0 <= x_min && x_min <= m.max_value()); SASSERT(0 <= x_max && x_max <= m.max_value()); rational M = m.two_to_N(); diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index dc19de801..6e5474a64 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -758,14 +758,14 @@ namespace polysat { } if (e == e0) { - out_hi = n->interval.lo_val(); + out_lo = n->interval.lo_val(); if (!n->interval.lo().is_val()) - out_c.push_back(s.eq(n->interval.lo(), out_hi)); + out_c.push_back(s.eq(n->interval.lo(), out_lo)); } else if (n == e0) { - out_lo = e->interval.hi_val(); + out_hi = e->interval.hi_val(); if (!e->interval.hi().is_val()) - out_c.push_back(s.eq(e->interval.hi(), out_lo)); + out_c.push_back(s.eq(e->interval.hi(), out_hi)); } else if (!e->interval.is_full()) { auto const& hi = e->interval.hi();