mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

lp: gate per-row batched fixed-column explanation behind lp.batch_explain_fixed_in_row

Browse source 
Add lp.batch_explain_fixed_in_row (default true) so the batched
linearization of fixed-column bound witnesses in explain_fixed_in_row
can be toggled off, restoring the per-column explanation behavior for
A/B benchmarking.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-05 11:35:29 -07:00
parent 2dfed1d96c
commit a0da774400
4 changed files with 13 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1135,7 +1135,15 @@ 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)) {

1
src/math/lp/lp_params_helper.pyg
View file

@ -15,5 +15,6 @@ def_module_params(module_name='lp',
('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'),
('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'),
('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
('batch_explain_fixed_in_row', BOOL, True, 'linearize the bound witnesses of all fixed columns in a row in a single dependency pass (de-duplicating shared sub-DAGs) instead of explaining each fixed column independently'),
))

1
src/math/lp/lp_settings.cpp
View file

@ -46,6 +46,7 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
m_dio_calls_period_decrease = lp_p.dio_calls_period_decrease();
m_dio_run_gcd = lp_p.dio_run_gcd();
m_random_hammers = lp_p.random_hammers();
m_batch_explain_fixed_in_row = lp_p.batch_explain_fixed_in_row();
m_lcube = lp_p.lcube();
m_lcube_flips = lp_p.lcube_flips();
unsigned hammer_period = lp_p.int_hammer_period();

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

@ -268,6 +268,7 @@ private:
unsigned m_dio_calls_period_decrease = 2;
bool m_dio_run_gcd = true;
bool m_random_hammers = true;
bool m_batch_explain_fixed_in_row = true;
bool m_lcube = true;
unsigned m_lcube_flips = 16;
public:
@ -279,6 +280,8 @@ public:
unsigned & dio_calls_period_decrease() { return m_dio_calls_period_decrease; }
bool random_hammers() const { return m_random_hammers; }
bool & random_hammers() { return m_random_hammers; }
bool batch_explain_fixed_in_row() const { return m_batch_explain_fixed_in_row; }
bool & batch_explain_fixed_in_row() { return m_batch_explain_fixed_in_row; }
bool print_external_var_name() const { return m_print_external_var_name; }
bool propagate_eqs() const { return m_propagate_eqs;}
unsigned hnf_cut_period() const { return m_hnf_cut_period; }