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

better tracking changinc rows and monomials

Browse source
This commit is contained in:
Lev Nachmanson 2023-09-29 15:27:22 -07:00
parent f30a2c13be
commit b64fdef41f
6 changed files with 35 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -200,16 +200,10 @@ namespace lp {
}
lp_status lar_solver::solve() {
if (m_status == lp_status::INFEASIBLE) {
if (m_status == lp_status::INFEASIBLE)
return m_status;
}
solve_with_core_solver();
if (m_status != lp_status::INFEASIBLE) {
if (m_settings.bound_propagation())
detect_rows_with_changed_bounds();
}
clear_columns_with_changed_bounds();
return m_status;
}
@ -789,8 +783,7 @@ namespace lp {
void lar_solver::detect_rows_with_changed_bounds() {
for (auto j : m_columns_with_changed_bounds)
detect_rows_with_changed_bounds_for_column(j);
if (m_find_monics_with_changed_bounds_func)
m_find_monics_with_changed_bounds_func(m_columns_with_changed_bounds);
}
void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() {
@ -1623,10 +1616,9 @@ namespace lp {
SASSERT(m_terms.size() == m_term_register.size());
unsigned adjusted_term_index = m_terms.size() - 1;
var_index ret = tv::mask_term(adjusted_term_index);
if (!coeffs.empty()) {
if (!coeffs.empty())
add_row_from_term_no_constraint(m_terms.back(), ret);
add_touched_row(A_r().row_count() - 1);
}
lp_assert(m_var_register.size() == A_r().column_count());
if (m_need_register_terms)
register_normalized_term(*t, A_r().column_count() - 1);

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

@ -89,6 +89,11 @@ class lar_solver : public column_namer {
constraint_set m_constraints;
// the set of column indices j such that bounds have changed for j
indexed_uint_set m_columns_with_changed_bounds;
public:
const indexed_uint_set& columns_with_changed_bounds() const { return m_columns_with_changed_bounds; }
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); }
private:
// m_touched_rows contains rows that have been changed by a pivoting or have a column with changed bounds
indexed_uint_set m_touched_rows;
unsigned_vector m_row_bounds_to_replay;
u_dependency_manager m_dependencies;
@ -138,9 +143,7 @@ class lar_solver : public column_namer {
void add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index);
void add_basic_var_to_core_fields();
bool compare_values(impq const& lhs, lconstraint_kind k, const mpq& rhs);
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); }
public:
public:
void insert_to_columns_with_changed_bounds(unsigned j);
const u_dependency* crossed_bounds_deps() const { return m_crossed_bounds_deps;}
u_dependency*& crossed_bounds_deps() { return m_crossed_bounds_deps;}
@ -149,12 +152,12 @@ class lar_solver : public column_namer {
lpvar& crossed_bounds_column() { return m_crossed_bounds_column; }
private:
private:
void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&);
void update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci);
public:
public:
void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
private:
private:
void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
@ -358,6 +361,8 @@ class lar_solver : public column_namer {
void add_column_rows_to_touched_rows(lpvar j);
template <typename T>
void propagate_bounds_for_touched_rows(lp_bound_propagator<T>& bp) {
detect_rows_with_changed_bounds();
clear_columns_with_changed_bounds();
if (settings().propagate_eqs()) {
if (settings().random_next() % 10 == 0)
remove_fixed_vars_from_base();
@ -688,7 +693,6 @@ class lar_solver : public column_namer {
return 0;
return m_usage_in_terms[j];
}
std::function<void (const indexed_uint_set& columns_with_changed_bound)> m_find_monics_with_changed_bounds_func = nullptr;
friend int_solver;
friend int_branch;
};

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

@ -41,19 +41,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp:
m_use_nra_model(false),
m_nra(s, m_nra_lim, *this),
m_implied_bounds(implied_bounds) {
m_nlsat_delay = lp_settings().nlsat_delay();
lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
m_monics_with_changed_bounds.reset();
for (lpvar j : columns_with_changed_bounds) {
if (is_monic_var(j))
m_monics_with_changed_bounds.insert(j);
else {
for (const auto & m: m_emons.get_use_list(j)) {
m_monics_with_changed_bounds.insert(m.var());
}
}
}
};
m_nlsat_delay = lp_settings().nlsat_delay();
}
bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
@ -1983,6 +1971,15 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
m_improved_upper_bounds.reset();
m_column_types = &lra.get_column_types();
m_lemmas.clear();
// find m_monics_with_changed_bounds
for (lpvar j : lra.columns_with_changed_bounds()) {
if (is_monic_var(j))
m_monics_with_changed_bounds.insert(j);
else {
for (const auto & m: m_emons.get_use_list(j)) {
m_monics_with_changed_bounds.insert(m.var());
}
}
}
}
} // namespace nla

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

@ -120,7 +120,7 @@ class core {
std_vector<lp::implied_bound> & m_implied_bounds;
// try to improve bounds for variables in monomials.
bool improve_bounds();
void clear_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); }
public:
// constructor
core(lp::lar_solver& s, params_ref const& p, reslimit&, std_vector<lp::implied_bound> & implied_bounds);

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

@ -110,7 +110,12 @@ namespace nla {
void solver::propagate_bounds_for_touched_monomials() {
init_bound_propagation();
for (unsigned v : monics_with_changed_bounds())
calculate_implied_bounds_for_monic(v);
for (unsigned v : m_core->monics_with_changed_bounds()) {
calculate_implied_bounds_for_monic(v);
if (m_core->lra.get_status() == lp::lp_status::INFEASIBLE) {
break;
}
}
m_core->clear_monics_with_changed_bounds();
}
}

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

@ -26,7 +26,6 @@ namespace nla {
solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds);
~solver();
const auto& monics_with_changed_bounds() const { return m_core->monics_with_changed_bounds(); }
void add_monic(lpvar v, unsigned sz, lpvar const* vs);
void add_idivision(lpvar q, lpvar x, lpvar y);
void add_rdivision(lpvar q, lpvar x, lpvar y);