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

hoist out basic union find

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-21 11:10:42 -07:00
parent 6f575689b1
commit f100d4feda
2 changed files with 70 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

66
src/muz/transforms/dl_mk_quantifier_instantiation.h
View file

@ -28,6 +28,7 @@ Revision History:
#include "dl_rule_transformer.h" #include "dl_rule_transformer.h"
#include "expr_safe_replace.h" #include "expr_safe_replace.h"
#include "union_find.h"
namespace datalog { namespace datalog {
@ -37,75 +38,12 @@ namespace datalog {
class mk_quantifier_instantiation : public rule_transformer::plugin { class mk_quantifier_instantiation : public rule_transformer::plugin {
typedef svector<std::pair<expr*,expr*> > term_pairs; typedef svector<std::pair<expr*,expr*> > term_pairs;
class union_find {
unsigned_vector m_find;
unsigned_vector m_size;
unsigned_vector m_next;
void ensure_size(unsigned v) {
while (v >= get_num_vars()) {
mk_var();
}
}
public:
unsigned mk_var() {
unsigned r = m_find.size();
m_find.push_back(r);
m_size.push_back(1);
m_next.push_back(r);
return r;
}
unsigned get_num_vars() const { return m_find.size(); }
unsigned find(unsigned v) const {
if (v >= get_num_vars()) {
return v;
}
while (true) {
unsigned new_v = m_find[v];
if (new_v == v)
return v;
v = new_v;
}
}
unsigned next(unsigned v) const {
if (v >= get_num_vars()) {
return v;
}
return m_next[v];
}
bool is_root(unsigned v) const {
return v >= get_num_vars() || m_find[v] == v;
}
void merge(unsigned v1, unsigned v2) {
unsigned r1 = find(v1);
unsigned r2 = find(v2);
if (r1 == r2)
return;
ensure_size(v1);
ensure_size(v2);
if (m_size[r1] > m_size[r2])
std::swap(r1, r2);
m_find[r1] = r2;
m_size[r2] += m_size[r1];
std::swap(m_next[r1], m_next[r2]);
}
void reset() {
m_find.reset();
m_next.reset();
m_size.reset();
}
};
ast_manager& m; ast_manager& m;
context& m_ctx; context& m_ctx;
expr_safe_replace m_var2cnst; expr_safe_replace m_var2cnst;
expr_safe_replace m_cnst2var; expr_safe_replace m_cnst2var;
union_find m_uf; basic_union_find m_uf;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
ptr_vector<expr> m_terms; ptr_vector<expr> m_terms;
ptr_vector<expr> m_binding; ptr_vector<expr> m_binding;

66
src/util/union_find.h
View file

@ -173,5 +173,71 @@ public:
#endif #endif
}; };
class basic_union_find {
unsigned_vector m_find;
unsigned_vector m_size;
unsigned_vector m_next;
void ensure_size(unsigned v) {
while (v >= get_num_vars()) {
mk_var();
}
}
public:
unsigned mk_var() {
unsigned r = m_find.size();
m_find.push_back(r);
m_size.push_back(1);
m_next.push_back(r);
return r;
}
unsigned get_num_vars() const { return m_find.size(); }
unsigned find(unsigned v) const {
if (v >= get_num_vars()) {
return v;
}
while (true) {
unsigned new_v = m_find[v];
if (new_v == v)
return v;
v = new_v;
}
}
unsigned next(unsigned v) const {
if (v >= get_num_vars()) {
return v;
}
return m_next[v];
}
bool is_root(unsigned v) const {
return v >= get_num_vars() || m_find[v] == v;
}
void merge(unsigned v1, unsigned v2) {
unsigned r1 = find(v1);
unsigned r2 = find(v2);
if (r1 == r2)
return;
ensure_size(v1);
ensure_size(v2);
if (m_size[r1] > m_size[r2])
std::swap(r1, r2);
m_find[r1] = r2;
m_size[r2] += m_size[r1];
std::swap(m_next[r1], m_next[r2]);
}
void reset() {
m_find.reset();
m_next.reset();
m_size.reset();
}
};
#endif /* _UNION_FIND_H_ */ #endif /* _UNION_FIND_H_ */