mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 05:46:08 +00:00
Code Activity

lp: avoid per-call join allocation in explain_fixed_column (#9984)

Browse source
This commit is contained in:
Lev Nachmanson 2026-06-28 08:12:52 -07:00 • committed by GitHub
parent f07acb459f
commit 56bb49f8dc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 24 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1125,8 +1125,10 @@ namespace lp {
void lar_solver::explain_fixed_column(unsigned j, explanation& ex) { void lar_solver::explain_fixed_column(unsigned j, explanation& ex) {
SASSERT(column_is_fixed(j)); SASSERT(column_is_fixed(j));
auto* deps = get_bound_constraint_witnesses_for_column(j); const column& ul = m_imp->m_columns[j];
for (auto ci : flatten(deps)) m_imp->m_tmp_dependencies.reset();
m_imp->m_dependencies.linearize(ul.lower_bound_witness(), ul.upper_bound_witness(), m_imp->m_tmp_dependencies);
for (auto ci : m_imp->m_tmp_dependencies)
ex.push_back(ci); ex.push_back(ci);
} }

20
src/util/dependency.h
View file

@ -234,6 +234,22 @@ public:
m_todo.reset(); m_todo.reset();
} }
// Linearize the union of two dependencies without allocating a join node.
void linearize(dependency * d1, dependency * d2, vector<value, false> & vs) const {
SASSERT(m_todo.empty());
if (d1) {
d1->mark();
m_todo.push_back(d1);
}
if (d2 && !d2->is_marked()) {
d2->mark();
m_todo.push_back(d2);
}
if (!m_todo.empty())
linearize_todo(m_todo, vs);
m_todo.reset();
}
void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) const { void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) const {
if (deps.empty()) if (deps.empty())
return; return;
@ -333,6 +349,10 @@ public:
return m_dep_manager.linearize(d, vs); return m_dep_manager.linearize(d, vs);
} }
void linearize(dependency * d1, dependency * d2, vector<value, false> & vs) const {
return m_dep_manager.linearize(d1, d2, vs);
}
static vector<value, false> const& s_linearize(dependency* d, vector<value, false>& vs) { static vector<value, false> const& s_linearize(dependency* d, vector<value, false>& vs) {
dep_manager::s_linearize(d, vs); dep_manager::s_linearize(d, vs);
return vs; return vs;