From c78007fd1aa1d660bcaddfa848c40eed58e38096 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 29 Jun 2022 14:28:59 +0200 Subject: [PATCH] Use mul_ovfl constraint directly instead of approximating it with bounds --- src/math/polysat/saturation.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index 88f72b537..e85202bb6 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -181,9 +181,11 @@ namespace polysat { return x.manager().max_value(); } - // determine worst case upper bounds for x, y - // then extract premises for a non-worst-case bound. void inf_saturate::push_omega(pdd const& x, pdd const& y) { + m_new_constraints.insert(~s.mul_ovfl(x, y)); + /* + // determine worst case upper bounds for x, y + // then extract premises for a non-worst-case bound. auto& pddm = x.manager(); rational x_max = max_value(x); rational y_max = max_value(y); @@ -198,6 +200,7 @@ namespace polysat { for (auto const& c : s.m_viable.get_constraints(x.var())) m_new_constraints.insert(c); } + */ } /*