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

DoC: code cleanups

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2014-09-30 17:16:14 +01:00
parent 8d1177bf3f
commit 115ab12ade
5 changed files with 30 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/muz/rel/doc.cpp
View file

@ -280,7 +280,7 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
// indices where BIT_0 is set are positive.
//
doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
doc* doc_manager::project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src) {
tbv_manager& dstt = dstm.m;
tbv_ref t(dstt);
t = dstt.project(n, to_delete, src.pos());
@ -391,7 +391,7 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
doc_manager::project_action_t
doc_manager::pick_resolvent(
tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx) {
tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx) {
if (neg.empty()) return project_done;
for (unsigned j = 0; j < neg.size(); ++j) {
if (m.equals(pos, *neg[j])) return project_is_empty;
@ -401,7 +401,7 @@ doc_manager::pick_resolvent(
unsigned best_neg = UINT_MAX;
unsigned best_idx = UINT_MAX;
for (unsigned i = 0; i < num_tbits(); ++i) {
if (!to_delete[i]) continue;
if (!to_delete.get(i)) continue;
if (pos[i] != BIT_x) continue;
unsigned num_pos = 0, num_neg = 0;
tbit b1 = (*neg[0])[i];
@ -480,7 +480,6 @@ void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
for (unsigned i = 0; i < B.neg().size(); ++i) {
r = allocate(A);
if (set_and(*r, B.neg()[i])) {
r->neg().intersect(m, r->pos());
result.push_back(r.detach());
}
}
@ -566,7 +565,7 @@ std::ostream& doc_manager::display(std::ostream& out, doc const& b, unsigned hi,
}
void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst) {
void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst) {
expr_ref fml1 = to_formula(m, src);
expr_ref fml2 = dstm.to_formula(m, dst);
project_rename(fml2, to_delete);
@ -603,11 +602,11 @@ expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
return result;
}
void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) {
ast_manager& m = fml.get_manager();
expr_ref tmp1(m), tmp2(m);
for (unsigned i = 0; i < num_tbits(); ++i) {
if (to_delete[i]) {
if (to_delete.get(i)) {
expr_safe_replace rep1(m), rep2(m);
rep1.insert(tbvm().mk_var(m, i), m.mk_true());
rep1(fml, tmp1);
@ -623,11 +622,11 @@ void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
}
}
void doc_manager::project_rename(expr_ref& fml, bool const* to_delete) {
void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) {
ast_manager& m = fml.get_manager();
expr_safe_replace rep(m);
for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
if (!to_delete[i]) {
if (!to_delete.get(i)) {
rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
++j;
}

17
src/muz/rel/doc.h
View file

@ -48,7 +48,7 @@ class doc_manager {
project_resolve
};
project_action_t pick_resolvent(
tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx);
tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx);
public:
doc_manager(unsigned num_bits);
~doc_manager();
@ -88,17 +88,17 @@ public:
std::ostream& display(std::ostream& out, doc const& b) const;
std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const;
unsigned num_tbits() const { return m.num_tbits(); }
doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src);
doc* project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src);
bool well_formed(doc const& d) const;
bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
void set(doc& d, unsigned idx, tbit value);
void verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst);
void verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst);
private:
unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols);
void project_rename(expr_ref& fml, bool const* to_delete);
void project_expand(expr_ref& fml, bool const* to_delete);
void project_rename(expr_ref& fml, bit_vector const& to_delete);
void project_expand(expr_ref& fml, bit_vector const& to_delete);
expr_ref to_formula(ast_manager& m, doc const& src);
void check_equiv(ast_manager& m, expr* fml1, expr* fml2);
};
@ -171,11 +171,13 @@ public:
SASSERT(t);
unsigned sz = size(), j = 0;
bool found = false;
for (unsigned i = 0; i < sz; ++i, ++j) {
unsigned i = 0;
for ( ; i < sz; ++i, ++j) {
if (m.contains(*m_elems[i], *t)) {
found = true;
break;
}
if (!found && m.contains(*t, *m_elems[i])) {
if (m.contains(*t, *m_elems[i])) {
m.deallocate(m_elems[i]);
--j;
}
@ -185,6 +187,7 @@ public:
}
if (j != sz) m_elems.resize(j);
if (found) {
SASSERT(j == i);
m.deallocate(t);
}
else {

4
src/muz/rel/tbv.cpp
View file

@ -99,11 +99,11 @@ tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
}
return r;
}
tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
tbv* tbv_manager::project(unsigned n, bit_vector const& to_delete, tbv const& src) {
tbv* r = allocate();
unsigned i, j;
for (i = 0, j = 0; i < n; ++i) {
if (!to_delete[i]) {
if (!to_delete.get(i)) {
set(*r, j, src[i]);
++j;
}

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

@ -76,7 +76,7 @@ public:
bool intersect(tbv const& a, tbv const& b, tbv& result);
std::ostream& display(std::ostream& out, tbv const& b) const;
std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const;
tbv* project(unsigned n, bool const* to_delete, tbv const& src);
tbv* project(unsigned n, bit_vector const& to_delete, tbv const& src);
bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
void set(tbv& dst, uint64 n, unsigned hi, unsigned lo);
void set(tbv& dst, rational const& r, unsigned hi, unsigned lo);

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

@ -54,9 +54,6 @@ Notes:
return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN)
We have most of the facilities required for a join project operation.
For example, the filter_project function uses both equalities and deleted columns.
- Lipstick service:
- filter_proj_fn uses both a bit_vector and a svector<bool> for representing removed bits.
This is due to underlying routines using different types for the same purpose.
--*/
#include "udoc_relation.h"
#include "dl_relation_manager.h"
@ -473,7 +470,7 @@ namespace datalog {
}
class udoc_plugin::project_fn : public convenient_relation_project_fn {
svector<bool> m_to_delete;
bit_vector m_to_delete;
public:
project_fn(udoc_relation const & t, unsigned removed_col_cnt, const unsigned * removed_cols)
: convenient_relation_project_fn(t.get_signature(), removed_col_cnt, removed_cols) {
@ -481,7 +478,7 @@ namespace datalog {
unsigned n = t.get_dm().num_tbits();
m_to_delete.resize(n, false);
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_to_delete[m_removed_cols[i]] = true;
m_to_delete.set(m_removed_cols[i], true);
}
}
@ -496,7 +493,7 @@ namespace datalog {
udoc const& ud1 = t.get_udoc();
udoc& ud2 = r->get_udoc();
for (unsigned i = 0; i < ud1.size(); ++i) {
d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), ud1[i]);
d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete, ud1[i]);
ud2.push_back(d2.detach());
}
TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';);
@ -1198,8 +1195,7 @@ namespace datalog {
expr_ref m_reduced_condition;
udoc m_udoc;
udoc m_udoc2;
bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed)
svector<bool> m_to_delete; // same
bit_vector m_to_delete; // map: col idx -> bool (whether the column is to be removed)
subset_ints m_equalities;
unsigned_vector m_roots;
@ -1213,19 +1209,17 @@ namespace datalog {
m_equalities(union_ctx) {
unsigned num_bits = t.get_num_bits();
t.expand_column_vector(m_removed_cols);
m_col_list.resize(num_bits, false);
m_to_delete.resize(num_bits, false);
for (unsigned i = 0; i < num_bits; ++i) {
m_equalities.mk_var();
}
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_col_list.set(m_removed_cols[i], true);
m_to_delete[m_removed_cols[i]] = true;
m_to_delete.set(m_removed_cols[i], true);
}
expr_ref guard(m), non_eq_cond(condition, m);
t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots);
t.extract_guard(non_eq_cond, guard, m_reduced_condition);
t.compile_guard(guard, m_udoc, m_col_list);
t.compile_guard(guard, m_udoc, m_to_delete);
}
virtual ~filter_proj_fn() {
@ -1238,13 +1232,13 @@ namespace datalog {
ast_manager& m = m_reduced_condition.get_manager();
m_udoc2.copy(dm, u1);
m_udoc2.intersect(dm, m_udoc);
t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_col_list);
m_udoc2.merge(dm, m_roots, m_equalities, m_col_list);
t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_to_delete);
m_udoc2.merge(dm, m_roots, m_equalities, m_to_delete);
SASSERT(m_udoc2.well_formed(dm));
udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
doc_manager& dm2 = r->get_dm();
for (unsigned i = 0; i < m_udoc2.size(); ++i) {
doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), m_udoc2[i]);
doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete, m_udoc2[i]);
r->get_udoc().insert(dm2, d);
SASSERT(r->get_udoc().well_formed(dm2));
}