mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

do not throttle lp bound propagation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-07 14:21:11 -08:00
parent 6b01376f51
commit 6027224e34
2 changed files with 12 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/stacked_vector.h
View file

@ -140,8 +140,10 @@ public:
for (unsigned j = m_changes.size(); j-- > first_change; ) { for (unsigned j = m_changes.size(); j-- > first_change; ) {
const auto & p = m_changes[j]; const auto & p = m_changes[j];
unsigned jc = p.first; unsigned jc = p.first;
if (jc < m_vector.size()) if (jc < m_vector.size()) {
m_vector[jc] = p.second; // restore the old value m_vector[jc] = p.second; // restore the old value
m_vector[jc] = p.second; // restore the old value
}
} }
resize(m_changes, first_change); resize(m_changes, first_change);

24
src/smt/theory_lra.cpp
View file

@ -2346,23 +2346,18 @@ public:
} }
unsigned m_propagation_delay{1};
unsigned m_propagation_count{0};
bool should_propagate() { bool should_propagate() {
++m_propagation_count; return BP_NONE != propagation_mode();
return BP_NONE != propagation_mode() && (m_propagation_count >= m_propagation_delay);
} }
void update_propagation_threshold(bool made_progress) { // void update_propagation_threshold(bool made_progress) {
m_propagation_count = 0; // if (made_progress) {
if (made_progress) { // m_propagation_delay = std::max(1u, m_propagation_delay-1u);
m_propagation_delay = std::max(1u, m_propagation_delay-1u); // }
} // else {
else { // m_propagation_delay += 2;
m_propagation_delay += 2; // }
} // }
}
void propagate_bounds_with_lp_solver() { void propagate_bounds_with_lp_solver() {
if (!should_propagate()) if (!should_propagate())
@ -2383,7 +2378,6 @@ public:
propagate_lp_solver_bound(bp.m_ibounds[i]); propagate_lp_solver_bound(bp.m_ibounds[i]);
} }
} }
update_propagation_threshold(props < m_stats.m_bound_propagations1);
} }
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const { bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {