mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Batch fixed-column bound-witness linearization per row

Browse source 
explain_fixed_in_row explained each fixed column of a row independently
via explain_fixed_column, re-traversing and re-inserting the shared
bound-witness dependency sub-DAGs once per column. Collect the lower and
upper witnesses of all fixed columns in the row and linearize them in a
single u_dependency_manager pass, so each shared sub-DAG node and each
distinct leaf constraint is handled once. explanation is a set, so the
result is identical.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-03 02:01:38 -07:00 • committed by GitHub
parent f15584cdae
commit 2dfed1d96c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 25 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -63,6 +63,7 @@ namespace lp {
unsigned_vector m_row_bounds_to_replay;
u_dependency_manager m_dependencies;
svector<constraint_index> m_tmp_dependencies;
ptr_vector<u_dependency> m_tmp_witnesses;
u_dependency* m_crossed_bounds_deps = nullptr;
lpvar m_crossed_bounds_column = null_lpvar;
@ -1132,6 +1133,24 @@ namespace lp {
ex.push_back(ci);
}
// Linearize the bound witnesses of all fixed columns in the row together, so the
// mark bits walk each dependency sub-DAG shared between columns only once.
void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) {
auto& witnesses = m_imp->m_tmp_witnesses;
witnesses.reset();
for (auto const& c : get_row(row)) {
if (!column_is_fixed(c.var()))
continue;
const column& ul = m_imp->m_columns[c.var()];
witnesses.push_back(ul.lower_bound_witness());
witnesses.push_back(ul.upper_bound_witness());
}
m_imp->m_tmp_dependencies.reset();
m_imp->m_dependencies.linearize(witnesses, m_imp->m_tmp_dependencies);
for (auto ci : m_imp->m_tmp_dependencies)
ex.push_back(ci);
}
void lar_solver::remove_fixed_vars_from_base() {
// this will allow to disable and restore the tracking of the touched rows
flet<indexed_uint_set*> f(get_core_solver().m_r_solver.m_touched_rows, nullptr);

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

@ -521,6 +521,7 @@ public:
}
void explain_fixed_column(unsigned j, explanation& ex);
void explain_fixed_in_row(unsigned row, explanation& ex);
u_dependency* join_deps(u_dependency* a, u_dependency *b) { return dep_manager().mk_join(a, b); }
const constraint_set & constraints() const;
void push();

16
src/math/lp/lp_bound_propagator.h
View file

@ -248,22 +248,16 @@ public:
void explain_fixed_in_row(unsigned row, explanation& ex) {
TRACE(eq, tout << lp().get_row(row) << std::endl);
for (const auto& c : lp().get_row(row))
if (lp().column_is_fixed(c.var()))
lp().explain_fixed_column(c.var(), ex);
lp().explain_fixed_in_row(row, ex);
}
unsigned explain_fixed_in_row_and_get_base(unsigned row, explanation& ex) {
unsigned base = UINT_MAX;
TRACE(eq, tout << lp().get_row(row) << std::endl);
for (const auto& c : lp().get_row(row)) {
if (lp().column_is_fixed(c.var())) {
lp().explain_fixed_column(c.var(), ex);
}
else if (lp().is_base(c.var())) {
lp().explain_fixed_in_row(row, ex);
unsigned base = UINT_MAX;
for (const auto& c : lp().get_row(row))
if (!lp().column_is_fixed(c.var()) && lp().is_base(c.var()))
base = c.var();
}
}
return base;
}