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

track changed monics efficiently

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-09-27 09:09:38 -07:00
parent 42767b9aab
commit 29b5c47a8d
4 changed files with 11 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -43,18 +43,17 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp:
m_implied_bounds(implied_bounds) { m_implied_bounds(implied_bounds) {
m_nlsat_delay = lp_settings().nlsat_delay(); m_nlsat_delay = lp_settings().nlsat_delay();
lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) { lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
for (const auto& m : m_emons) { m_monics_with_changed_bounds.reset();
if (columns_with_changed_bounds.contains(m.var())) { for (lpvar j : columns_with_changed_bounds) {
m_monics_with_changed_bounds.push_back(m.var()); if (is_monic_var(j))
continue; m_monics_with_changed_bounds.insert(j);
} else {
for (lpvar j : m.vars()) { for (const auto & m: m_emons.get_use_list(j)) {
if (columns_with_changed_bounds.contains(j)) { m_monics_with_changed_bounds.insert(m.var());
m_monics_with_changed_bounds.push_back(m.var()); }
break;
} }
} }
} }; };
} }
bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const { bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {

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

@ -88,7 +88,7 @@ class core {
vector<lemma> m_lemmas; vector<lemma> m_lemmas;
vector<ineq> * m_literal_vec = nullptr; vector<ineq> * m_literal_vec = nullptr;
indexed_uint_set m_to_refine; indexed_uint_set m_to_refine;
vector<lpvar> m_monics_with_changed_bounds; indexed_uint_set m_monics_with_changed_bounds;
tangents m_tangents; tangents m_tangents;
basics m_basics; basics m_basics;
order m_order; order m_order;
@ -125,7 +125,6 @@ public:
// constructor // constructor
core(lp::lar_solver& s, params_ref const& p, reslimit&, std_vector<lp::implied_bound> & implied_bounds); core(lp::lar_solver& s, params_ref const& p, reslimit&, std_vector<lp::implied_bound> & implied_bounds);
const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; } const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; }
void reset_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); }
void insert_to_refine(lpvar j); void insert_to_refine(lpvar j);
void erase_from_to_refine(lpvar j); void erase_from_to_refine(lpvar j);

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

@ -112,6 +112,5 @@ namespace nla {
init_bound_propagation(); init_bound_propagation();
for (unsigned v : monics_with_changed_bounds()) for (unsigned v : monics_with_changed_bounds())
calculate_implied_bounds_for_monic(v); calculate_implied_bounds_for_monic(v);
reset_monics_with_changed_bounds();
} }
} }

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

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