mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

ensure bounds propagation on changed columns after nla propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-10-03 14:28:59 +09:00
parent 7de06c4350
commit 00ba064cd3
2 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1067,6 +1067,8 @@ namespace lp {
}
bool lar_solver::init_model() const {
CTRACE("lar_solver_model",!m_columns_with_changed_bounds.empty(), tout << "non-empty changed bounds\n");
TRACE("lar_solver_model", tout << get_status() << "\n");
if (get_status() != lp_status::OPTIMAL && get_status() != lp_status::FEASIBLE)
return false;
if (!m_columns_with_changed_bounds.empty())

11
src/smt/theory_lra.cpp
View file

@ -2115,8 +2115,9 @@ public:
flush_bound_axioms();
// disabled in master:
propagate_nla();
if (!can_propagate_core())
if (!can_propagate_core())
return false;
m_new_def = false;
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
@ -2160,6 +2161,7 @@ public:
m_nla->propagate();
add_lemmas();
add_equalities();
propagate_bounds_with_lp_solver();
}
}
@ -2210,9 +2212,6 @@ public:
}
void propagate_bounds_with_lp_solver() {
if (!should_propagate())
return;
m_bp.init();
lp().propagate_bounds_for_touched_rows(m_bp);
@ -2224,13 +2223,11 @@ public:
// verbose_stream() << "unsat\n";
}
else {
unsigned count = 0, prop = 0;
for (auto& ib : m_bp.ibounds()) {
m.inc();
if (ctx().inconsistent())
break;
++prop;
count += propagate_lp_solver_bound(ib);
propagate_lp_solver_bound(ib);
}
}
}