From 65e59e3ec4ebd9c06469c15739a308d3c5f22d08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Sep 2023 20:43:38 -0700 Subject: [PATCH] sketch of internal propagation Signed-off-by: Nikolaj Bjorner --- src/math/lp/monomial_bounds.cpp | 28 +++++++++++++++------------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 96e4f9ba9..22b7ed6c6 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -298,19 +298,21 @@ namespace nla { u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) { u_dependency* dep = nullptr; - for (auto j : m.vars()) { - if (k == 0) { - if (c().var_is_fixed_to_zero(j)) { - dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j)); - dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j)); - return dep; - } - continue; - } - if (c().var_is_fixed(j)) { - dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j)); - dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j)); - } + auto update_dep = [&](unsigned j) { + dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_lower_bound_witness(j)); + dep = c().lra.dep_manager().mk_join(dep, c().lra.get_column_upper_bound_witness(j)); + return dep; + }; + + if (k == 0) { + for (auto j : m.vars()) + if (c().var_is_fixed_to_zero(j)) + return update_dep(j); + } + else { + for (auto j : m.vars()) + if (c().var_is_fixed(j)) + update_dep(j); } return dep; }