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

make m_inf_set private and cosmetic improvements in nla patching

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-25 13:46:47 -07:00
parent d8cea7c8d5
commit caa384f6c9
12 changed files with 95 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/core_solver_pretty_printer_def.h
View file

@ -347,6 +347,11 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::print()
if (!m_core_solver.m_column_norms.empty())
print_approx_norms();
m_out << std::endl;
if (m_core_solver.inf_set().size()) {
m_out << "inf columns: ";
print_vector(m_core_solver.inf_set(), m_out);
m_out << std::endl;
}
}
template <typename T, typename X> void core_solver_pretty_printer<T, X>::print_basis_heading() {

9
src/math/lp/int_solver.cpp
View file

@ -503,18 +503,19 @@ bool int_solver::at_upper(unsigned j) const {
}
}
void int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
auto & rslv = lrac.m_r_solver;
for (const auto &c: rslv.m_A.m_rows[row_index]) {
if (numeric_traits<mpq>::is_pos(c.coeff()))
out << "+";
out << c.coeff() << rslv.column_name(c.var()) << " ";
}
out << "\n";
for (const auto& c: rslv.m_A.m_rows[row_index]) {
rslv.print_column_bound_info(c.var(), out);
rslv.print_column_info(c.var(), out);
if (is_base(c.var())) out << "j" << c.var() << " base\n";
}
rslv.print_column_bound_info(rslv.m_basis[row_index], out);
return out;
}
bool int_solver::shift_var(unsigned j, unsigned range) {

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

@ -118,8 +118,8 @@ public:
bool current_solution_is_inf_on_cut() const;
bool shift_var(unsigned j, unsigned range);
std::ostream& display_row_info(std::ostream & out, unsigned row_index) const;
private:
void display_row_info(std::ostream & out, unsigned row_index) const;
unsigned random();
bool has_inf_int() const;
public:

6
src/math/lp/lar_core_solver_def.h
View file

@ -217,8 +217,8 @@ void lar_core_solver::calculate_pivot_row(unsigned i) {
m_d_solver.m_steepest_edge_coefficients.resize(m_d_solver.m_n());
m_d_solver.m_column_norms.clear();
m_d_solver.m_column_norms.resize(m_d_solver.m_n(), 2);
m_d_solver.m_inf_set.clear();
m_d_solver.m_inf_set.resize(m_d_solver.m_n());
m_d_solver.clear_inf_set();
m_d_solver.resize_inf_set(m_d_solver.m_n());
}
void lar_core_solver::fill_not_improvable_zero_sum_from_inf_row() {
@ -268,7 +268,7 @@ void lar_core_solver::solve() {
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
lp_assert(m_r_solver.inf_set_is_correct());
TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.m_inf_set.size() << ", int_infs = " << get_number_of_non_ints() << std::endl;);
TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.inf_set_size() << ", int_infs = " << get_number_of_non_ints() << std::endl;);
if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) {
m_r_solver.set_status(lp_status::OPTIMAL);
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);

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

