mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

add base line bounds tightening utility

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-21 12:46:32 -08:00
parent 7044bb8485
commit 1a3d1ad69d
2 changed files with 85 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

82
src/math/lp/int_solver.cpp
View file

@ -30,7 +30,7 @@ namespace lp {
};
class int_solver::imp {
public:
public:
int_solver& lia;
lar_solver& lra;
lar_core_solver& lrac;
@ -196,6 +196,8 @@ namespace lp {
return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0;
}
// HNF
bool should_hnf_cut() {
return (!settings().dio_eqs() || settings().dio_enable_hnf_cuts())
&& settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0;
@ -210,6 +212,83 @@ namespace lp {
return r;
}
// Tighten bounds
// expose at level of lar_solver so it can be invoked by theory_lra after back-jumping
// consider multi-round bound tightnening as well and deal with divergence issues.
lia_move tighten_bounds() {
struct bound_consumer {
imp& i;
bound_consumer(imp& i) : i(i) {}
lar_solver& lp() { return i.lra; }
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational& bval) const { return true; }
bool add_eq(lpvar u, lpvar v, lp::explanation const& e, bool is_fixed) { return false; }
};
bound_consumer bc(*this);
std_vector<implied_bound> ibounds;
lp_bound_propagator<bound_consumer> bp(bc, ibounds);
bp.init();
unsigned num_refined_bounds = 0;
auto set_conflict = [&](unsigned j, u_dependency * d1, u_dependency * d2) {
++settings().stats().m_bounds_tightening_conflicts;
for (auto e : lra.flatten(d1))
m_ex->push_back(e);
for (auto e : lra.flatten(d2))
m_ex->push_back(e);
};
auto refine_bound = [&](implied_bound const& ib) {
unsigned j = ib.m_j;
auto const& bound = ib.m_bound;
if (!lra.column_is_int(j)) // for now, ignore non-integers.
return l_undef;
if (ib.m_is_lower_bound) {
if (lra.column_has_lower_bound(j) && lra.column_lower_bound(j) >= bound)
return l_undef;
auto d = ib.explain_implied();
if (lra.column_has_upper_bound(j) && lra.column_upper_bound(j) < ceil(bound)) {
set_conflict(j, d, lra.get_column_upper_bound_witness(j));
return l_false;
}
lra.update_column_type_and_bound(j, lconstraint_kind::GE, ceil(bound), d);
++num_refined_bounds;
} else {
if (lra.column_has_upper_bound(j) && lra.column_upper_bound(j) <= bound)
return l_undef;
auto d = ib.explain_implied();
if (lra.column_has_lower_bound(j) && lra.column_lower_bound(j) > floor(bound)) {
set_conflict(j, d, lra.get_column_lower_bound_witness(j));
return l_false;
}
lra.update_column_type_and_bound(j, lconstraint_kind::LE, floor(bound), d);
++num_refined_bounds;
}
return l_true;
};
for (unsigned row_index = 0; row_index < lra.row_count(); ++row_index) {
auto nb = bound_analyzer_on_row<row_strip<mpq>, lp_bound_propagator<bound_consumer>>::analyze_row(
lra.A_r().m_rows[row_index],
null_ci,
zero_of_type<numeric_pair<mpq>>(),
row_index,
bp);
settings().stats().m_bounds_tightenings += static_cast<unsigned>(ibounds.size());
for (auto const& ib : ibounds)
if (l_false == refine_bound(ib))
return lia_move::conflict;
ibounds.clear();
}
verbose_stream() << num_refined_bounds << "\n";
return num_refined_bounds > 0 ? lia_move::continue_with_check : lia_move::undef;
}
lia_move check(lp::explanation * e) {
SASSERT(lra.ax_is_correct());
@ -236,6 +315,7 @@ namespace lp {
if (r == lia_move::undef) r = patch_basic_columns();
if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)();
if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds();
// if (r == lia_move::undef) r = tighten_bounds();
if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut();
if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2);
if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();

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

@ -138,6 +138,8 @@ struct statistics {
unsigned m_dio_rewrite_conflicts = 0;
unsigned m_dio_branching_sats = 0;
unsigned m_dio_branching_conflicts = 0;
unsigned m_bounds_tightening_conflicts = 0;
unsigned m_bounds_tightenings = 0;
::statistics m_st = {};
void reset() {
@ -181,6 +183,8 @@ struct statistics {
st.update("arith-dio-branching-sats", m_dio_branching_sats);
st.update("arith-dio-branching-depth", m_dio_branching_depth);
st.update("arith-dio-branching-conflicts", m_dio_branching_conflicts);
st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
st.update("arith-bounds-tightenings", m_bounds_tightenings);
st.copy(m_st);
}
};