mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

Perf branch (#4710)

Browse source 
* avoid creating rows with  all but one fixed columns

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* pb

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* once in a while flip bounds of boxed variables during move_nbasic_to_bounds

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* flip rarely

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* flip rarely

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* flip rarely

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* return an empty model when lar_solver is not ready

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* randomly change bounded base var on demand only

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* randomly change bounded base var on demand only

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-09-25 17:47:29 -07:00 • committed by GitHub
parent e775964cfd
commit 25724401cf
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
10 changed files with 72 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -388,11 +388,7 @@ int gomory::find_basic_var() {
int result = -1; int result = -1;
unsigned n = 0; unsigned n = 0;
unsigned min_row_size = UINT_MAX; unsigned min_row_size = UINT_MAX;
// Prefer smaller row size // Prefer smaller row size
// Prefer boxed to non-boxed
// Prefer smaller ranges
for (unsigned j : lra.r_basis()) { for (unsigned j : lra.r_basis()) {
if (!lia.column_is_int_inf(j)) if (!lia.column_is_int_inf(j))
@ -400,7 +396,6 @@ int gomory::find_basic_var() {
const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(j)); const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(j));
if (!is_gomory_cut_target(row)) if (!is_gomory_cut_target(row))
continue; continue;
IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j))); IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j)));
if (min_row_size == UINT_MAX || if (min_row_size == UINT_MAX ||
2*row.size() < min_row_size || 2*row.size() < min_row_size ||
@ -414,7 +409,7 @@ int gomory::find_basic_var() {
} }
lia_move gomory::operator()() { lia_move gomory::operator()() {
lra.move_non_basic_columns_to_bounds(); lra.move_non_basic_columns_to_bounds(true);
int j = find_basic_var(); int j = find_basic_var();
if (j == -1) return lia_move::undef; if (j == -1) return lia_move::undef;
unsigned r = lia.row_of_basic_column(j); unsigned r = lia.row_of_basic_column(j);

22
src/math/lp/int_branch.cpp
View file

@ -25,8 +25,7 @@ namespace lp {
int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {} int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {}
lia_move int_branch::operator()() { lia_move int_branch::operator()() {
lra.move_non_basic_columns_to_bounds(); int j = find_inf_int_column();
int j = find_inf_int_base_column();
return j == -1? lia_move::sat : create_branch_on_column(j); return j == -1? lia_move::sat : create_branch_on_column(j);
} }
@ -51,7 +50,7 @@ lia_move int_branch::create_branch_on_column(int j) {
} }
int int_branch::find_inf_int_base_column() { int int_branch::find_inf_int_column() {
int result = -1; int result = -1;
mpq range; mpq range;
mpq new_range; mpq new_range;
@ -59,19 +58,16 @@ int int_branch::find_inf_int_base_column() {
unsigned n = 0; unsigned n = 0;
lar_core_solver & lcs = lra.m_mpq_lar_core_solver; lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
unsigned prev_usage = 0; // to quiet down the compile unsigned prev_usage = 0; // to quiet down the compile
unsigned k = 0;
unsigned usage; unsigned usage;
unsigned j; unsigned j = 0;
// this loop looks for a column with the most usages, but breaks when // this loop looks for a column with the most usages, but breaks when
// a column with a small span of bounds is found // a column with a small span of bounds is found
for (; k < lra.r_basis().size(); k++) { for (; j < lra.column_count(); j++) {
j = lra.r_basis()[k];
if (!lia.column_is_int_inf(j)) if (!lia.column_is_int_inf(j))
continue; continue;
usage = lra.usage_in_terms(j); usage = lra.usage_in_terms(j);
if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_range_thresold) { if (lia.is_boxed(j) && (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_range_thresold) {
result = j; result = j++;
k++;
n = 1; n = 1;
break; break;
} }
@ -83,14 +79,12 @@ int int_branch::find_inf_int_base_column() {
result = j; result = j;
} }
} }
SASSERT(k == lra.r_basis().size() || n == 1);
// this loop looks for boxed columns with a small span // this loop looks for boxed columns with a small span
for (; k < lra.r_basis().size(); k++) { for (; j < lra.column_count(); j++) {
j = lra.r_basis()[k];
usage = lra.usage_in_terms(j);
if (!lia.column_is_int_inf(j) || !lia.is_boxed(j)) if (!lia.column_is_int_inf(j) || !lia.is_boxed(j))
continue; continue;
SASSERT(!lia.is_fixed(j)); usage = lra.usage_in_terms(j);
new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage); new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage);
if (new_range < range) { if (new_range < range) {
n = 1; n = 1;

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

@ -28,7 +28,7 @@ namespace lp {
class int_solver& lia; class int_solver& lia;
class lar_solver& lra; class lar_solver& lra;
lia_move create_branch_on_column(int j); lia_move create_branch_on_column(int j);
int find_inf_int_base_column(); int find_inf_int_column();
public: public:
int_branch(int_solver& lia); int_branch(int_solver& lia);

2
src/math/lp/int_cube.cpp
View file

@ -43,7 +43,7 @@ namespace lp {
if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) { if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
TRACE("cube", tout << "cannot find a feasible solution";); TRACE("cube", tout << "cannot find a feasible solution";);
lra.pop(); lra.pop();
lra.move_non_basic_columns_to_bounds(); lra.move_non_basic_columns_to_bounds(false);
// it can happen that we found an integer solution here // it can happen that we found an integer solution here
return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef; return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
} }

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

@ -68,7 +68,6 @@ class int_solver {
bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise bool m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
hnf_cutter m_hnf_cutter; hnf_cutter m_hnf_cutter;
unsigned m_hnf_cut_period; unsigned m_hnf_cut_period;
public: public:
int_solver(lar_solver& lp); int_solver(lar_solver& lp);

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

@ -210,7 +210,7 @@ lp_status lar_solver::solve() {
detect_rows_with_changed_bounds(); detect_rows_with_changed_bounds();
} }
m_columns_with_changed_bound.clear(); clear_columns_with_changed_bounds();
return m_status; return m_status;
} }
@ -272,7 +272,7 @@ void lar_solver::pop(unsigned k) {
m_mpq_lar_core_solver.pop(k); m_mpq_lar_core_solver.pop(k);
remove_non_fixed_from_fixed_var_table(); remove_non_fixed_from_fixed_var_table();
clean_popped_elements(n, m_columns_with_changed_bound); clean_popped_elements(n, m_columns_with_changed_bounds);
clean_popped_elements(n, m_incorrect_columns); clean_popped_elements(n, m_incorrect_columns);
unsigned m = A_r().row_count(); unsigned m = A_r().row_count();
@ -335,7 +335,7 @@ bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const {
void lar_solver::set_costs_to_zero(const lar_term& term) { void lar_solver::set_costs_to_zero(const lar_term& term) {
auto & rslv = m_mpq_lar_core_solver.m_r_solver; auto & rslv = m_mpq_lar_core_solver.m_r_solver;
auto & jset = m_mpq_lar_core_solver.m_r_solver.inf_set(); // hijack this set that should be empty right now auto & jset = m_mpq_lar_core_solver.m_r_solver.inf_set(); // hijack this set that should be empty right now
lp_assert(jset.is_empty()); lp_assert(jset.empty());
for (const auto & p : term) { for (const auto & p : term) {
unsigned j = p.column(); unsigned j = p.column();
@ -361,7 +361,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
void lar_solver::prepare_costs_for_r_solver(const lar_term & term) { void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";); TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size()); m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
move_non_basic_columns_to_bounds(); move_non_basic_columns_to_bounds(false);
auto & rslv = m_mpq_lar_core_solver.m_r_solver; auto & rslv = m_mpq_lar_core_solver.m_r_solver;
rslv.set_using_infeas_costs(false); rslv.set_using_infeas_costs(false);
lp_assert(costs_are_zeros_for_r_solver()); lp_assert(costs_are_zeros_for_r_solver());
@ -379,34 +379,41 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
lp_assert(rslv.reduced_costs_are_correct_tableau()); lp_assert(rslv.reduced_costs_are_correct_tableau());
} }
void lar_solver::move_non_basic_columns_to_bounds() { void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) {
auto & lcs = m_mpq_lar_core_solver; auto & lcs = m_mpq_lar_core_solver;
bool change = false; bool change = false;
for (unsigned j : lcs.m_r_nbasis) { for (unsigned j : lcs.m_r_nbasis) {
if (move_non_basic_column_to_bounds(j)) if (move_non_basic_column_to_bounds(j, shift_randomly))
change = true; change = true;
} }
if (!change)
if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs && change) return;
if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs)
update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
if (change) {
find_feasible_solution(); find_feasible_solution();
} }
}
bool lar_solver::move_non_basic_column_to_bounds(unsigned j) { bool lar_solver::move_non_basic_column_to_bounds(unsigned j, bool force_change) {
auto & lcs = m_mpq_lar_core_solver; auto & lcs = m_mpq_lar_core_solver;
auto & val = lcs.m_r_x[j]; auto & val = lcs.m_r_x[j];
switch (lcs.m_column_types()[j]) { switch (lcs.m_column_types()[j]) {
case column_type::boxed: case column_type::boxed: {
if (val != lcs.m_r_lower_bounds()[j] && val != lcs.m_r_upper_bounds()[j]) { bool at_l = val == lcs.m_r_lower_bounds()[j];
if (m_settings.random_next() % 2 == 0) bool at_u = !at_l && (val == lcs.m_r_upper_bounds()[j]);
if (!at_l && !at_u) {
if (m_settings.random_next() % 2)
set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]); set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]);
else else
set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]); set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]);
return true; return true;
} else if (force_change && m_settings.random_next() % 3 == 0) {
set_value_for_nbasic_column(j,
at_l?lcs.m_r_upper_bounds()[j]:lcs.m_r_lower_bounds()[j]);
return true;
} }
}
break; break;
case column_type::lower_bound: case column_type::lower_bound:
if (val != lcs.m_r_lower_bounds()[j]) { if (val != lcs.m_r_lower_bounds()[j]) {
@ -414,18 +421,21 @@ bool lar_solver::move_non_basic_column_to_bounds(unsigned j) {
return true; return true;
} }
break; break;
case column_type::fixed:
case column_type::upper_bound: case column_type::upper_bound:
if (val != lcs.m_r_upper_bounds()[j]) { if (val != lcs.m_r_upper_bounds()[j]) {
set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]); set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]);
return true; return true;
} }
break; break;
default: case column_type::free_column:
if (column_is_int(j) && !val.is_int()) { if (column_is_int(j) && !val.is_int()) {
set_value_for_nbasic_column(j, impq(floor(val))); set_value_for_nbasic_column(j, impq(floor(val)));
return true; return true;
} }
break; break;
default:
SASSERT(false);
} }
return false; return false;
} }
@ -728,17 +738,17 @@ void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) {
} }
void lar_solver::detect_rows_with_changed_bounds() { void lar_solver::detect_rows_with_changed_bounds() {
for (auto j : m_columns_with_changed_bound) for (auto j : m_columns_with_changed_bounds)
detect_rows_with_changed_bounds_for_column(j); detect_rows_with_changed_bounds_for_column(j);
} }
void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds() { void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds() {
for (auto j : m_columns_with_changed_bound) for (auto j : m_columns_with_changed_bounds)
update_x_and_inf_costs_for_column_with_changed_bounds(j); update_x_and_inf_costs_for_column_with_changed_bounds(j);
} }
void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() { void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() {
for (auto j : m_columns_with_changed_bound) for (auto j : m_columns_with_changed_bounds)
update_x_and_inf_costs_for_column_with_changed_bounds(j); update_x_and_inf_costs_for_column_with_changed_bounds(j);
if (tableau_with_costs()) { if (tableau_with_costs()) {
@ -867,15 +877,6 @@ void lar_solver::copy_from_mpq_matrix(static_matrix<U, V> & matr) {
} }
} }
bool lar_solver::try_to_set_fixed(column_info<mpq> & ci) {
if (ci.upper_bound_is_set() && ci.lower_bound_is_set() && ci.get_upper_bound() == ci.get_lower_bound() && !ci.is_fixed()) {
ci.set_fixed_value(ci.get_upper_bound());
return true;
}
return false;
}
bool lar_solver::all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side) { bool lar_solver::all_constrained_variables_are_registered(const vector<std::pair<mpq, var_index>>& left_side) {
for (auto it : left_side) { for (auto it : left_side) {
if (! var_is_registered(it.second)) if (! var_is_registered(it.second))
@ -1114,7 +1115,8 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
// (x, y) != (x', y') => (x + delta*y) != (x' + delta*y') // (x, y) != (x', y') => (x + delta*y) != (x' + delta*y')
void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const { void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
if (!(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE)) { if (!(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE) ||
!m_columns_with_changed_bounds.empty()) {
variable_values.clear(); variable_values.clear();
return; return;
} }
@ -1549,7 +1551,7 @@ bool lar_solver::external_is_used(unsigned v) const {
void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) { void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) {
register_new_ext_var_index(ext_j, is_int); register_new_ext_var_index(ext_j, is_int);
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
m_columns_with_changed_bound.increase_size_by_one(); increase_by_one_columns_with_changed_bounds();
add_new_var_to_core_fields_for_mpq(false); // false for not adding a row add_new_var_to_core_fields_for_mpq(false); // false for not adding a row
if (use_lu()) if (use_lu())
add_new_var_to_core_fields_for_doubles(false); add_new_var_to_core_fields_for_doubles(false);
@ -1710,7 +1712,7 @@ void lar_solver::add_basic_var_to_core_fields() {
bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver(); bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver();
lp_assert(!use_lu || A_r().column_count() == A_d().column_count()); lp_assert(!use_lu || A_r().column_count() == A_d().column_count());
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
m_columns_with_changed_bound.increase_size_by_one(); increase_by_one_columns_with_changed_bounds();
m_incorrect_columns.increase_size_by_one(); m_incorrect_columns.increase_size_by_one();
m_rows_with_changed_bounds.increase_size_by_one(); m_rows_with_changed_bounds.increase_size_by_one();
add_new_var_to_core_fields_for_mpq(true); add_new_var_to_core_fields_for_mpq(true);
@ -2019,7 +2021,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return; if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci); set_upper_bound_witness(j, ci);
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
} }
break; break;
case GT: case GT:
@ -2034,7 +2036,7 @@ void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, con
return; return;
} }
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci); set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]? column_type::fixed : column_type::boxed); m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]? column_type::fixed : column_type::boxed);
} }
@ -2074,7 +2076,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind,
} }
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci); set_upper_bound_witness(j, ci);
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j]? column_type::fixed : column_type::boxed); m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j]? column_type::fixed : column_type::boxed);
} }
break; break;
@ -2087,7 +2089,7 @@ void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind,
return; return;
} }
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci); set_lower_bound_witness(j, ci);
} }
break; break;
@ -2124,7 +2126,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return; if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci); set_upper_bound_witness(j, ci);
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
} }
break; break;
case GT: case GT:
@ -2136,7 +2138,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
set_infeasible_column(j); set_infeasible_column(j);
} }
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci); set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]? column_type::fixed : column_type::boxed); m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]? column_type::fixed : column_type::boxed);
} }
@ -2161,7 +2163,7 @@ void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind,
} }
void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j)); lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j));
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
mpq y_of_bound(0); mpq y_of_bound(0);
switch (kind) { switch (kind) {
@ -2181,7 +2183,7 @@ void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kin
{ {
auto low = numeric_pair<mpq>(right_side, y_of_bound); auto low = numeric_pair<mpq>(right_side, y_of_bound);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
m_columns_with_changed_bound.insert(j); insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci); set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound; m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
} }

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

@ -88,7 +88,7 @@ class lar_solver : public column_namer {
stacked_vector<ul_pair> m_columns_to_ul_pairs; stacked_vector<ul_pair> m_columns_to_ul_pairs;
constraint_set m_constraints; constraint_set m_constraints;
// the set of column indices j such that bounds have changed for j // the set of column indices j such that bounds have changed for j
u_set m_columns_with_changed_bound; u_set m_columns_with_changed_bounds;
u_set m_rows_with_changed_bounds; u_set m_rows_with_changed_bounds;
u_set m_basic_columns_with_changed_cost; u_set m_basic_columns_with_changed_cost;
// 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
@ -135,6 +135,12 @@ class lar_solver : public column_namer {
void add_basic_var_to_core_fields(); void add_basic_var_to_core_fields();
bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs); bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs);
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.clear(); }
inline void increase_by_one_columns_with_changed_bounds() { m_columns_with_changed_bounds.increase_size_by_one(); }
inline void insert_to_columns_with_changed_bounds(unsigned j) {
m_columns_with_changed_bounds.insert(j);
}
void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, unsigned&); void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index, unsigned&);
void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
@ -588,8 +594,8 @@ public:
inline const int_solver * get_int_solver() const { return m_int_solver; } inline const int_solver * get_int_solver() const { return m_int_solver; }
inline const lar_term & get_term(tv const& t) const { lp_assert(t.is_term()); return *m_terms[t.id()]; } inline const lar_term & get_term(tv const& t) const { lp_assert(t.is_term()); return *m_terms[t.id()]; }
lp_status find_feasible_solution(); lp_status find_feasible_solution();
void move_non_basic_columns_to_bounds(); void move_non_basic_columns_to_bounds(bool);
bool move_non_basic_column_to_bounds(unsigned j); bool move_non_basic_column_to_bounds(unsigned j, bool);
inline bool r_basis_has_inf_int() const { inline bool r_basis_has_inf_int() const {
for (unsigned j : r_basis()) { for (unsigned j : r_basis()) {
if (column_is_int(j) && ! column_value_is_int(j)) if (column_is_int(j) && ! column_value_is_int(j))

2
src/math/lp/nla_core.cpp
View file

@ -1467,7 +1467,7 @@ lbool core::check(vector<lemma>& l_vec) {
init_to_refine(); init_to_refine();
patch_monomials(); patch_monomials();
set_use_nra_model(false); set_use_nra_model(false);
if (m_to_refine.is_empty()) { return l_true; } if (m_to_refine.empty()) { return l_true; }
init_search(); init_search();
lbool ret = l_undef; lbool ret = l_undef;

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

@ -87,7 +87,7 @@ public:
unsigned data_size() const { return m_data.size(); } unsigned data_size() const { return m_data.size(); }
unsigned size() const { return m_index.size();} unsigned size() const { return m_index.size();}
bool is_empty() const { return size() == 0; } bool empty() const { return size() == 0; }
void clear() { void clear() {
for (unsigned j : m_index) for (unsigned j : m_index)
m_data[j] = -1; m_data[j] = -1;

6
src/smt/theory_lra.cpp
View file

@ -921,6 +921,12 @@ class theory_lra::imp {
init_left_side(st); init_left_side(st);
lpvar vi = get_lpvar(v); lpvar vi = get_lpvar(v);
if (vi == UINT_MAX) { if (vi == UINT_MAX) {
if (m_left_side.empty()) {
vi = lp().add_var(v, a.is_int(term));
add_def_constraint_and_equality(vi, lp::GE, st.offset());
add_def_constraint_and_equality(vi, lp::LE, st.offset());
return v;
}
if (!st.offset().is_zero()) { if (!st.offset().is_zero()) {
m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term)))); m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term))));
} }