mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

DoC: fix bugs in the new join_project

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2014-10-07 14:33:23 +01:00
parent 1066955a0f
commit 06c7f3f246
2 changed files with 4 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz/rel/udoc_relation.cpp
View file

@ -80,7 +80,7 @@ namespace datalog {
void udoc_relation::reset() { void udoc_relation::reset() {
m_elems.reset(dm); m_elems.reset(dm);
} }
void udoc_relation::expand_column_vector(unsigned_vector& v, udoc_relation* other) const { void udoc_relation::expand_column_vector(unsigned_vector& v, const udoc_relation* other) const {
unsigned_vector orig; unsigned_vector orig;
orig.swap(v); orig.swap(v);
for (unsigned i = 0; i < orig.size(); ++i) { for (unsigned i = 0; i < orig.size(); ++i) {
@ -1076,13 +1076,12 @@ namespace datalog {
m_equalities(union_ctx) m_equalities(union_ctx)
{ {
udoc_plugin& p = t1.get_plugin(); udoc_plugin& p = t1.get_plugin();
udoc_relation* res = get(p.mk_empty(get_result_signature()));
unsigned num_bits = res->get_num_bits();
unsigned num_bits1 = t1.get_num_bits(); unsigned num_bits1 = t1.get_num_bits();
unsigned num_bits = num_bits1 + t2.get_num_bits();
unsigned_vector removed_cols(removed_col_cnt, rm_cols); unsigned_vector removed_cols(removed_col_cnt, rm_cols);
unsigned_vector expcols1(col_cnt, cols1); unsigned_vector expcols1(col_cnt, cols1);
unsigned_vector expcols2(col_cnt, cols2); unsigned_vector expcols2(col_cnt, cols2);
res->expand_column_vector(removed_cols); t1.expand_column_vector(removed_cols, &t2);
t1.expand_column_vector(expcols1); t1.expand_column_vector(expcols1);
t2.expand_column_vector(expcols2); t2.expand_column_vector(expcols2);
m_to_delete.resize(num_bits, false); m_to_delete.resize(num_bits, false);
@ -1096,7 +1095,6 @@ namespace datalog {
m_equalities.merge(expcols1[i], expcols2[i] + num_bits1); m_equalities.merge(expcols1[i], expcols2[i] + num_bits1);
} }
m_roots.append(expcols1); m_roots.append(expcols1);
res->deallocate();
} }

2
src/muz/rel/udoc_relation.h
View file

@ -62,7 +62,7 @@ namespace datalog {
unsigned get_num_cols() const { return m_column_info.size()-1; } unsigned get_num_cols() const { return m_column_info.size()-1; }
unsigned column_idx(unsigned col) const { return m_column_info[col]; } unsigned column_idx(unsigned col) const { return m_column_info[col]; }
unsigned column_num_bits(unsigned col) const { return m_column_info[col+1] - m_column_info[col]; } unsigned column_num_bits(unsigned col) const { return m_column_info[col+1] - m_column_info[col]; }
void expand_column_vector(unsigned_vector& v, udoc_relation* other = 0) const; void expand_column_vector(unsigned_vector& v, const udoc_relation* other = 0) const;
void extract_guard(expr* condition, expr_ref& guard, expr_ref& rest) const; void extract_guard(expr* condition, expr_ref& guard, expr_ref& rest) const;
bool is_guard(expr* g) const; bool is_guard(expr* g) const;
bool is_guard(unsigned n, expr* const *g) const; bool is_guard(unsigned n, expr* const *g) const;