From 615aad77795d7aaa35c9afb335f3c26563923c8a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Sep 2023 15:18:37 -0700 Subject: [PATCH] get rid of int*, use lambda scoping Signed-off-by: Nikolaj Bjorner --- src/math/lp/bound_analyzer_on_row.h | 4 +- src/math/lp/implied_bound.h | 12 ++-- src/math/lp/lar_solver.h | 2 +- src/math/lp/lp_bound_propagator.h | 91 ++++++++++++++--------------- src/sat/smt/arith_solver.cpp | 2 +- 5 files changed, 55 insertions(+), 56 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 4bad3c0bc..074b6e464 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -284,7 +284,9 @@ private: void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){ unsigned row_index = this->m_row_index; - auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index](int * s) { return explain_bound_on_var_on_coeff((B*)s, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); }; + auto explain = [bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index,this]() { + return explain_bound_on_var_on_coeff((B*)&m_bp, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); + }; m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain); } diff --git a/src/math/lp/implied_bound.h b/src/math/lp/implied_bound.h index 66b3453d2..195ec0359 100644 --- a/src/math/lp/implied_bound.h +++ b/src/math/lp/implied_bound.h @@ -31,13 +31,13 @@ class implied_bound { // by lar_solver::add_term() unsigned m_j; bool m_is_lower_bound; - bool m_strict; + bool m_strict; private: - std::function m_explain_bound = nullptr; + std::function m_explain_bound = nullptr; public: // s is expected to be the pointer to lp_bound_propagator. - u_dependency* explain_implied(int * s) const { return m_explain_bound(s); } - void set_explain(std::function f) { m_explain_bound = f; } + u_dependency* explain_implied() const { return m_explain_bound(); } + void set_explain(std::function f) { m_explain_bound = f; } lconstraint_kind kind() const { lconstraint_kind k = m_is_lower_bound? GE : LE; if (m_strict) @@ -48,8 +48,8 @@ class implied_bound { implied_bound(const mpq & a, unsigned j, bool is_lower_bound, - bool is_strict, - std::function get_dep): + bool is_strict, + std::function get_dep): m_bound(a), m_j(j), m_is_lower_bound(is_lower_bound), diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 9af24d567..9f878e363 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -311,7 +311,7 @@ class lar_solver : public column_namer { template void explain_implied_bound(const implied_bound& ib, lp_bound_propagator& bp) { - u_dependency* dep = ib.explain_implied((int*)&bp); + u_dependency* dep = ib.explain_implied(); for (auto ci : flatten(dep)) bp.consume(mpq(1), ci); // TODO: flatten should provide the coefficients /* diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 8af04c793..e912d4f23 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -140,22 +140,24 @@ public: } void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) { - auto lambda = [zero_var](int* s) { - return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var); + auto& lps = lp(); + auto lambda = [zero_var,&lps]() { + return lps.get_bound_constraint_witnesses_for_column(zero_var); }; TRACE("add_bound", lp().print_column_info(zero_var, tout) << std::endl;); add_lower_bound_monic(monic_var, mpq(0), false, lambda); add_upper_bound_monic(monic_var, mpq(0), false, lambda); } - void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function explain_dep) { + void add_lower_bound_monic(lpvar j, const mpq& v, bool is_strict, std::function explain_dep) { TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;); j = lp().column_to_reported_index(j); unsigned k; if (!m_improved_lower_bounds.find(j, k)) { m_improved_lower_bounds.insert(j,static_cast(m_ibounds.size())); m_ibounds.push_back(implied_bound(v, j, true, is_strict, explain_dep)); - } else { + } + else { auto& found_bound = m_ibounds[k]; if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) { found_bound = implied_bound(v, j, true, is_strict, explain_dep); @@ -164,13 +166,14 @@ public: } } - void add_upper_bound_monic(lpvar j, const mpq& bound_val, bool is_strict, std::function explain_bound) { + void add_upper_bound_monic(lpvar j, const mpq& bound_val, bool is_strict, std::function explain_bound) { j = lp().column_to_reported_index(j); unsigned k; if (!m_improved_upper_bounds.find(j, k)) { m_improved_upper_bounds.insert(j, static_cast(m_ibounds.size())); m_ibounds.push_back(implied_bound(bound_val, j, false, is_strict, explain_bound)); - } else { + } + else { auto& found_bound = m_ibounds[k]; if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) { found_bound = implied_bound(bound_val, j, false, is_strict, explain_bound); @@ -204,18 +207,16 @@ public: 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; + auto& lps = lp(); 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) { - auto& l = ((lp_bound_propagator*)s)->lp(); - u_dependency* dep = l.get_column_lower_bound_witness(non_fixed); - for (auto v : vars) { - if (v != non_fixed) { - dep = l.join_deps(dep, l.get_bound_constraint_witnesses_for_column(v)); - } - } + auto lambda = [vars, non_fixed,&lps]() { + u_dependency* dep = lps.get_column_lower_bound_witness(non_fixed); + for (auto v : vars) + if (v != non_fixed) + dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v)); return dep; }; if (k.is_pos()) @@ -227,14 +228,11 @@ public: if (upper_bound_is_available(non_fixed)) { bound_value = lp().column_upper_bound(non_fixed); is_strict = !bound_value.y.is_zero(); - auto lambda = [vars, non_fixed](int* s) { - auto& l = ((lp_bound_propagator*)s)->lp(); - u_dependency* dep = l.get_column_upper_bound_witness(non_fixed); - for (auto v : vars) { - if (v != non_fixed) { - dep = l.join_deps(dep, l.get_bound_constraint_witnesses_for_column(v)); - } - } + auto lambda = [vars, non_fixed,&lps]() { + u_dependency* dep = lps.get_column_upper_bound_witness(non_fixed); + for (auto v : vars) + if (v != non_fixed) + dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v)); return dep; }; if (k.is_neg()) @@ -244,33 +242,31 @@ public: } if (lower_bound_is_available(monic_var)) { - auto lambda = [vars, monic_var, non_fixed](int* s) { - auto& l = ((lp_bound_propagator*)s)->lp(); - u_dependency* dep = l.get_column_lower_bound_witness(monic_var); - for (auto v : vars) { - if (v != non_fixed) { - dep = l.join_deps(dep, l.get_bound_constraint_witnesses_for_column(v)); - } - } - return dep; - }; - bound_value = lp().column_lower_bound(monic_var); - is_strict = !bound_value.y.is_zero(); - if (k.is_pos()) - add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda); - else - add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda); + auto lambda = [vars, monic_var, non_fixed,&lps]() { + u_dependency* dep = lps.get_column_lower_bound_witness(monic_var); + for (auto v : vars) { + if (v != non_fixed) { + dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v)); + } + } + return dep; + }; + bound_value = lp().column_lower_bound(monic_var); + is_strict = !bound_value.y.is_zero(); + if (k.is_pos()) + add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda); + else + add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, lambda); } - + if (upper_bound_is_available(monic_var)) { bound_value = lp().column_upper_bound(monic_var); is_strict = !bound_value.y.is_zero(); - auto lambda = [vars, monic_var, non_fixed](int* s) { - auto& l = ((lp_bound_propagator*)s)->lp(); - u_dependency* dep = l.get_column_upper_bound_witness(monic_var); + auto lambda = [vars, monic_var, non_fixed,&lps]() { + u_dependency* dep = lps.get_column_upper_bound_witness(monic_var); for (auto v : vars) { if (v != non_fixed) { - dep = l.join_deps(dep, l.get_bound_constraint_witnesses_for_column(v)); + dep = lps.join_deps(dep, lps.get_bound_constraint_witnesses_for_column(v)); } } return dep; @@ -283,9 +279,10 @@ public: } void propagate_monic_with_all_fixed(lpvar monic_var, const svector& vars, const rational& k) { - auto lambda = [vars](int* s) { return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_columns(vars); }; - add_lower_bound_monic(monic_var, k, false, lambda); - add_upper_bound_monic(monic_var, k, false, lambda); + auto& lps = lp(); + auto lambda = [vars,&lps]() { return lps.get_bound_constraint_witnesses_for_columns(vars); }; + add_lower_bound_monic(monic_var, k, false, lambda); + add_upper_bound_monic(monic_var, k, false, lambda); } column_type get_column_type(unsigned j) const { @@ -313,7 +310,7 @@ public: return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero(); } - void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function explain_bound) { + void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function explain_bound) { j = lp().column_to_reported_index(j); lconstraint_kind kind = is_low ? GE : LE; diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 65329f9c4..fd55fb7d7 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -253,7 +253,7 @@ namespace arith { first = false; reset_evidence(); m_explanation.clear(); - be.explain_implied((int*)&m_bp); + be.explain_implied(); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1);