@ -420,7 +420,7 @@ bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const {
void lar_solver::set_costs_to_zero(const lar_term& term) {
auto & rslv = m_mpq_lar_core_solver.m_r_solver;
auto & jset = m_mpq_lar_core_solver.m_r_solver.m_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());
for (const auto & p : term) {
@ -558,7 +558,6 @@ bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term,
return false;
}
bool lar_solver::remove_from_basis(unsigned j) {
return m_mpq_lar_core_solver.m_r_solver.remove_from_basis(j);
}
@ -787,9 +786,9 @@ void lar_solver::change_basic_columns_dependend_on_a_given_nb_column(unsigned j,
void lar_solver::update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j) {
if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) {
if (costs_are_used()) {
bool was_infeas = m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j);
bool was_infeas = m_mpq_lar_core_solver.m_r_solver.inf_set_contains(j);
m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j);
if (was_infeas != m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j))
if (was_infeas != m_mpq_lar_core_solver.m_r_solver.inf_set_contains(j))
m_basic_columns_with_changed_cost.insert(j);
} else {
m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j);
@ -1208,7 +1207,7 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
variable_values.clear();
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1));
unsigned j;
unsigned n = m_mpq_lar_core_solver.m_r_x.size();
std::unordered_set<impq> set_of_different_pairs;
@ -1484,9 +1483,9 @@ void lar_solver::pop_tableau() {
void lar_solver::clean_inf_set_of_r_solver_after_pop() {
vector<unsigned> became_feas;
clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_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;
auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set;
auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.inf_set();
for (auto j: inf_index_copy) {
if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) {
continue;
@ -1504,16 +1503,16 @@ void lar_solver::clean_inf_set_of_r_solver_after_pop() {
lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0);
m_mpq_lar_core_solver.m_r_solver.m_d[j] -= m_mpq_lar_core_solver.m_r_solver.m_costs[j];
m_mpq_lar_core_solver.m_r_solver.m_costs[j] = zero_of_type<mpq>();
m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j);
m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j);
}
became_feas.clear();
for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_inf_set) {
for (unsigned j : m_mpq_lar_core_solver.m_r_solver.inf_set()) {
lp_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0);
if (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j))
became_feas.push_back(j);
}
for (unsigned j : became_feas)
m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j);
m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j);
if (use_tableau_costs()) {
@ -1662,7 +1661,7 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
m_mpq_lar_core_solver.m_r_x.resize(j + 1);
m_mpq_lar_core_solver.m_r_lower_bounds.increase_size_by_one();
m_mpq_lar_core_solver.m_r_upper_bounds.increase_size_by_one();
m_mpq_lar_core_solver.m_r_solver.m_inf_set.increase_size_by_one();
m_mpq_lar_core_solver.m_r_solver.inf_set_increase_size_by_one();
m_mpq_lar_core_solver.m_r_solver.m_costs.resize(j + 1);
m_mpq_lar_core_solver.m_r_solver.m_d.resize(j + 1);
lp_assert(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method
@ -2429,10 +2428,17 @@ bool lar_solver::inside_bounds(lpvar j, const impq& val) const {
return true;
}
void lar_solver::pivot_column_tableau(unsigned j, unsigned row_index) {
m_mpq_lar_core_solver.m_r_solver.pivot_column_tableau(j, row_index);
m_mpq_lar_core_solver.m_r_solver.change_basis(j, r_basis()[row_index]);
}
bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool (lpvar)>& blocker, const std::function<void (lpvar)>& report_change) {
if (is_base(j)) {
VERIFY(remove_from_basis(j));
if (is_base(j)) {
TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";);
remove_from_basis(j);
}
impq ival(val);
if (!inside_bounds(j, ival) || blocker(j))
return false;

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

@ -362,6 +362,8 @@ public:
return m_mpq_lar_core_solver.lower_bound(j);
}
void pivot_column_tableau(unsigned j, unsigned row_index);
inline const impq & column_upper_bound(unsigned j) const {
return m_mpq_lar_core_solver.upper_bound(j);
}

20
src/math/lp/lp_core_solver_base.h
View file

@ -51,10 +51,15 @@ public:
return m_inf_set.size() == 0;
}
bool current_x_is_infeasible() const { return m_inf_set.size() != 0; }
u_set m_inf_set;
private:
u_set m_inf_set;
bool m_using_infeas_costs;
public:
const u_set& inf_set() const { return m_inf_set; }
u_set& inf_set() { return m_inf_set; }
void inf_set_increase_size_by_one() { m_inf_set.increase_size_by_one(); }
bool inf_set_contains(unsigned j) const { return m_inf_set.contains(j); }
unsigned inf_set_size() const { return m_inf_set.size(); }
bool using_infeas_costs() const { return m_using_infeas_costs; }
void set_using_infeas_costs(bool val) { m_using_infeas_costs = val; }
vector<unsigned> m_columns_nz; // m_columns_nz[i] keeps an approximate value of non zeroes the i-th column
@ -723,13 +728,26 @@ public:
insert_column_into_inf_set(j);
}
void insert_column_into_inf_set(unsigned j) {
TRACE("lar_solver", tout << "j = " << j << "\n";);
m_inf_set.insert(j);
lp_assert(!column_is_feasible(j));
}
void remove_column_from_inf_set(unsigned j) {
TRACE("lar_solver", tout << "j = " << j << "\n";);
m_inf_set.erase(j);
lp_assert(column_is_feasible(j));
}
void resize_inf_set(unsigned size) {
TRACE("lar_solver",);
m_inf_set.resize(size);
}
void clear_inf_set() {
TRACE("lar_solver",);
m_inf_set.clear();
}
bool costs_on_nbasis_are_zeros() const {
lp_assert(this->basis_heading_is_correct());
for (unsigned j = 0; j < this->m_n(); j++) {

6
src/math/lp/lp_primal_core_solver.h
View file

@ -484,7 +484,7 @@ public:
int find_smallest_inf_column() {
int j = -1;
for (unsigned k : this->m_inf_set) {
for (unsigned k : this->inf_set()) {
if (k < static_cast<unsigned>(j)) {
j = k;
}
@ -821,12 +821,12 @@ public:
if (this->using_infeas_costs()) {
init_infeasibility_costs_for_changed_basis_only();
this->m_costs[leaving] = zero_of_type<T>();
this->m_inf_set.erase(leaving);
this->remove_column_from_inf_set(leaving);
}
}
void init_inf_set() {
this->m_inf_set.clear();
this->clear_inf_set();
for (unsigned j = 0; j < this->m_n(); j++) {
if (this->m_basis_heading[j] < 0)
continue;

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

@ -1179,7 +1179,7 @@ lp_primal_core_solver<T, X>::init_infeasibility_cost_for_column(unsigned j) {
// set zero cost for each non-basis column
if (this->m_basis_heading[j] < 0) {
this->m_costs[j] = numeric_traits<T>::zero();
this->m_inf_set.erase(j);
this->remove_column_from_inf_set(j);
return;
}
// j is a basis column

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

@ -1210,17 +1210,34 @@ bool core::elists_are_consistent(bool check_in_model) const {
return true;
}
bool core::var_is_used_in_a_correct_monic(lpvar j) const {
if (emons().is_monic_var(j)) {
if (!m_to_refine.contains(j))
return true;
}
for (const monic & m : emons().get_use_list(j)) {
if (!m_to_refine.contains(m.var())) {
TRACE("nla_solver", tout << "j" << j << " is used in a correct monic \n";);
return true;
bool core::var_breaks_correct_monic_as_factor(lpvar j, const monic& m) const {
if (!val(var(m)).is_zero())
return true;
if (!val(j).is_zero()) // j was not zero: the new value does not matter - m must have another zero product
return false;
// do we have another zero in m?
for (lpvar k : m) {
if (k != j && val(k).is_zero()) {
return false; // not breaking
}
}
// j was the only zero in m
return true;
}
bool core::var_breaks_correct_monic(lpvar j) const {
if (emons().is_monic_var(j) && !m_to_refine.contains(j)) {
TRACE("nla_solver", tout << "j = " << j << ", m = "; print_monic(emons()[j], tout) << "\n";);
return true; // changing the value of a correct monic
}
for (const monic & m : emons().get_use_list(j)) {
if (m_to_refine.contains(m.var()))
continue;
if (var_breaks_correct_monic_as_factor(j, m))
return true;
}
return false;
}
@ -1274,12 +1291,12 @@ bool core::has_real(const monic& m) const {
bool core::patch_blocker(lpvar u, const monic& m) const {
SASSERT(m_to_refine.contains(m.var()));
if (var_is_used_in_a_correct_monic(u)) {
if (var_breaks_correct_monic(u)) {
TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";);
return true;
}
bool ret = u == m.var() || m.contains_var(u);
bool ret = u == m.var() || (m.contains_var(u) && var_breaks_correct_monic_as_factor(u, m));
TRACE("nla_solver", tout << "u = " << u << ", m = "; print_monic(m, tout) <<
"ret = " << ret << "\n";);
@ -1326,7 +1343,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
if (val(j).is_zero() || v.is_zero()) // a lemma will catch it
return;
if (!var_is_int(j) && !var_is_used_in_a_correct_monic(j) && try_to_patch(j, v, m)) {
if (!var_breaks_correct_monic(j) && try_to_patch(j, v, m)) {
SASSERT(to_refine_is_correct());
return;
}
@ -1337,7 +1354,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
if (v.is_perfect_square(root)) {
lpvar k = m.vars()[0];
if (!var_is_int(k) &&
!var_is_used_in_a_correct_monic(k) &&
!var_breaks_correct_monic(k) &&
(try_to_patch(k, root, m) || try_to_patch(k, -root, m))
) {
}
@ -1352,7 +1369,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
lpvar k = m.vars()[l];
if (!in_power(m.vars(), l) &&
!var_is_int(k) &&
!var_is_used_in_a_correct_monic(k) &&
!var_breaks_correct_monic(k) &&
try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k
SASSERT(mul_val(m) == var_val(m));
erase_from_to_refine(j);

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

@ -466,7 +466,8 @@ public:
bool is_used_in_monic(lpvar) const;
void patch_monomials_with_real_vars();
void patch_monomial_with_real_var(lpvar);
bool var_is_used_in_a_correct_monic(lpvar) const;
bool var_breaks_correct_monic(lpvar) const;
bool var_breaks_correct_monic_as_factor(lpvar, const monic&) const;
void update_to_refine_of_var(lpvar j);
bool try_to_patch(lpvar, const rational&, const monic&);
bool to_refine_is_correct() const;

6
src/smt/theory_lra.cpp
View file

@ -1712,7 +1712,6 @@ public:
final_check_status st = FC_DONE;
switch (is_sat) {
case l_true:
TRACE("arith", display(tout););
switch (check_lia()) {
case l_true:
@ -2189,7 +2188,10 @@ public:
TRACE("arith", tout << "canceled\n";);
return l_undef;
}
if (!m_nla) return l_true;
if (!m_nla) {
TRACE("arith", tout << "no nla\n";);
return l_true;
}
if (!m_nla->need_check()) return l_true;
return check_nla_continue();
}