From f9de65a464265655557f7656a3a3f6c3c0e11d9d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Sep 2023 15:22:28 -0700 Subject: [PATCH] indetation Signed-off-by: Nikolaj Bjorner --- src/math/lp/lp_bound_propagator.h | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index e912d4f23..f6cc83825 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -183,27 +183,27 @@ 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 (zero_var != null_lpvar) + lpvar non_fixed, zero_var; + if (!is_linear(vars, zero_var, non_fixed)) + return; + + 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) { k *= lp().get_column_value(v).x; if (k.is_big()) return; } - + if (non_fixed != null_lpvar) propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k); 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;