mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

debug new propagation scheme

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-10-03 16:25:49 -07:00
parent 00ba064cd3
commit a88aa7ffa5
4 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/lar_solver.cpp
View file

@ -1822,6 +1822,7 @@ namespace lp {
if (is_base(j) && column_is_fixed(j)) if (is_base(j) && column_is_fixed(j))
m_fixed_base_var_set.insert(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;); 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 // 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) { 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); set_status(lp_status::INFEASIBLE);
m_crossed_bounds_column = j; m_crossed_bounds_column = j;
const auto& ul = this->m_columns_to_ul_pairs()[j]; const auto& ul = this->m_columns_to_ul_pairs()[j];

3
src/math/lp/lar_solver.h
View file

@ -152,7 +152,8 @@ public:
lpvar crossed_bounds_column() const { return m_crossed_bounds_column; } lpvar crossed_bounds_column() const { return m_crossed_bounds_column; }
lpvar& crossed_bounds_column() { 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: private:
void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&); void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);

6
src/math/lp/monomial_bounds.cpp
View file

@ -311,8 +311,8 @@ namespace nla {
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep); c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
// propagate fixed equality // propagate fixed equality
auto exp = get_explanation(dep); auto exp = get_explanation(dep);
c().add_fixed_equality(m.var(), k, exp); 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) { void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
@ -327,7 +327,7 @@ namespace nla {
if (k == 1) { if (k == 1) {
lp::explanation exp = get_explanation(dep); 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);
} }
} }

4
src/smt/theory_lra.cpp
View file

@ -2212,6 +2212,10 @@ public:
} }
void propagate_bounds_with_lp_solver() { void propagate_bounds_with_lp_solver() {
if (!lp().current_x_is_feasible()) {
lp().clear_columns_with_changed_bounds();
return;
}
m_bp.init(); m_bp.init();
lp().propagate_bounds_for_touched_rows(m_bp); lp().propagate_bounds_for_touched_rows(m_bp);