mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-19 05:25:48 +00:00
Code Activity

make the batch explanation of fixed in row the default

Browse source
This commit is contained in:
Lev Nachmanson 2026-07-07 10:15:07 -07:00
parent b2f0d0682a
commit ff7e22c055
4 changed files with 0 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1135,15 +1135,7 @@ namespace lp {
// 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.
// When lp.batch_explain_fixed_in_row is disabled, fall back to explaining each
// fixed column independently (the pre-batching behavior).
void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) {
if (!settings().batch_explain_fixed_in_row()) {
for (auto const& c : get_row(row))
if (column_is_fixed(c.var()))
explain_fixed_column(c.var(), ex);
return;
}
auto& witnesses = m_imp->m_tmp_witnesses;
witnesses.reset();
for (auto const& c : get_row(row)) {