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

use union_find in emonomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-14 17:20:08 -07:00
parent d78cc4975a
commit 45b72d7790
5 changed files with 123 additions and 84 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

99
src/util/lp/emonomials.cpp
View file

@ -36,7 +36,8 @@ void emonomials::inc_visited() const {
}
}
void emonomials::push() {
void emonomials::push() {
m_u_f_stack.push_scope();
m_lim.push_back(m_monomials.size());
m_region.push_scope();
m_ve.push();
@ -48,7 +49,7 @@ void emonomials::pop(unsigned n) {
unsigned old_sz = m_lim[m_lim.size() - n];
for (unsigned i = m_monomials.size(); i-- > old_sz; ) {
monomial & m = m_monomials[i];
remove_cg(i, m);
remove_cg_mon(m);
m_var2index[m.var()] = UINT_MAX;
lpvar last_var = UINT_MAX;
for (lpvar v : m.vars()) {
@ -63,6 +64,12 @@ void emonomials::pop(unsigned n) {
m_region.pop_scope(n);
m_lim.shrink(m_lim.size() - n);
SASSERT(monomials_are_canonized());
m_mons_to_rehash.clear();
m_u_f_stack.pop_scope(n);
for (unsigned j : m_mons_to_rehash) {
remove_cg_mon(m_monomials[j]);
insert_cg_mon(m_monomials[j]);
}
}
void emonomials::remove_cell(head_tail& v, unsigned mIndex) {
@ -161,32 +168,18 @@ void emonomials::remove_cg(lpvar v) {
monomial & m = m_monomials[idx];
if (!is_visited(m)) {
set_visited(m);
remove_cg(idx, m);
remove_cg_mon(m);
}
}
while (c != first);
}
void emonomials::remove_cg(unsigned idx, monomial& m) {
monomial& sv = m_monomials[idx];
unsigned next = sv.next();
unsigned prev = sv.prev();
void emonomials::remove_cg_mon(const monomial& m) {
lpvar u = m.var(), w;
// equivalence class of u:
if (m_cg_table.find(u, w) && w == u) {
if (m_cg_table.find(u, w)) {
TRACE("nla_solver", tout << "erase << " << m << "\n";);
m_cg_table.erase(u);
// insert other representative:
if (prev != idx) {
m_cg_table.insert(m_monomials[prev].var());
}
}
if (prev != idx) {
m_monomials[next].prev() = prev;
m_monomials[prev].next() = next;
sv.next() = idx;
sv.prev() = idx;
}
}
@ -212,28 +205,69 @@ void emonomials::insert_cg(lpvar v) {
monomial & m = m_monomials[idx];
if (!is_visited(m)) {
set_visited(m);
insert_cg(idx, m);
insert_cg_mon(m);
}
}
while (c != first);
}
void emonomials::insert_cg(unsigned idx, monomial & m) {
bool emonomials::elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector>& lists) const {
for (auto const & m : m_monomials) {
auto it = lists.find(m.rvars());
if (it == lists.end()) {
std::unordered_set<lpvar> v;
v.insert(m.var());
lists[m.rvars()] = v;
} else {
it->second.insert(m.var());
}
}
for (auto const & m : m_monomials) {
SASSERT(is_canonized(m));
if (!is_canonical_monomial(m.var()))
continue;
std::unordered_set<lpvar> c;
for (const monomial& e : enum_sign_equiv_monomials(m))
c.insert(e.var());
auto it = lists.find(m.rvars());
CTRACE("nla_solver", it->second != c,
tout << "m = " << m << "\n";
tout << "c = " ; print_vector(c, tout); tout << "\n";
if (it == lists.end()) {
tout << "m.rvars are not found\n";
}
else {
tout << "it->second = "; print_vector(it->second, tout); tout << "\n";
for (unsigned j : it->second) {
tout << (*this)[j] << "\n";
}
});
SASSERT(c == it->second);
}
return true;
}
void emonomials::insert_cg_mon(monomial & m) {
do_canonize(m);
lpvar v = m.var(), w;
if (m_cg_table.find(v, w)) {
SASSERT(w != v);
unsigned idxr = m_var2index[w];
unsigned idxl = m_monomials[idxr].prev();
m_monomials[idx].next() = idxr;
m_monomials[idx].prev() = idxl;
m_monomials[idxr].prev() = idx;
m_monomials[idxl].next() = idx;
if (v == w) {
TRACE("nla_solver", tout << "found " << v << "\n";);
return;
}
unsigned v_idx = m_var2index[v];
unsigned w_idx = m_var2index[w];
unsigned max_i = std::max(v_idx, w_idx);
while (m_u_f.get_num_vars() <= max_i)
m_u_f.mk_var();
TRACE("nla_solver", tout << "merge " << v << " idx " << v_idx << ", and " << w << " idx " << w_idx << "\n";);
m_u_f.merge(v_idx, w_idx);
}
else {
TRACE("nla_solver", tout << "insert " << m << "\n";);
m_cg_table.insert(v);
SASSERT(m_monomials[idx].next() == idx);
SASSERT(m_monomials[idx].prev() == idx);
}
}
@ -267,7 +301,7 @@ void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
}
SASSERT(m_ve.is_root(v));
m_var2index.setx(v, idx, UINT_MAX);
insert_cg(idx, m_monomials[idx]);
insert_cg_mon(m_monomials[idx]);
}
void emonomials::do_canonize(monomial & m) const {
@ -349,6 +383,7 @@ void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, sig
TRACE("nla_solver", tout << r2 << " <- " << r1 << "\n";);
if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged
m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1);
TRACE("nla_solver", tout << "rehasing " << r1.var() << "\n";);
rehash_cg(r1.var());
merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);
}

54
src/util/lp/emonomials.h
View file

@ -27,6 +27,12 @@
namespace nla {
struct hash_svector {
size_t operator()(const unsigned_vector & v) const {
return svector_hash<unsigned_hash>()(v);
}
};
class core;
class emonomials {
@ -73,9 +79,12 @@ class emonomials {
return uvec == vvec;
}
};
mutable svector<lpvar> m_find_key; // the key used when looking for a monomial with the specific variables
var_eqs<emonomials>& m_ve;
union_find<emonomials> m_u_f;
trail_stack<emonomials> m_u_f_stack;
std::unordered_set<unsigned> m_mons_to_rehash;
mutable svector<lpvar> m_find_key; // the key used when looking for a monomial with the specific variables
var_eqs<emonomials>& m_ve;
mutable vector<monomial> m_monomials; // set of monomials
mutable unsigned_vector m_var2index; // var_mIndex -> mIndex
unsigned_vector m_lim; // backtracking point
@ -86,6 +95,7 @@ class emonomials {
eq_canonical m_cg_eq;
hashtable<lpvar, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
void inc_visited() const;
void remove_cell(head_tail& v, unsigned mIndex);
@ -95,8 +105,8 @@ class emonomials {
void remove_cg(lpvar v);
void insert_cg(lpvar v);
void insert_cg(unsigned idx, monomial & m);
void remove_cg(unsigned idx, monomial & m);
void insert_cg_mon(monomial & m);
void remove_cg_mon(const monomial & m);
void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
void do_canonize(monomial& m) const;
@ -110,7 +120,9 @@ public:
push and pop on emonomials calls push/pop on var_eqs, so no
other calls to push/pop to the var_eqs should take place.
*/
emonomials(var_eqs<emonomials>& ve):
emonomials(var_eqs<emonomials>& ve):
m_u_f(*this),
m_u_f_stack(*this),
m_ve(ve),
m_visited(0),
m_cg_hash(*this),
@ -119,6 +131,18 @@ public:
m_ve.set_merge_handler(this);
}
void unmerge_eh(unsigned i, unsigned j) {
TRACE("nla_solver", tout << "unmerged " << i << " and " << j << "\n";);
m_mons_to_rehash.insert(i);
m_mons_to_rehash.insert(j);
}
void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {}
// this method is required by union_find
trail_stack<emonomials> & get_trail_stack() { return m_u_f_stack; }
/**
\brief push/pop scopes.
The life-time of a merge is local within a scope.
@ -229,7 +253,13 @@ public:
products_of get_products_of(lpvar v) const { inc_visited(); return products_of(*this, v); }
monomial const* find_canonical(svector<lpvar> const& vars) const;
bool is_canonical_monomial(lpvar j) const {
SASSERT(is_monomial_var(j));
unsigned idx = m_var2index[j];
if (idx >= m_u_f.get_num_vars())
return true;
return m_u_f.find(idx) == idx;
}
/**
\brief iterator over sign equivalent monomials.
These are monomials that are equivalent modulo m_var_eqs amd modulo signs.
@ -245,8 +275,9 @@ public:
monomial const& operator*() { return m.m_monomials[m_index]; }
sign_equiv_monomials_it& operator++() {
m_touched = true;
m_index = m.m_monomials[m_index].next();
m_touched = true;
if (m_index < m.m_u_f.get_num_vars())
m_index = m.m_u_f.next(m_index);
return *this;
}
@ -295,7 +326,10 @@ public:
void unmerge_eh(signed_var r2, signed_var r1);
bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
};
bool elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> &lists) const;
}; // end of emonomials
struct pp_emons {
const core& m_c;

8
src/util/lp/monomial.h
View file

@ -43,21 +43,15 @@ class monomial: public mon_eq {
// fields
svector<lpvar> m_rvars;
bool m_rsign;
unsigned m_next; // next congruent node.
unsigned m_prev; // previous congruent node
mutable unsigned m_visited;
public:
// constructors
monomial(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): monomial(v, svector<lpvar>(sz, vs), idx) {
}
monomial(lpvar v, const svector<lpvar> &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_next(idx), m_prev(idx), m_visited(0) {
monomial(lpvar v, const svector<lpvar> &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_visited(0) {
std::sort(vars().begin(), vars().end());
}
unsigned next() const { return m_next; }
unsigned& next() { return m_next; }
unsigned prev() const { return m_prev; }
unsigned& prev() { return m_prev; }
unsigned visited() const { return m_visited; }
unsigned& visited() { return m_visited; }
svector<lpvar> const& rvars() const { return m_rvars; }

44
src/util/lp/nla_core.cpp
View file

@ -133,7 +133,8 @@ void core::push() {
void core::pop(unsigned n) {
TRACE("nla_solver", tout << "n = " << n << "\n";);
m_emons.pop(n);
m_emons.pop(n);
SASSERT(elists_are_consistent(false));
}
rational core::product_value(const unsigned_vector & m) const {
@ -811,11 +812,7 @@ bool core::find_canonical_monomial_of_vars(const svector<lpvar>& vars, lpvar & i
}
bool core::is_canonical_monomial(lpvar j) const {
const monomial & m = m_emons[j];
unsigned k;
SASSERT(find_canonical_monomial_of_vars(m.rvars(), k));
find_canonical_monomial_of_vars(m.rvars(), k);
return j == k;
return m_emons.is_canonical_monomial(j);
}
@ -1366,6 +1363,7 @@ void core::clear() {
void core::init_search() {
clear();
init_vars_equivalence();
SASSERT(elists_are_consistent(false));
}
void core::init_to_refine() {
@ -1866,7 +1864,7 @@ lbool core:: inner_check(bool derived) {
}
if (derived) continue;
TRACE("nla_solver", tout << "passed derived and basic lemmas\n";);
SASSERT(elists_are_consistent());
SASSERT(elists_are_consistent(true));
if (search_level == 1) {
m_order.order_lemma();
} else { // search_level == 2
@ -1877,12 +1875,6 @@ lbool core:: inner_check(bool derived) {
return m_lemma_vec->empty()? l_undef : l_false;
}
struct hash_svector {
size_t operator()(const unsigned_vector & v) const {
return svector_hash<unsigned_hash>()(v);
}
};
bool core::elist_is_consistent(const std::unordered_set<lpvar> & list) const {
bool first = true;
bool p;
@ -1897,29 +1889,13 @@ bool core::elist_is_consistent(const std::unordered_set<lpvar> & list) const {
return true;
}
bool core::elists_are_consistent() const {
bool core::elists_are_consistent(bool check_in_model) const {
std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> lists;
for (auto const & m : m_emons) {
auto it = lists.find(m.rvars());
if (it == lists.end()) {
std::unordered_set<lpvar> v;
v.insert(m.var());
lists[m.rvars()] = v;
} else {
it->second.insert(m.var());
}
}
for (auto const & m : m_emons) {
if (!is_canonical_monomial(m.var()))
continue;
std::unordered_set<lpvar> c;
for (const monomial& e : m_emons.enum_sign_equiv_monomials(m))
c.insert(e.var());
auto it = lists.find(m.rvars());
SASSERT(it->second == c);
}
if (!m_emons.elists_are_consistent(lists))
return false;
if (!check_in_model)
return true;
for (const auto & p : lists) {
if (! elist_is_consistent(p.second))
return false;

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

@ -241,7 +241,7 @@ public:
bool find_canonical_monomial_of_vars(const svector<lpvar>& vars, lpvar & i) const;
bool is_canonical_monomial(lpvar) const;
bool elists_are_consistent() const;
bool elists_are_consistent(bool check_in_model) const;
bool elist_is_consistent(const std::unordered_set<lpvar>&) const;
bool var_has_positive_lower_bound(lpvar j) const;