From b3673d491e45e3319e155979630f9b74a1cccf11 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 14 Sep 2023 19:20:47 -0700 Subject: [PATCH] fix the build for gcc --- src/math/lp/bound_analyzer_on_row.h | 7 ++-- src/math/lp/implied_bound.h | 9 ++--- src/math/lp/lar_constraints.h | 4 +- src/math/lp/lar_solver.h | 2 +- src/math/lp/lp_bound_propagator.h | 58 ++++++++++++++--------------- src/sat/smt/arith_solver.cpp | 2 +- 6 files changed, 41 insertions(+), 41 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 5af864220..fa29d6201 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -284,8 +284,8 @@ 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](lar_solver& s) { return explain_bound_on_var_on_coeff(s, 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 ); + 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); }; + m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain); } void advance_u(unsigned j) { @@ -318,7 +318,8 @@ private: break; } } - static u_dependency* explain_bound_on_var_on_coeff(lar_solver& lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) { + static u_dependency* explain_bound_on_var_on_coeff(B* bp, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) { + auto& lar = bp->lp(); int bound_sign = (is_lower_bound ? 1 : -1); int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign; diff --git a/src/math/lp/implied_bound.h b/src/math/lp/implied_bound.h index 0df1f4f60..04f55f867 100644 --- a/src/math/lp/implied_bound.h +++ b/src/math/lp/implied_bound.h @@ -20,7 +20,6 @@ Revision History: #pragma once #include "math/lp/lp_settings.h" #include "math/lp/lar_constraints.h" -#include "math/lp/lar_solver.h" namespace lp { class implied_bound { public: @@ -34,10 +33,10 @@ class implied_bound { bool m_is_lower_bound; bool m_strict; private: - std::function m_explain_bound = nullptr; + std::function m_explain_bound = nullptr; public: - u_dependency* explain(lar_solver& s) const { return m_explain_bound(s); } - void set_explain(std::function f) { m_explain_bound = f; } + u_dependency* explain(int * s) const { return m_explain_bound(s); } + 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) @@ -49,7 +48,7 @@ class implied_bound { unsigned j, bool is_lower_bound, bool is_strict, - std::function get_dep): + std::function get_dep): m_bound(a), m_j(j), m_is_lower_bound(is_lower_bound), diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index 0a16353c1..b5e679e7e 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -137,8 +137,8 @@ class constraint_set { public: constraint_set(u_dependency_manager& d, column_namer& cn): - m_dep_manager(d), - m_namer(cn) {} + m_namer(cn), + m_dep_manager(d) {} ~constraint_set() { for (auto* c : m_constraints) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 50e9de7a3..e2023aeaa 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(*this); + u_dependency* dep = ib.explain((int*)&bp); for (auto ci : flatten(dep)) bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients /* diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index c67e99651..d48d9b50c 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -40,6 +40,8 @@ class lp_bound_propagator { return x != UINT_MAX; } public: + const lar_solver& lp() const { return m_imp.lp(); } + lar_solver& lp() { return m_imp.lp(); } bool upper_bound_is_available(unsigned j) const { switch (get_column_type(j)) { case column_type::fixed: @@ -138,12 +140,13 @@ private: return n_of_non_fixed <= 1 && !big_bound; } + void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) { - add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);}); - add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](lar_solver& s){return s.get_bound_constraint_witnesses_for_column(zero_var);}); + add_lower_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);}); + add_upper_bound_monic(monic_var, mpq(0), false, [zero_var](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_column(zero_var);}); } - void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function explain_dep) { + void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function explain_dep) { unsigned k; if (!try_get_value(m_improved_lower_bounds, monic_var, k)) { m_improved_lower_bounds[monic_var] = m_ibounds.size(); @@ -152,12 +155,12 @@ private: 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, monic_var, true, is_strict, explain_dep); - TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); } } } - void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function explain_bound) { + void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function explain_bound) { unsigned k; if (!try_get_value(m_improved_upper_bounds, monic_var, k)) { m_improved_upper_bounds[monic_var] = m_ibounds.size(); @@ -166,7 +169,7 @@ private: 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, monic_var, false, is_strict, explain_bound); - TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); } } } @@ -193,66 +196,63 @@ private: bound_value = lp().column_lower_bound(non_fixed); is_strict = !bound_value.y.is_zero(); if (k.is_pos()) - add_lower_bound_monic(monic_var, k * bound_value.x, is_strict , [non_fixed](lar_solver& s) { return s.get_column_lower_bound_witness(non_fixed); }); + add_lower_bound_monic(monic_var, k * bound_value.x, is_strict , [non_fixed](int* s) { return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(non_fixed); }); else - add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_lower_bound_witness(non_fixed);}); + add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(non_fixed);}); } if (upper_bound_is_available(non_fixed)) { bound_value = lp().column_upper_bound(non_fixed); is_strict = !bound_value.y.is_zero(); if (k.is_neg()) - add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);}); + add_lower_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(non_fixed);}); else - add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](lar_solver& s) {return s.get_column_upper_bound_witness(non_fixed);}); + add_upper_bound_monic(monic_var, k * bound_value.x, is_strict, [non_fixed](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(non_fixed);}); } if (lower_bound_is_available(monic_var)) { 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, [monic_var](lar_solver& s) {return s.get_column_lower_bound_witness(monic_var);}); + add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(monic_var);}); else - add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_lower_bound_witness(monic_var);}); + add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_lower_bound_witness(monic_var);}); } if (upper_bound_is_available(monic_var)) { bound_value = lp().column_upper_bound(monic_var); is_strict = !bound_value.y.is_zero(); if (k.is_neg()) - add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver& s) {return s.get_column_upper_bound_witness(monic_var);}); + add_lower_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(monic_var);}); else - add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](lar_solver & s) {return s.get_column_upper_bound_witness(monic_var);}); + add_upper_bound_monic(non_fixed, bound_value.x / k, is_strict, [monic_var](int* s) {return ((lp_bound_propagator*)s)->lp().get_column_upper_bound_witness(monic_var);}); } } else { // all variables are fixed - add_lower_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);}); - add_upper_bound_monic(monic_var, k, false, [vars](lar_solver& s){return s.get_bound_constraint_witnesses_for_columns(vars);}); + add_lower_bound_monic(monic_var, k, false, [vars](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_columns(vars);}); + add_upper_bound_monic(monic_var, k, false, [vars](int* s){return ((lp_bound_propagator*)s)->lp().get_bound_constraint_witnesses_for_columns(vars);}); } } } - const lar_solver& lp() const { return m_imp.lp(); } - lar_solver& lp() { return m_imp.lp(); } - column_type get_column_type(unsigned j) const { return (*m_column_types)[j]; } const impq& get_lower_bound(unsigned j) const { - return m_imp.lp().get_lower_bound(j); + return lp().get_lower_bound(j); } const mpq& get_lower_bound_rational(unsigned j) const { - return m_imp.lp().get_lower_bound(j).x; + return lp().get_lower_bound(j).x; } const impq& get_upper_bound(unsigned j) const { - return m_imp.lp().get_upper_bound(j); + return lp().get_upper_bound(j); } const mpq& get_upper_bound_rational(unsigned j) const { - return m_imp.lp().get_upper_bound(j).x; + return lp().get_upper_bound(j).x; } // require also the zero infinitesemal part @@ -260,8 +260,8 @@ private: 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) { - j = m_imp.lp().column_to_reported_index(j); + 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; if (strict) @@ -277,12 +277,12 @@ private: found_bound.m_bound = v; found_bound.m_strict = strict; found_bound.set_explain(explain_bound); - TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); } } else { m_improved_lower_bounds[j] = m_ibounds.size(); m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); - TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout);); } } else { // the upper bound case if (try_get_value(m_improved_upper_bounds, j, k)) { @@ -291,12 +291,12 @@ private: found_bound.m_bound = v; found_bound.m_strict = strict; found_bound.set_explain(explain_bound); - TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + TRACE("add_bound", lp().print_implied_bound(found_bound, tout);); } } else { m_improved_upper_bounds[j] = m_ibounds.size(); m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); - TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + TRACE("add_bound", lp().print_implied_bound(m_ibounds.back(), tout);); } } } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 346fbb7a9..d2e8e5b39 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(lp()); + be.explain((int*)&m_bp); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1);