From f07553ed3a2ca03c69b0a60b13671a579b7313b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Sep 2023 15:18:38 -0700 Subject: [PATCH] formatting updates Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_bound_propagator.h | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index d035d9bcb..8af04c793 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -181,13 +181,12 @@ public: void propagate_monic(lpvar monic_var, const svector& vars) { lpvar non_fixed, zero_var; - if (!is_linear(vars, zero_var, non_fixed)) { - return; - } + if (!is_linear(vars, zero_var, non_fixed)) + return; - if (zero_var != null_lpvar) { + if (zero_var != null_lpvar) add_bounds_for_zero_var(monic_var, zero_var); - } else { + else { rational k = rational(1); for (auto v : vars) if (v != non_fixed) { @@ -195,19 +194,18 @@ public: if (k.is_big()) return; } - if (non_fixed != null_lpvar) { + if (non_fixed != null_lpvar) propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k); - } else { // all variables are fixed + else // all variables are fixed propagate_monic_with_all_fixed(monic_var, vars, k); - } } } void propagate_monic_with_non_fixed(lpvar monic_var, const svector& vars, lpvar non_fixed, const rational& k) { - lp::impq bound_value; - bool is_strict; + lp::impq bound_value; + bool is_strict; - if (lower_bound_is_available(non_fixed)) { + if (lower_bound_is_available(non_fixed)) { bound_value = lp().column_lower_bound(non_fixed); is_strict = !bound_value.y.is_zero(); auto lambda = [vars, non_fixed](int* s) {