mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 09:55:19 +00:00
remove buggy and unused equivalence relation plugin. Github issue #770
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
ff75f88c4f
commit
fa1a0aa7ba
|
|
@ -12,7 +12,6 @@ z3_add_component(rel
|
||||||
dl_interval_relation.cpp
|
dl_interval_relation.cpp
|
||||||
dl_lazy_table.cpp
|
dl_lazy_table.cpp
|
||||||
dl_mk_explanations.cpp
|
dl_mk_explanations.cpp
|
||||||
dl_mk_partial_equiv.cpp
|
|
||||||
dl_mk_similarity_compressor.cpp
|
dl_mk_similarity_compressor.cpp
|
||||||
dl_mk_simple_joins.cpp
|
dl_mk_simple_joins.cpp
|
||||||
dl_product_relation.cpp
|
dl_product_relation.cpp
|
||||||
|
|
|
||||||
|
|
@ -1,155 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2012 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
dl_mk_partial_equiv.cpp
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Rule transformer which identifies predicates that are partial equivalence relations.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2012-05-14
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
#include "dl_mk_partial_equiv.h"
|
|
||||||
#include "dl_relation_manager.h"
|
|
||||||
#include "ast_pp.h"
|
|
||||||
|
|
||||||
namespace datalog {
|
|
||||||
|
|
||||||
bool mk_partial_equivalence_transformer::is_symmetry(rule const* r) {
|
|
||||||
func_decl* p = r->get_decl();
|
|
||||||
return
|
|
||||||
p->get_arity() == 2 &&
|
|
||||||
p->get_domain(0) == p->get_domain(1) &&
|
|
||||||
r->get_tail_size() == 1 &&
|
|
||||||
r->get_tail(0)->get_decl() == p &&
|
|
||||||
r->get_head()->get_arg(0) == r->get_tail(0)->get_arg(1) &&
|
|
||||||
r->get_head()->get_arg(1) == r->get_tail(0)->get_arg(0) &&
|
|
||||||
is_var(r->get_head()->get_arg(0)) &&
|
|
||||||
is_var(r->get_head()->get_arg(1)) &&
|
|
||||||
r->get_head()->get_arg(0) != r->get_head()->get_arg(1);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
bool mk_partial_equivalence_transformer::is_transitivity(rule const* r) {
|
|
||||||
func_decl* p = r->get_decl();
|
|
||||||
if (p->get_arity() != 2 ||
|
|
||||||
p->get_domain(0) != p->get_domain(1) ||
|
|
||||||
r->get_tail_size() != 2 ||
|
|
||||||
r->get_tail(0)->get_decl() != p ||
|
|
||||||
r->get_tail(1)->get_decl() != p) {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
app* h = r->get_head();
|
|
||||||
app* a = r->get_tail(0);
|
|
||||||
app* b = r->get_tail(1);
|
|
||||||
expr* x1 = h->get_arg(0);
|
|
||||||
expr* x2 = h->get_arg(1);
|
|
||||||
expr* a1 = a->get_arg(0);
|
|
||||||
expr* a2 = a->get_arg(1);
|
|
||||||
expr* b1 = b->get_arg(0);
|
|
||||||
expr* b2 = b->get_arg(1);
|
|
||||||
|
|
||||||
if (!(is_var(x1) && is_var(x2) && is_var(a1) && is_var(a2) && is_var(b1) && is_var(b2))) {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
if (x1 == x2 || a1 == a2 || b1 == b2) {
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
if (a2 == b1) {
|
|
||||||
if (x1 == b2 && x2 == a1) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
if (x1 == a1 && x2 == b2) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
if (a1 == b2) {
|
|
||||||
if (x1 == b1 && x2 == a2) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
if (x1 == a2 && x2 == b1) {
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
return false;
|
|
||||||
}
|
|
||||||
|
|
||||||
return false;
|
|
||||||
;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source) {
|
|
||||||
// TODO mc
|
|
||||||
|
|
||||||
if (source.get_num_rules() == 0) {
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (m_context.get_engine() != DATALOG_ENGINE) {
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
relation_manager & rm = m_context.get_rel_context()->get_rmanager();
|
|
||||||
rule_set::decl2rules::iterator it = source.begin_grouped_rules();
|
|
||||||
rule_set::decl2rules::iterator end = source.end_grouped_rules();
|
|
||||||
|
|
||||||
rule_set* res = alloc(rule_set, m_context);
|
|
||||||
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
func_decl* p = it->m_key;
|
|
||||||
rule_vector const& rv = *(it->m_value);
|
|
||||||
bool has_symmetry = false;
|
|
||||||
bool has_transitivity = false;
|
|
||||||
unsigned i_symmetry = 0, i_transitivity = 0;
|
|
||||||
family_id kind = rm.get_requested_predicate_kind(p);
|
|
||||||
for (unsigned i = 0; i < rv.size(); ++i) {
|
|
||||||
|
|
||||||
if (kind != null_family_id) {
|
|
||||||
res->add_rule(rv[i]);
|
|
||||||
}
|
|
||||||
else if (is_symmetry(rv[i])) {
|
|
||||||
i_symmetry = i;
|
|
||||||
has_symmetry = true;
|
|
||||||
}
|
|
||||||
else if (is_transitivity(rv[i])) {
|
|
||||||
i_transitivity = i;
|
|
||||||
has_transitivity = true;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
res->add_rule(rv[i]);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (has_symmetry && !has_transitivity) {
|
|
||||||
res->add_rule(rv[i_symmetry]);
|
|
||||||
}
|
|
||||||
else if (!has_symmetry && has_transitivity) {
|
|
||||||
res->add_rule(rv[i_transitivity]);
|
|
||||||
}
|
|
||||||
else if (has_symmetry && has_transitivity) {
|
|
||||||
TRACE("dl", tout << "updating predicate " << mk_pp(p, m) << " to partial equivalence\n";);
|
|
||||||
SASSERT(kind == null_family_id);
|
|
||||||
rm.set_predicate_kind(p, rm.get_table_plugin(symbol("equivalence"))->get_kind());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (res->get_num_rules() == source.get_num_rules()) {
|
|
||||||
dealloc(res);
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
res->inherit_predicates(source);
|
|
||||||
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -1,50 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2012 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
dl_mk_partial_equiv.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
Rule transformer which identifies predicates that are partial equivalence relations.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Nikolaj Bjorner (nbjorner) 2012-05-14
|
|
||||||
|
|
||||||
Revision History:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
|
|
||||||
|
|
||||||
#ifndef DL_MK_PARTIAL_EQUIVALENCE_TRANSFORMER_H_
|
|
||||||
#define DL_MK_PARTIAL_EQUIVALENCE_TRANSFORMER_H_
|
|
||||||
|
|
||||||
#include "dl_context.h"
|
|
||||||
#include "dl_rule_transformer.h"
|
|
||||||
|
|
||||||
namespace datalog {
|
|
||||||
|
|
||||||
class mk_partial_equivalence_transformer : public rule_transformer::plugin {
|
|
||||||
ast_manager & m;
|
|
||||||
context & m_context;
|
|
||||||
public:
|
|
||||||
mk_partial_equivalence_transformer(context & ctx, unsigned priority=30000)
|
|
||||||
: plugin(priority),
|
|
||||||
m(ctx.get_manager()),
|
|
||||||
m_context(ctx) {}
|
|
||||||
|
|
||||||
rule_set * operator()(rule_set const & source);
|
|
||||||
|
|
||||||
private:
|
|
||||||
|
|
||||||
bool is_symmetry(rule const* r);
|
|
||||||
bool is_transitivity(rule const* r);
|
|
||||||
};
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
#endif /* DL_MK_PARTIAL_EQUIV_TRANSFORMER_H_ */
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -292,482 +292,5 @@ namespace datalog {
|
||||||
table_base::iterator bitvector_table::end() const {
|
table_base::iterator bitvector_table::end() const {
|
||||||
return mk_iterator(alloc(bv_iterator, *this, true));
|
return mk_iterator(alloc(bv_iterator, *this, true));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// -----------------------------------
|
|
||||||
//
|
|
||||||
// equivalence_table
|
|
||||||
//
|
|
||||||
// -----------------------------------
|
|
||||||
|
|
||||||
bool equivalence_table_plugin::can_handle_signature(const table_signature & sig) {
|
|
||||||
return sig.functional_columns() == 0 && sig.size() == 2 && sig[0] < UINT_MAX && sig[0] == sig[1];
|
|
||||||
}
|
|
||||||
|
|
||||||
bool equivalence_table_plugin::is_equivalence_table(table_base const& tbl) const {
|
|
||||||
if (tbl.get_kind() != get_kind()) return false;
|
|
||||||
equivalence_table const& t = static_cast<equivalence_table const&>(tbl);
|
|
||||||
return !t.is_sparse();
|
|
||||||
}
|
|
||||||
|
|
||||||
table_base * equivalence_table_plugin::mk_empty(const table_signature & s) {
|
|
||||||
TRACE("dl", for (unsigned i = 0; i < s.size(); ++i) tout << s[i] << " "; tout << "\n";);
|
|
||||||
SASSERT(can_handle_signature(s));
|
|
||||||
return alloc(equivalence_table, *this, s);
|
|
||||||
}
|
|
||||||
|
|
||||||
class equivalence_table_plugin::select_equal_and_project_fn : public table_transformer_fn {
|
|
||||||
unsigned m_val;
|
|
||||||
table_sort m_sort;
|
|
||||||
public:
|
|
||||||
select_equal_and_project_fn(const table_signature & sig, table_element val, unsigned col)
|
|
||||||
: m_val(static_cast<unsigned>(val)),
|
|
||||||
m_sort(sig[0]) {
|
|
||||||
SASSERT(val <= UINT_MAX);
|
|
||||||
SASSERT(col == 0 || col == 1);
|
|
||||||
SASSERT(sig.functional_columns() == 0);
|
|
||||||
SASSERT(sig.size() == 2);
|
|
||||||
SASSERT(sig[0] < UINT_MAX && sig[0] == sig[1]);
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual table_base* operator()(const table_base& tb) {
|
|
||||||
TRACE("dl", tout << "\n";);
|
|
||||||
table_plugin & plugin = tb.get_plugin();
|
|
||||||
table_plugin* rp = plugin.get_manager().get_table_plugin(symbol("sparse"));
|
|
||||||
SASSERT(rp);
|
|
||||||
table_signature sig;
|
|
||||||
sig.push_back(m_sort);
|
|
||||||
table_base* result = rp->mk_empty(sig);
|
|
||||||
equivalence_table const& eq_table = static_cast<equivalence_table const&>(tb);
|
|
||||||
if (eq_table.is_valid(m_val)) {
|
|
||||||
table_fact fact;
|
|
||||||
fact.resize(1);
|
|
||||||
unsigned r = m_val;
|
|
||||||
do {
|
|
||||||
fact[0] = r;
|
|
||||||
result->add_fact(fact);
|
|
||||||
r = eq_table.m_uf.next(r);
|
|
||||||
}
|
|
||||||
while (r != m_val);
|
|
||||||
}
|
|
||||||
TRACE("dl", tb.display(tout << "src:\n"); result->display(tout << "result\n"););
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
table_transformer_fn * equivalence_table_plugin::mk_select_equal_and_project_fn(
|
|
||||||
const table_base & t, const table_element & value, unsigned col) {
|
|
||||||
return alloc(select_equal_and_project_fn, t.get_signature(), value, col);
|
|
||||||
}
|
|
||||||
|
|
||||||
class equivalence_table_plugin::union_fn : public table_union_fn {
|
|
||||||
|
|
||||||
equivalence_table_plugin& m_plugin;
|
|
||||||
|
|
||||||
|
|
||||||
void mk_union1(equivalence_table & tgt, const equivalence_table & src, table_base * delta) {
|
|
||||||
unsigned num_vars = src.m_uf.get_num_vars();
|
|
||||||
table_fact fact;
|
|
||||||
fact.resize(2);
|
|
||||||
for (unsigned i = 0; i < num_vars; ++i) {
|
|
||||||
if (src.is_valid(i) && src.m_uf.find(i) == i) {
|
|
||||||
fact[0] = i;
|
|
||||||
equivalence_table::class_iterator it = src.class_begin(i);
|
|
||||||
equivalence_table::class_iterator end = src.class_end(i);
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
fact[1] = *it;
|
|
||||||
if (!tgt.contains_fact(fact)) {
|
|
||||||
tgt.add_fact(fact);
|
|
||||||
if (delta) {
|
|
||||||
delta->add_fact(fact);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void mk_union2(equivalence_table & tgt, const table_base & src, table_base * delta) {
|
|
||||||
table_fact fact;
|
|
||||||
table_base::iterator it = src.begin(), end = src.end();
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
it->get_fact(fact);
|
|
||||||
if (!tgt.contains_fact(fact)) {
|
|
||||||
tgt.add_fact(fact);
|
|
||||||
if (delta) {
|
|
||||||
delta->add_fact(fact);
|
|
||||||
TRACE("dl",
|
|
||||||
tout << "Add: ";
|
|
||||||
for (unsigned i = 0; i < fact.size(); ++i) tout << fact[i] << " ";
|
|
||||||
tout << "\n";);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
public:
|
|
||||||
union_fn(equivalence_table_plugin& p) : m_plugin(p) {}
|
|
||||||
|
|
||||||
virtual void operator()(table_base & tgt0, const table_base & src, table_base * delta) {
|
|
||||||
TRACE("dl", tout << "union\n";);
|
|
||||||
equivalence_table & tgt = static_cast<equivalence_table &>(tgt0);
|
|
||||||
if (m_plugin.is_equivalence_table(src)) {
|
|
||||||
mk_union1(tgt, static_cast<equivalence_table const&>(src), delta);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
mk_union2(tgt, src, delta);
|
|
||||||
}
|
|
||||||
TRACE("dl", src.display(tout << "src\n"); tgt.display(tout << "tgt\n");
|
|
||||||
if (delta) delta->display(tout << "delta\n"););
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
table_union_fn * equivalence_table_plugin::mk_union_fn(
|
|
||||||
const table_base & tgt, const table_base & src, const table_base * delta) {
|
|
||||||
if (!is_equivalence_table(tgt) ||
|
|
||||||
tgt.get_signature() != src.get_signature() ||
|
|
||||||
(delta && delta->get_signature() != tgt.get_signature())) {
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
return alloc(union_fn,*this);
|
|
||||||
}
|
|
||||||
|
|
||||||
class equivalence_table_plugin::join_project_fn : public convenient_table_join_project_fn {
|
|
||||||
equivalence_table_plugin& m_plugin;
|
|
||||||
public:
|
|
||||||
join_project_fn(
|
|
||||||
equivalence_table_plugin& plugin, const table_signature & t1_sig, const table_signature & t2_sig, unsigned col_cnt,
|
|
||||||
const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt,
|
|
||||||
const unsigned * removed_cols)
|
|
||||||
: convenient_table_join_project_fn(t1_sig, t2_sig, col_cnt, cols1, cols2, removed_col_cnt, removed_cols),
|
|
||||||
m_plugin(plugin) {
|
|
||||||
m_removed_cols.push_back(UINT_MAX);
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual table_base * operator()(const table_base & tb1, const table_base & tb2) {
|
|
||||||
SASSERT(m_cols1.size() == 1);
|
|
||||||
const table_signature & res_sign = get_result_signature();
|
|
||||||
table_plugin * plugin = &tb1.get_plugin();
|
|
||||||
if (!plugin->can_handle_signature(res_sign)) {
|
|
||||||
plugin = &tb2.get_plugin();
|
|
||||||
if (!plugin->can_handle_signature(res_sign)) {
|
|
||||||
plugin = &tb1.get_manager().get_appropriate_plugin(res_sign);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
SASSERT(plugin->can_handle_signature(res_sign));
|
|
||||||
table_base * result = plugin->mk_empty(res_sign);
|
|
||||||
|
|
||||||
if (m_plugin.is_equivalence_table(tb1)) {
|
|
||||||
mk_join(0, m_cols1[0], static_cast<const equivalence_table&>(tb1),
|
|
||||||
2, m_cols2[0], tb2, result);
|
|
||||||
}
|
|
||||||
else if (m_plugin.is_equivalence_table(tb2)) {
|
|
||||||
mk_join(tb1.get_signature().size(), m_cols2[0], static_cast<const equivalence_table&>(tb2),
|
|
||||||
0, m_cols1[0], tb1, result);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
UNREACHABLE();
|
|
||||||
}
|
|
||||||
TRACE("dl", tb1.display(tout << "tb1\n"); tb2.display(tout << "tb2\n"); result->display(tout << "result\n"););
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
|
|
||||||
private:
|
|
||||||
table_base * mk_join(unsigned offs1, unsigned col1, equivalence_table const & t1,
|
|
||||||
unsigned offs2, unsigned col2, table_base const& t2, table_base* res) {
|
|
||||||
table_base::iterator els2it = t2.begin();
|
|
||||||
table_base::iterator els2end = t2.end();
|
|
||||||
|
|
||||||
table_fact acc, proj;
|
|
||||||
acc.resize(t1.get_signature().size() + t2.get_signature().size());
|
|
||||||
|
|
||||||
for(; els2it != els2end; ++els2it) {
|
|
||||||
const table_base::row_interface & row2 = *els2it;
|
|
||||||
table_element const& e2 = row2[col2];
|
|
||||||
equivalence_table::class_iterator it = t1.class_begin(e2);
|
|
||||||
equivalence_table::class_iterator end = t1.class_end(e2);
|
|
||||||
if (it != end) {
|
|
||||||
for (unsigned i = 0; i < row2.size(); ++i) {
|
|
||||||
acc[i+offs2] = row2[i];
|
|
||||||
}
|
|
||||||
}
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
acc[offs1+col1] = e2;
|
|
||||||
acc[offs1+1-col1] = *it;
|
|
||||||
mk_project(acc, proj);
|
|
||||||
TRACE("dl", for (unsigned i = 0; i < proj.size(); ++i) tout << proj[i] << " "; tout << "\n";);
|
|
||||||
res->add_fact(proj);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return res;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual void mk_project(table_fact const & f, table_fact & p) const {
|
|
||||||
unsigned sz = f.size();
|
|
||||||
p.reset();
|
|
||||||
for (unsigned i = 0, r = 0; i < sz; ++i) {
|
|
||||||
if (r < m_removed_cols.size() && m_removed_cols[r] == i) {
|
|
||||||
++r;
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
p.push_back(f[i]);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
table_join_fn * equivalence_table_plugin::mk_join_project_fn(
|
|
||||||
const table_base & t1, const table_base & t2,
|
|
||||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt,
|
|
||||||
const unsigned * removed_cols) {
|
|
||||||
if (col_cnt != 1) {
|
|
||||||
TRACE("dl", tout << "WARNING: join_project on multiple columns is not implemented\n";);
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
if (is_equivalence_table(t1) || is_equivalence_table(t2)) {
|
|
||||||
return alloc(join_project_fn, *this, t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2,
|
|
||||||
removed_col_cnt, removed_cols);
|
|
||||||
}
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
class equivalence_table::eq_iterator : public iterator_core {
|
|
||||||
|
|
||||||
equivalence_table const& m_eq;
|
|
||||||
unsigned m_last;
|
|
||||||
unsigned m_current;
|
|
||||||
unsigned m_next;
|
|
||||||
|
|
||||||
class our_row : public caching_row_interface {
|
|
||||||
const eq_iterator& m_parent;
|
|
||||||
public:
|
|
||||||
our_row(const eq_iterator & p) : caching_row_interface(p.m_eq), m_parent(p) {}
|
|
||||||
|
|
||||||
virtual void get_fact(table_fact& result) const {
|
|
||||||
if (result.size() < size()) {
|
|
||||||
result.resize(size(), 0);
|
|
||||||
}
|
|
||||||
result[0] = m_parent.m_current;
|
|
||||||
result[1] = m_parent.m_next;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual table_element operator[](unsigned col) const {
|
|
||||||
if (col == 0) return m_parent.m_current;
|
|
||||||
if (col == 1) return m_parent.m_next;
|
|
||||||
UNREACHABLE();
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
};
|
|
||||||
our_row m_row_obj;
|
|
||||||
|
|
||||||
public:
|
|
||||||
eq_iterator(const equivalence_table& eq, bool end):
|
|
||||||
m_eq(eq),
|
|
||||||
m_last(eq.m_uf.get_num_vars()),
|
|
||||||
m_current(end?m_last:0),
|
|
||||||
m_next(0),
|
|
||||||
m_row_obj(*this)
|
|
||||||
{
|
|
||||||
while (m_current < m_last && !m_eq.is_valid(m_current)) {
|
|
||||||
m_current++;
|
|
||||||
m_next = m_current;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual bool is_finished() const {
|
|
||||||
return m_current == m_last;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual row_interface & operator*() {
|
|
||||||
SASSERT(!is_finished());
|
|
||||||
return m_row_obj;
|
|
||||||
}
|
|
||||||
|
|
||||||
virtual void operator++() {
|
|
||||||
SASSERT(!is_finished());
|
|
||||||
m_next = m_eq.m_uf.next(m_next);
|
|
||||||
if (m_next == m_current) {
|
|
||||||
do {
|
|
||||||
m_current++;
|
|
||||||
m_next = m_current;
|
|
||||||
}
|
|
||||||
while (m_current < m_last && !m_eq.is_valid(m_current));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
equivalence_table::equivalence_table(equivalence_table_plugin & plugin, const table_signature & sig)
|
|
||||||
: table_base(plugin, sig), m_uf(m_ctx), m_sparse(0) {
|
|
||||||
SASSERT(plugin.can_handle_signature(sig));
|
|
||||||
}
|
|
||||||
|
|
||||||
equivalence_table::~equivalence_table() {
|
|
||||||
if (is_sparse()) {
|
|
||||||
m_sparse->deallocate();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void equivalence_table::add_fact(const table_fact & f) {
|
|
||||||
if (is_sparse()) {
|
|
||||||
add_fact_sparse(f);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
TRACE("dl_verbose", for (unsigned i = 0; i < f.size(); ++i) tout << f[i] << " "; tout << "\n";);
|
|
||||||
while (first(f) >= m_uf.get_num_vars()) m_uf.mk_var();
|
|
||||||
while (second(f) >= m_uf.get_num_vars()) m_uf.mk_var();
|
|
||||||
m_uf.merge(first(f), second(f));
|
|
||||||
m_valid.reserve(m_uf.get_num_vars());
|
|
||||||
m_valid.set(first(f));
|
|
||||||
m_valid.set(second(f));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void equivalence_table::remove_fact(const table_element* fact) {
|
|
||||||
mk_sparse();
|
|
||||||
m_sparse->remove_fact(fact);
|
|
||||||
}
|
|
||||||
|
|
||||||
void equivalence_table::mk_sparse() {
|
|
||||||
if (m_sparse) return;
|
|
||||||
|
|
||||||
TRACE("dl",tout << "\n";);
|
|
||||||
table_plugin & plugin = get_plugin();
|
|
||||||
table_plugin* rp = plugin.get_manager().get_table_plugin(symbol("sparse"));
|
|
||||||
SASSERT(rp);
|
|
||||||
table_base* result = rp->mk_empty(get_signature());
|
|
||||||
table_base::iterator it = begin(), e = end();
|
|
||||||
table_fact fact;
|
|
||||||
for (; it != e; ++it) {
|
|
||||||
it->get_fact(fact);
|
|
||||||
result->add_fact(fact);
|
|
||||||
}
|
|
||||||
m_sparse = result;
|
|
||||||
}
|
|
||||||
|
|
||||||
void equivalence_table::add_fact_sparse(table_fact const& f) {
|
|
||||||
table_base::iterator it = m_sparse->begin(), end = m_sparse->end();
|
|
||||||
vector<table_fact> to_add;
|
|
||||||
to_add.push_back(f);
|
|
||||||
table_fact f1(f);
|
|
||||||
|
|
||||||
f1[0] = f[1];
|
|
||||||
f1[1] = f[0];
|
|
||||||
to_add.push_back(f1);
|
|
||||||
|
|
||||||
f1[0] = f[1];
|
|
||||||
f1[1] = f[1];
|
|
||||||
to_add.push_back(f1);
|
|
||||||
|
|
||||||
f1[0] = f[0];
|
|
||||||
f1[1] = f[0];
|
|
||||||
to_add.push_back(f1);
|
|
||||||
|
|
||||||
for (; it != end; ++it) {
|
|
||||||
if ((*it)[0] == f[0]) {
|
|
||||||
f1[0] = f[1];
|
|
||||||
f1[1] = (*it)[1];
|
|
||||||
to_add.push_back(f1);
|
|
||||||
std::swap(f1[0],f1[1]);
|
|
||||||
to_add.push_back(f1);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < to_add.size(); ++i) {
|
|
||||||
m_sparse->add_fact(to_add[i]);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
bool equivalence_table::contains_fact(const table_fact & f) const {
|
|
||||||
TRACE("dl_verbose", for (unsigned i = 0; i < f.size(); ++i) tout << f[i] << " "; tout << "\n";);
|
|
||||||
if (is_sparse()) {
|
|
||||||
return m_sparse->contains_fact(f);
|
|
||||||
}
|
|
||||||
return
|
|
||||||
is_valid(first(f)) &&
|
|
||||||
is_valid(second(f)) &&
|
|
||||||
m_uf.find(first(f)) == m_uf.find(second(f));
|
|
||||||
}
|
|
||||||
|
|
||||||
table_base* equivalence_table::clone() const {
|
|
||||||
if (is_sparse()) {
|
|
||||||
return m_sparse->clone();
|
|
||||||
}
|
|
||||||
TRACE("dl",tout << "\n";);
|
|
||||||
table_plugin & plugin = get_plugin();
|
|
||||||
table_base* result = plugin.mk_empty(get_signature());
|
|
||||||
table_fact fact;
|
|
||||||
fact.resize(2);
|
|
||||||
for (unsigned i = 0; i < m_uf.get_num_vars(); ++i) {
|
|
||||||
if (m_valid.get(i) && m_uf.find(i) == i) {
|
|
||||||
unsigned n = m_uf.next(i);
|
|
||||||
fact[0] = i;
|
|
||||||
while (n != i) {
|
|
||||||
fact[1] = n;
|
|
||||||
result->add_fact(fact);
|
|
||||||
n = m_uf.next(n);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
|
|
||||||
table_base::iterator equivalence_table::begin() const {
|
|
||||||
if (is_sparse()) return m_sparse->begin();
|
|
||||||
return mk_iterator(alloc(eq_iterator, *this, false));
|
|
||||||
}
|
|
||||||
|
|
||||||
table_base::iterator equivalence_table::end() const {
|
|
||||||
if (is_sparse()) return m_sparse->end();
|
|
||||||
return mk_iterator(alloc(eq_iterator, *this, true));
|
|
||||||
}
|
|
||||||
|
|
||||||
equivalence_table::class_iterator equivalence_table::class_begin(table_element const& _e) const {
|
|
||||||
SASSERT(!is_sparse());
|
|
||||||
unsigned e = static_cast<unsigned>(_e);
|
|
||||||
return class_iterator(*this, e, !is_valid(e));
|
|
||||||
}
|
|
||||||
|
|
||||||
equivalence_table::class_iterator equivalence_table::class_end(table_element const& _e) const {
|
|
||||||
SASSERT(!is_sparse());
|
|
||||||
unsigned e = static_cast<unsigned>(_e);
|
|
||||||
return class_iterator(*this, e, true);
|
|
||||||
}
|
|
||||||
|
|
||||||
void equivalence_table::display(std::ostream& out) const {
|
|
||||||
if (is_sparse()) {
|
|
||||||
m_sparse->display(out);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
for (unsigned i = 0; i < m_uf.get_num_vars(); ++i) {
|
|
||||||
if (is_valid(i) && m_uf.find(i) == i) {
|
|
||||||
unsigned j = i, last = i;
|
|
||||||
do {
|
|
||||||
out << "<" << i << " " << j << ">\n";
|
|
||||||
j = m_uf.next(j);
|
|
||||||
}
|
|
||||||
while (last != j);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned equivalence_table::get_size_estimate_rows() const {
|
|
||||||
if (is_sparse()) return m_sparse->get_size_estimate_rows();
|
|
||||||
return static_cast<unsigned>(get_signature()[0]);
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned equivalence_table::get_size_estimate_bytes() const {
|
|
||||||
if (is_sparse()) return m_sparse->get_size_estimate_bytes();
|
|
||||||
return static_cast<unsigned>(get_signature()[0]);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool equivalence_table::knows_exact_size() const {
|
|
||||||
return (!is_sparse() || m_sparse->knows_exact_size());
|
|
||||||
}
|
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -144,119 +144,6 @@ namespace datalog {
|
||||||
virtual iterator end() const;
|
virtual iterator end() const;
|
||||||
};
|
};
|
||||||
|
|
||||||
// -------------------------------------------
|
|
||||||
// Equivalence table.
|
|
||||||
// Really: partial equivalence relation table.
|
|
||||||
// -------------------------------------------
|
|
||||||
|
|
||||||
class equivalence_table;
|
|
||||||
|
|
||||||
class equivalence_table_plugin : public table_plugin {
|
|
||||||
class union_fn;
|
|
||||||
class select_equal_and_project_fn;
|
|
||||||
class join_project_fn;
|
|
||||||
|
|
||||||
bool is_equivalence_table(table_base const& tbl) const;
|
|
||||||
|
|
||||||
public:
|
|
||||||
typedef equivalence_table table;
|
|
||||||
|
|
||||||
equivalence_table_plugin(relation_manager & manager)
|
|
||||||
: table_plugin(symbol("equivalence"), manager) {}
|
|
||||||
|
|
||||||
virtual bool can_handle_signature(const table_signature & s);
|
|
||||||
|
|
||||||
virtual table_base * mk_empty(const table_signature & s);
|
|
||||||
|
|
||||||
protected:
|
|
||||||
virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src,
|
|
||||||
const table_base * delta);
|
|
||||||
virtual table_transformer_fn * mk_select_equal_and_project_fn(
|
|
||||||
const table_base & t,
|
|
||||||
const table_element & value, unsigned col);
|
|
||||||
virtual table_join_fn * mk_join_project_fn(const table_base & t1, const table_base & t2,
|
|
||||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt,
|
|
||||||
const unsigned * removed_cols);
|
|
||||||
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2,
|
|
||||||
unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
|
|
||||||
virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt,
|
|
||||||
const unsigned * removed_cols);
|
|
||||||
virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len,
|
|
||||||
const unsigned * permutation_cycle);
|
|
||||||
const table_element & value, unsigned col);
|
|
||||||
virtual table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t,
|
|
||||||
const table_base & negated_obj, unsigned joined_col_cnt,
|
|
||||||
const unsigned * t_cols, const unsigned * negated_cols);
|
|
||||||
#endif
|
|
||||||
};
|
|
||||||
|
|
||||||
class equivalence_table : public table_base {
|
|
||||||
friend class equivalence_table_plugin;
|
|
||||||
|
|
||||||
class eq_iterator;
|
|
||||||
union_find_default_ctx m_ctx;
|
|
||||||
bit_vector m_valid;
|
|
||||||
union_find<> m_uf;
|
|
||||||
table_base* m_sparse;
|
|
||||||
|
|
||||||
equivalence_table(equivalence_table_plugin & plugin, const table_signature & sig);
|
|
||||||
virtual ~equivalence_table();
|
|
||||||
|
|
||||||
unsigned first(table_fact const& f) const { return static_cast<unsigned>(f[0]); }
|
|
||||||
unsigned second(table_fact const& f) const { return static_cast<unsigned>(f[1]); }
|
|
||||||
|
|
||||||
bool is_valid(unsigned entry) const { return entry < m_valid.size() && m_valid.get(entry); }
|
|
||||||
bool is_sparse() const { return m_sparse != 0; }
|
|
||||||
|
|
||||||
// iterator over equivalence class of 'n'.
|
|
||||||
class class_iterator {
|
|
||||||
equivalence_table const& m_parent;
|
|
||||||
unsigned m_current;
|
|
||||||
unsigned m_last;
|
|
||||||
bool m_end;
|
|
||||||
public:
|
|
||||||
class_iterator(equivalence_table const& s, unsigned n, bool end):
|
|
||||||
m_parent(s), m_current(n), m_last(n), m_end(end) {}
|
|
||||||
|
|
||||||
unsigned operator*() { return m_current; }
|
|
||||||
|
|
||||||
class_iterator& operator++() {
|
|
||||||
m_current = m_parent.m_uf.next(m_current);
|
|
||||||
m_end = (m_current == m_last);
|
|
||||||
return *this;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool operator==(const class_iterator & it) const {
|
|
||||||
return
|
|
||||||
(m_end && it.m_end) ||
|
|
||||||
(!m_end && !it.m_end && m_current == it.m_current);
|
|
||||||
}
|
|
||||||
bool operator!=(const class_iterator & it) const { return !operator==(it); }
|
|
||||||
|
|
||||||
};
|
|
||||||
class_iterator class_begin(table_element const& e) const;
|
|
||||||
class_iterator class_end(table_element const& e) const;
|
|
||||||
|
|
||||||
void add_fact_sparse(table_fact const& f);
|
|
||||||
void mk_sparse();
|
|
||||||
|
|
||||||
|
|
||||||
public:
|
|
||||||
virtual void add_fact(const table_fact & f);
|
|
||||||
virtual void remove_fact(const table_element* fact);
|
|
||||||
virtual bool contains_fact(const table_fact & f) const;
|
|
||||||
virtual table_base* clone() const;
|
|
||||||
virtual iterator begin() const;
|
|
||||||
virtual iterator end() const;
|
|
||||||
virtual unsigned get_size_estimate_rows() const;
|
|
||||||
virtual unsigned get_size_estimate_bytes() const;
|
|
||||||
virtual bool knows_exact_size() const;
|
|
||||||
virtual void display(std::ostream & out) const;
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
|
||||||
|
|
@ -43,7 +43,6 @@ Revision History:
|
||||||
#include"dl_mk_similarity_compressor.h"
|
#include"dl_mk_similarity_compressor.h"
|
||||||
#include"dl_mk_unbound_compressor.h"
|
#include"dl_mk_unbound_compressor.h"
|
||||||
#include"dl_mk_subsumption_checker.h"
|
#include"dl_mk_subsumption_checker.h"
|
||||||
#include"dl_mk_partial_equiv.h"
|
|
||||||
#include"dl_mk_coi_filter.h"
|
#include"dl_mk_coi_filter.h"
|
||||||
#include"dl_mk_filter_rules.h"
|
#include"dl_mk_filter_rules.h"
|
||||||
#include"dl_mk_rule_inliner.h"
|
#include"dl_mk_rule_inliner.h"
|
||||||
|
|
@ -108,7 +107,6 @@ namespace datalog {
|
||||||
rm.register_plugin(alloc(sparse_table_plugin, rm));
|
rm.register_plugin(alloc(sparse_table_plugin, rm));
|
||||||
rm.register_plugin(alloc(hashtable_table_plugin, rm));
|
rm.register_plugin(alloc(hashtable_table_plugin, rm));
|
||||||
rm.register_plugin(alloc(bitvector_table_plugin, rm));
|
rm.register_plugin(alloc(bitvector_table_plugin, rm));
|
||||||
rm.register_plugin(alloc(equivalence_table_plugin, rm));
|
|
||||||
rm.register_plugin(lazy_table_plugin::mk_sparse(rm));
|
rm.register_plugin(lazy_table_plugin::mk_sparse(rm));
|
||||||
|
|
||||||
// register plugins for builtin relations
|
// register plugins for builtin relations
|
||||||
|
|
@ -308,7 +306,6 @@ namespace datalog {
|
||||||
transf.register_plugin(alloc(mk_similarity_compressor, m_context));
|
transf.register_plugin(alloc(mk_similarity_compressor, m_context));
|
||||||
}
|
}
|
||||||
transf.register_plugin(alloc(mk_rule_inliner, m_context));
|
transf.register_plugin(alloc(mk_rule_inliner, m_context));
|
||||||
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
|
|
||||||
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
|
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
|
||||||
transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
|
transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue