From 77e56b0a6953ff1e03063c600b9f5f447ffcfe1c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 16 Sep 2023 13:54:14 -0700 Subject: [PATCH] debug --- src/math/lp/bound_analyzer_on_row.h | 1 + src/math/lp/implied_bound.h | 2 +- src/math/lp/lar_solver.h | 4 ++-- src/math/lp/lp_bound_propagator.h | 10 +++++++--- src/sat/smt/arith_solver.cpp | 2 +- 5 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index fa29d6201e9..642ed9d1c5b 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -319,6 +319,7 @@ public : } } 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) { + TRACE("bound_analyzer", tout << "explain_bound_on_var_on_coeff, bound_j = " << bound_j << ", coeff_before_j_is_pos = " << coeff_before_j_is_pos << ", is_lower_bound = " << is_lower_bound << ", strict = " << strict << ", row_index = " << row_index << "\n";); 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 e6d2bb89855..66b3453d215 100644 --- a/src/math/lp/implied_bound.h +++ b/src/math/lp/implied_bound.h @@ -36,7 +36,7 @@ class implied_bound { std::function m_explain_bound = nullptr; public: // s is expected to be the pointer to lp_bound_propagator. - u_dependency* explain(int * s) const { return m_explain_bound(s); } + u_dependency* explain_implied(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; diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index e2023aeaae1..9af24d567d2 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -311,9 +311,9 @@ class lar_solver : public column_namer { template void explain_implied_bound(const implied_bound& ib, lp_bound_propagator& bp) { - u_dependency* dep = ib.explain((int*)&bp); + u_dependency* dep = ib.explain_implied((int*)&bp); for (auto ci : flatten(dep)) - bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients + bp.consume(mpq(1), ci); // TODO: flatten should provide the coefficients /* if (ib.m_is_monic) { NOT_IMPLEMENTED_YET(); diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 61eeae32575..c7b0d1f3f82 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -137,14 +137,18 @@ class lp_bound_propagator { return n_of_non_fixed <= 1; } - void add_bounds_for_zero_var(lpvar monic_var, lpvar 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);}); + auto lambda = [zero_var](int* s) { + return ((lp_bound_propagator*)s)->lp().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) { unsigned k; + TRACE("add_bound", lp().print_column_info(j, tout) << std::endl;); j = lp().column_to_reported_index(j); if (!try_get_value(m_improved_lower_bounds, j, k)) { m_improved_lower_bounds[j] = m_ibounds.size(); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index d2e8e5b3941..65329f9c4c9 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((int*)&m_bp); + be.explain_implied((int*)&m_bp); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1);