mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

tune backtracking

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-18 16:51:01 -08:00
parent 91c54f6c39
commit 3ed490d4ed
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1454,15 +1454,16 @@ namespace lp {
vector<unsigned> became_feas; vector<unsigned> became_feas;
clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.inf_set()); clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.inf_set());
std::unordered_set<unsigned> basic_columns_with_changed_cost; std::unordered_set<unsigned> basic_columns_with_changed_cost;
auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.inf_set(); m_inf_index_copy.reset();
for (auto j : inf_index_copy) { for (auto j : m_mpq_lar_core_solver.m_r_solver.inf_set())
m_inf_index_copy.push_back(j);
for (auto j : m_inf_index_copy) {
if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) {
continue; continue;
} }
// some basic columns might become non-basic - these columns need to be made feasible // some basic columns might become non-basic - these columns need to be made feasible
numeric_pair<mpq> delta; numeric_pair<mpq> delta;
if (m_mpq_lar_core_solver.m_r_solver.make_column_feasible(j, delta)) { if (m_mpq_lar_core_solver.m_r_solver.make_column_feasible(j, delta)) {
change_basic_columns_dependend_on_a_given_nb_column(j, delta); change_basic_columns_dependend_on_a_given_nb_column(j, delta);
} }
became_feas.push_back(j); became_feas.push_back(j);

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

@ -94,6 +94,8 @@ class lar_solver : public column_namer {
// these are basic columns with the value changed, so the the corresponding row in the tableau // these are basic columns with the value changed, so the the corresponding row in the tableau
// does not sum to zero anymore // does not sum to zero anymore
u_set m_incorrect_columns; u_set m_incorrect_columns;
// copy of m_r_solver.inf_set()
unsigned_vector m_inf_index_copy;
stacked_value<unsigned> m_term_count; stacked_value<unsigned> m_term_count;
vector<lar_term*> m_terms; vector<lar_term*> m_terms;
indexed_vector<mpq> m_column_buffer; indexed_vector<mpq> m_column_buffer;