From a88aa7ffa51769e607c5a6a9384a4f34f2320b74 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 3 Oct 2023 16:25:49 -0700
Subject: [PATCH] debug new propagation scheme
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/lar_solver.cpp | 4 +++-
src/math/lp/lar_solver.h | 3 ++-
src/math/lp/monomial_bounds.cpp | 6 +++---
src/smt/theory_lra.cpp | 4 ++++
4 files changed, 12 insertions(+), 5 deletions(-)
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 4049d7204..43acce576 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1822,6 +1822,7 @@ namespace lp {
if (is_base(j) && column_is_fixed(j))
m_fixed_base_var_set.insert(j);
+ track_column_feasibility(j);
TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j) ? "feas" : "non-feas") << ", and " << (this->column_is_bounded(j) ? "bounded" : "non-bounded") << " val = " << get_column_value(j) << std::endl;);
}
@@ -2359,7 +2360,8 @@ namespace lp {
// dep is the reason for the new bound
void lar_solver::set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep) {
- SASSERT(m_crossed_bounds_deps == nullptr && m_crossed_bounds_deps == nullptr);
+ if (m_crossed_bounds_column != null_lpvar) return; // already set
+ SASSERT(m_crossed_bounds_deps == nullptr);
set_status(lp_status::INFEASIBLE);
m_crossed_bounds_column = j;
const auto& ul = this->m_columns_to_ul_pairs()[j];
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 0748d2507..9b0dd8381 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -152,7 +152,8 @@ public:
lpvar crossed_bounds_column() const { return m_crossed_bounds_column; }
lpvar& crossed_bounds_column() { return m_crossed_bounds_column; }
-
+ bool current_x_is_feasible() const { return m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible(); }
+
private:
void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 8bb6ab306..0e4a5041e 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -311,8 +311,8 @@ namespace nla {
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
// propagate fixed equality
- auto exp = get_explanation(dep);
- c().add_fixed_equality(m.var(), k, exp);
+ auto exp = get_explanation(dep);
+ c().add_fixed_equality(c().lra.column_to_reported_index(m.var()), k, exp);
}
void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
@@ -327,7 +327,7 @@ namespace nla {
if (k == 1) {
lp::explanation exp = get_explanation(dep);
- c().add_equality(m.var(), w, exp);
+ c().add_equality(c().lra.column_to_reported_index(m.var()), c().lra.column_to_reported_index(w), exp);
}
}
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b746a88bf..7f7951b20 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2212,6 +2212,10 @@ public:
}
void propagate_bounds_with_lp_solver() {
+ if (!lp().current_x_is_feasible()) {
+ lp().clear_columns_with_changed_bounds();
+ return;
+ }
m_bp.init();
lp().propagate_bounds_for_touched_rows(m_bp);