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: fix fast path of filter_negated

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2014-10-01 18:03:59 +01:00
parent 5211e9aa1a
commit 04b5d436b3
6 changed files with 76 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -536,16 +536,15 @@ bool doc_manager::contains(doc const& a, doc const& b) const {
return true;
}
bool doc_manager::contains(
unsigned offset_a, doc const& a,
doc_manager const& dm_b,
unsigned offset_b, doc const& b,
unsigned length) const {
if (!m.contains(offset_a, a.pos(), dm_b.tbvm(), offset_b, b.pos(), length)) return false;
bool doc_manager::contains(doc const& a, unsigned_vector const& colsa,
doc const& b, unsigned_vector const& colsb) const {
if (!m.contains(a.pos(), colsa, b.pos(), colsb))
return false;
for (unsigned i = 0; i < a.neg().size(); ++i) {
bool found = false;
for (unsigned j = 0; !found && j < b.neg().size(); ++j) {
found = dm_b.tbvm().contains(offset_b, b.neg()[j], tbvm(), offset_a, a.neg()[i], length);
found = m.contains(b.neg()[j], colsb, a.neg()[i], colsa);
}
if (!found) return false;
}

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

@ -82,9 +82,8 @@ public:
bool equals(doc const& a, doc const& b) const;
unsigned hash(doc const& src) const;
bool contains(doc const& a, doc const& b) const;
bool contains(unsigned offset_a, doc const& a,
doc_manager const& dm_b, unsigned offset_b, doc const& b,
unsigned length) const;
bool contains(doc const& a, unsigned_vector const& colsa,
doc const& b, unsigned_vector const& colsb) const;
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(); }

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

@ -245,18 +245,12 @@ bool tbv_manager::contains(tbv const& a, tbv const& b) const {
return m.contains(a, b);
}
bool tbv_manager::contains(unsigned offset_a, tbv const& a,
tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
unsigned length) const {
if (this == &dm_b && length == num_tbits()) {
SASSERT(offset_a == 0);
SASSERT(offset_b == 0);
return m.contains(a, b);
}
for (unsigned i = 0; i < length; ++i) {
tbit bit_a = a[offset_a + i];
bool tbv_manager::contains(tbv const& a, unsigned_vector const& colsa,
tbv const& b, unsigned_vector const& colsb) const {
for (unsigned i = 0; i < colsa.size(); ++i) {
tbit bit_a = a[colsa[i]];
if (bit_a == BIT_x) continue;
if (bit_a != b[offset_b + i]) return false;
if (bit_a != b[colsb[i]]) return false;
}
return true;
}

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

@ -70,9 +70,8 @@ public:
bool equals(tbv const& a, tbv const& b) const;
unsigned hash(tbv const& src) const;
bool contains(tbv const& a, tbv const& b) const;
bool contains(unsigned offset_a, tbv const& a,
tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
unsigned length) const;
bool contains(tbv const& a, unsigned_vector const& colsa,
tbv const& b, unsigned_vector const& colsb) const;
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;

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

@ -1064,14 +1064,16 @@ namespace datalog {
// 4. Unit/stress test cases are needed.
//
class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn {
const unsigned_vector m_t_cols;
const unsigned_vector m_neg_cols;
unsigned_vector m_t_cols;
unsigned_vector m_neg_cols;
public:
negation_filter_fn(const udoc_relation & r, const udoc_relation & neg, unsigned joined_col_cnt,
const unsigned *t_cols, const unsigned *neg_cols)
: m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols) {
SASSERT(joined_col_cnt > 0);
r.expand_column_vector(m_t_cols);
neg.expand_column_vector(m_neg_cols);
}
virtual void operator()(relation_base& tb, const relation_base& negb) {
@ -1086,30 +1088,16 @@ namespace datalog {
udoc result;
for (unsigned i = 0; i < dst.size(); ++i) {
bool subsumed = false;
for (unsigned j = 0; j < neg.size(); ++j) {
for (unsigned c = 0; c < m_t_cols.size(); ++c) {
unsigned t_col = m_t_cols[c];
unsigned n_col = m_neg_cols[c];
unsigned num_bits = t.column_num_bits(t_col);
SASSERT(num_bits == n.column_num_bits(n_col));
unsigned t_idx = t.column_idx(t_col);
unsigned n_idx = n.column_idx(n_col);
bool cont = dmn.contains(n_idx, neg[j], dmt, t_idx, dst[i], num_bits);
IF_VERBOSE(
3,
dmt.display(verbose_stream() << "dst:", dst[i], t_idx+num_bits-1,t_idx) << "\n";
dmn.display(verbose_stream() << "neg:", neg[j], n_idx+num_bits-1,n_idx) << "\n";
verbose_stream() << "contains: " << (cont?"true":"false") << "\n";);
if (!cont) {
goto next_neg_disj;
}
if (dmn.contains(neg[j], m_neg_cols, dst[i], m_t_cols)) {
dmt.deallocate(&dst[i]);
subsumed = true;
break;
}
dmt.deallocate(&dst[i]);
goto next_disj;
next_neg_disj:;
}
result.push_back(&dst[i]);
next_disj:;
if (!subsumed)
result.push_back(&dst[i]);
}
std::swap(dst, result);
if (dst.is_empty()) {

50
src/test/udoc_relation.cpp
View file

@ -148,6 +148,7 @@ public:
test_rename();
test_filter_neg();
test_filter_neg2();
// empty
@ -551,6 +552,55 @@ public:
t2->deallocate();
}
void test_filter_neg2() {
// filter_by_negation
relation_signature sig4;
sig4.push_back(bv.mk_sort(1));
sig4.push_back(bv.mk_sort(1));
sig4.push_back(bv.mk_sort(1));
unsigned_vector cols, allcols;
cols.push_back(0);
cols.push_back(2);
allcols.push_back(0);
allcols.push_back(1);
allcols.push_back(2);
/// xxx \ 1x0
udoc_relation* t1 = mk_full(sig4);
{
udoc_relation* neg = mk_full(sig4);
doc& n = neg->get_udoc()[0];
neg->get_dm().set(n, 0, BIT_1);
neg->get_dm().set(n, 2, BIT_0);
apply_filter_neg(*t1, *neg, allcols, allcols);
neg->deallocate();
}
/// xxx \ (1x1 u 0x0)
udoc_relation* t2 = mk_full(sig4);
{
udoc_relation* neg = mk_full(sig4);
doc& n = neg->get_udoc()[0];
neg->get_dm().set(n, 0, BIT_0);
neg->get_dm().set(n, 2, BIT_0);
apply_filter_neg(*t2, *neg, allcols, allcols);
neg->deallocate();
}
{
udoc_relation* neg = mk_full(sig4);
doc& n = neg->get_udoc()[0];
neg->get_dm().set(n, 0, BIT_1);
neg->get_dm().set(n, 2, BIT_1);
apply_filter_neg(*t2, *neg, allcols, allcols);
neg->deallocate();
}
apply_filter_neg(*t2, *t1, cols, cols);
t1->deallocate();
t2->deallocate();
}
void set_random(udoc_relation& r, unsigned num_vals) {
unsigned num_bits = r.get_dm().num_tbits();
udoc_relation* full = mk_full(r.get_signature());