mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove a few leftovers from min aggregation cleanup
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
parent
83db19654f
commit
d9cd01f3f7
|
@ -484,126 +484,4 @@ namespace datalog {
|
|||
}
|
||||
brw.mk_or(disjs.size(), disjs.c_ptr(), fml);
|
||||
}
|
||||
|
||||
class table_plugin::min_fn : public table_min_fn{
|
||||
table_signature m_sig;
|
||||
const unsigned_vector m_group_by_cols;
|
||||
const unsigned m_col;
|
||||
public:
|
||||
min_fn(const table_signature & t_sig, const unsigned_vector& group_by_cols, const unsigned col)
|
||||
: m_sig(t_sig),
|
||||
m_group_by_cols(group_by_cols),
|
||||
m_col(col) {}
|
||||
|
||||
virtual table_base* operator()(table_base const& t) {
|
||||
//return reference_implementation(t);
|
||||
return reference_implementation_with_hash(t);
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
/**
|
||||
Reference implementation with negation:
|
||||
|
||||
T1 = join(T, T) by group_cols
|
||||
T2 = { (t1,t2) in T1 | t1[col] > t2[col] }
|
||||
T3 = { t1 | (t1,t2) in T2 }
|
||||
T4 = T \ T3
|
||||
|
||||
The point of this reference implementation is to show
|
||||
that the minimum requires negation (set difference).
|
||||
This is relevant for fixed point computations.
|
||||
*/
|
||||
virtual table_base * reference_implementation(const table_base & t) {
|
||||
relation_manager & manager = t.get_manager();
|
||||
scoped_ptr<table_join_fn> join_fn = manager.mk_join_fn(t, t, m_group_by_cols, m_group_by_cols);
|
||||
scoped_rel<table_base> join_table = (*join_fn)(t, t);
|
||||
|
||||
table_base::iterator join_table_it = join_table->begin();
|
||||
table_base::iterator join_table_end = join_table->end();
|
||||
table_fact row;
|
||||
|
||||
table_element i, j;
|
||||
|
||||
for (; join_table_it != join_table_end; ++join_table_it) {
|
||||
join_table_it->get_fact(row);
|
||||
i = row[m_col];
|
||||
j = row[t.num_columns() + m_col];
|
||||
|
||||
if (i > j) {
|
||||
continue;
|
||||
}
|
||||
|
||||
join_table->remove_fact(row);
|
||||
}
|
||||
|
||||
unsigned_vector cols(t.num_columns());
|
||||
for (unsigned k = 0; k < cols.size(); ++k) {
|
||||
cols[k] = cols.size() + k;
|
||||
SASSERT(cols[k] < join_table->num_columns());
|
||||
}
|
||||
|
||||
scoped_ptr<table_transformer_fn> project_fn = manager.mk_project_fn(*join_table, cols);
|
||||
scoped_rel<table_base> gt_table = (*project_fn)(*join_table);
|
||||
|
||||
for (unsigned k = 0; k < cols.size(); ++k) {
|
||||
cols[k] = k;
|
||||
SASSERT(cols[k] < t.num_columns());
|
||||
SASSERT(cols[k] < gt_table->num_columns());
|
||||
}
|
||||
|
||||
table_base * result = t.clone();
|
||||
scoped_ptr<table_intersection_filter_fn> diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols);
|
||||
(*diff_fn)(*result, *gt_table);
|
||||
return result;
|
||||
}
|
||||
|
||||
typedef map < table_fact, table_element, svector_hash_proc<table_element_hash>,
|
||||
vector_eq_proc<table_fact> > group_map;
|
||||
|
||||
// Thanks to Nikolaj who kindly helped with the second reference implementation!
|
||||
virtual table_base * reference_implementation_with_hash(const table_base & t) {
|
||||
group_map group;
|
||||
table_base::iterator it = t.begin();
|
||||
table_base::iterator end = t.end();
|
||||
table_fact row, row2;
|
||||
table_element current_value, min_value;
|
||||
for (; it != end; ++it) {
|
||||
it->get_fact(row);
|
||||
current_value = row[m_col];
|
||||
group_by(row, row2);
|
||||
group_map::entry* entry = group.find_core(row2);
|
||||
if (!entry) {
|
||||
group.insert(row2, current_value);
|
||||
}
|
||||
else if (entry->get_data().m_value > current_value) {
|
||||
entry->get_data().m_value = current_value;
|
||||
}
|
||||
}
|
||||
table_base* result = t.get_plugin().mk_empty(m_sig);
|
||||
table_base::iterator it2 = t.begin();
|
||||
for (; it2 != end; ++it2) {
|
||||
it2->get_fact(row);
|
||||
current_value = row[m_col];
|
||||
group_by(row, row2);
|
||||
VERIFY(group.find(row2, min_value));
|
||||
if (min_value == current_value) {
|
||||
result->add_fact(row);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
void group_by(table_fact const& in, table_fact& out) {
|
||||
out.reset();
|
||||
for (unsigned i = 0; i < m_group_by_cols.size(); ++i) {
|
||||
out.push_back(in[m_group_by_cols[i]]);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
table_min_fn * table_plugin::mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col) {
|
||||
return alloc(table_plugin::min_fn, t.get_signature(), group_by_cols, col);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -192,29 +192,6 @@ namespace datalog {
|
|||
virtual base_object * operator()(const base_object & t1, const base_object & t2) = 0;
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Aggregate minimum value
|
||||
|
||||
Informally, we want to group rows in a table \c t by \c group_by_cols and
|
||||
return the minimum value in column \c col among each group.
|
||||
|
||||
Let \c t be a table with N columns.
|
||||
Let \c group_by_cols be a set of column identifers for table \c t such that |group_by_cols| < N.
|
||||
Let \c col be a column identifier for table \c t such that \c col is not in \c group_by_cols.
|
||||
|
||||
Let R_col be a set of rows in table \c t such that, for all rows r_i, r_j in R_col
|
||||
and column identifiers k in \c group_by_cols, r_i[k] = r_j[k].
|
||||
|
||||
For each R_col, we want to restrict R_col to those rows whose value in column \c col is minimal.
|
||||
|
||||
min_fn(R, group_by_cols, col) =
|
||||
{ row in R | forall row' in R . row'[group_by_cols] = row[group_by_cols] => row'[col] >= row[col] }
|
||||
*/
|
||||
class min_fn : public base_fn {
|
||||
public:
|
||||
virtual base_object * operator()(const base_object & t) = 0;
|
||||
};
|
||||
|
||||
class transformer_fn : public base_fn {
|
||||
public:
|
||||
virtual base_object * operator()(const base_object & t) = 0;
|
||||
|
@ -879,7 +856,6 @@ namespace datalog {
|
|||
|
||||
typedef table_infrastructure::base_fn base_table_fn;
|
||||
typedef table_infrastructure::join_fn table_join_fn;
|
||||
typedef table_infrastructure::min_fn table_min_fn;
|
||||
typedef table_infrastructure::transformer_fn table_transformer_fn;
|
||||
typedef table_infrastructure::union_fn table_union_fn;
|
||||
typedef table_infrastructure::mutator_fn table_mutator_fn;
|
||||
|
@ -1044,7 +1020,6 @@ namespace datalog {
|
|||
|
||||
class table_plugin : public table_infrastructure::plugin_object {
|
||||
friend class relation_manager;
|
||||
class min_fn;
|
||||
protected:
|
||||
table_plugin(symbol const& n, relation_manager & manager) : plugin_object(n, manager) {}
|
||||
public:
|
||||
|
@ -1052,9 +1027,6 @@ namespace datalog {
|
|||
virtual bool can_handle_signature(const table_signature & s) { return s.functional_columns()==0; }
|
||||
|
||||
protected:
|
||||
virtual table_min_fn * mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col);
|
||||
|
||||
/**
|
||||
If the returned value is non-zero, the returned object must take ownership of \c mapper.
|
||||
Otherwise \c mapper must remain unmodified.
|
||||
|
|
|
@ -467,9 +467,6 @@ namespace datalog {
|
|||
// whether to dealloc the previous result
|
||||
bool dealloc = true;
|
||||
|
||||
// setup information for min aggregation
|
||||
unsigned_vector group_by_cols;
|
||||
|
||||
if(pt_len == 2) {
|
||||
reg_idx t1_reg=tail_regs[0];
|
||||
reg_idx t2_reg=tail_regs[1];
|
||||
|
|
|
@ -25,7 +25,6 @@ Revision History:
|
|||
#include"rel_context.h"
|
||||
#include"debug.h"
|
||||
#include"warning.h"
|
||||
#include"dl_table_relation.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -886,60 +885,6 @@ namespace datalog {
|
|||
removed_cols, result);
|
||||
}
|
||||
|
||||
class instr_min : public instruction {
|
||||
reg_idx m_source_reg;
|
||||
reg_idx m_target_reg;
|
||||
unsigned_vector m_group_by_cols;
|
||||
unsigned m_min_col;
|
||||
public:
|
||||
instr_min(reg_idx source_reg, reg_idx target_reg, const unsigned_vector & group_by_cols, unsigned min_col)
|
||||
: m_source_reg(source_reg),
|
||||
m_target_reg(target_reg),
|
||||
m_group_by_cols(group_by_cols),
|
||||
m_min_col(min_col) {
|
||||
}
|
||||
virtual bool perform(execution_context & ctx) {
|
||||
log_verbose(ctx);
|
||||
if (!ctx.reg(m_source_reg)) {
|
||||
ctx.make_empty(m_target_reg);
|
||||
return true;
|
||||
}
|
||||
|
||||
const relation_base & s = *ctx.reg(m_source_reg);
|
||||
if (!s.from_table()) {
|
||||
throw default_exception(default_exception::fmt(), "relation is not a table %s",
|
||||
s.get_plugin().get_name().bare_str());
|
||||
}
|
||||
++ctx.m_stats.m_min;
|
||||
const table_relation & tr = static_cast<const table_relation &>(s);
|
||||
const table_base & source_t = tr.get_table();
|
||||
relation_manager & r_manager = s.get_manager();
|
||||
|
||||
const relation_signature & r_sig = s.get_signature();
|
||||
scoped_ptr<table_min_fn> fn = r_manager.mk_min_fn(source_t, m_group_by_cols, m_min_col);
|
||||
table_base * target_t = (*fn)(source_t);
|
||||
|
||||
TRACE("dl",
|
||||
tout << "% ";
|
||||
target_t->display(tout);
|
||||
tout << "\n";);
|
||||
|
||||
relation_base * target_r = r_manager.mk_table_relation(r_sig, target_t);
|
||||
ctx.set_reg(m_target_reg, target_r);
|
||||
return true;
|
||||
}
|
||||
virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const {
|
||||
out << " MIN AGGR ";
|
||||
}
|
||||
virtual void make_annotations(execution_context & ctx) {
|
||||
}
|
||||
};
|
||||
|
||||
instruction * instruction::mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols,
|
||||
const unsigned min_col) {
|
||||
return alloc(instr_min, source, target, group_by_cols, min_col);
|
||||
}
|
||||
|
||||
class instr_select_equal_and_project : public instruction {
|
||||
reg_idx m_src;
|
||||
reg_idx m_result;
|
||||
|
|
|
@ -1023,12 +1023,6 @@ namespace datalog {
|
|||
return res;
|
||||
}
|
||||
|
||||
table_min_fn * relation_manager::mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col)
|
||||
{
|
||||
return t.get_plugin().mk_min_fn(t, group_by_cols, col);
|
||||
}
|
||||
|
||||
class relation_manager::auxiliary_table_transformer_fn {
|
||||
table_fact m_row;
|
||||
public:
|
||||
|
|
|
@ -251,9 +251,6 @@ namespace datalog {
|
|||
return mk_join_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), allow_product_relation);
|
||||
}
|
||||
|
||||
table_min_fn * mk_min_fn(const table_base & t,
|
||||
unsigned_vector & group_by_cols, const unsigned col);
|
||||
|
||||
/**
|
||||
\brief Return functor that transforms a table into one that lacks columns listed in
|
||||
\c removed_cols array.
|
||||
|
|
|
@ -291,27 +291,19 @@ namespace datalog {
|
|||
return res;
|
||||
}
|
||||
|
||||
#define _MIN_DONE_ 1
|
||||
|
||||
void rel_context::transform_rules() {
|
||||
rule_transformer transf(m_context);
|
||||
#ifdef _MIN_DONE_
|
||||
transf.register_plugin(alloc(mk_coi_filter, m_context));
|
||||
#endif
|
||||
transf.register_plugin(alloc(mk_filter_rules, m_context));
|
||||
transf.register_plugin(alloc(mk_simple_joins, m_context));
|
||||
if (m_context.unbound_compressor()) {
|
||||
transf.register_plugin(alloc(mk_unbound_compressor, m_context));
|
||||
}
|
||||
#ifdef _MIN_DONE_
|
||||
if (m_context.similarity_compressor()) {
|
||||
transf.register_plugin(alloc(mk_similarity_compressor, m_context));
|
||||
}
|
||||
#endif
|
||||
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
|
||||
#ifdef _MIN_DONE_
|
||||
transf.register_plugin(alloc(mk_rule_inliner, m_context));
|
||||
#endif
|
||||
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
|
||||
transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
|
||||
|
||||
|
|
|
@ -95,78 +95,8 @@ void test_dl_bitvector_table() {
|
|||
test_table(mk_bv_table);
|
||||
}
|
||||
|
||||
void test_table_min() {
|
||||
std::cout << "----- test_table_min -----\n";
|
||||
datalog::table_signature sig;
|
||||
sig.push_back(2);
|
||||
sig.push_back(4);
|
||||
sig.push_back(8);
|
||||
smt_params params;
|
||||
ast_manager ast_m;
|
||||
datalog::register_engine re;
|
||||
datalog::context ctx(ast_m, re, params);
|
||||
datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager();
|
||||
|
||||
m.register_plugin(alloc(datalog::bitvector_table_plugin, m));
|
||||
|
||||
datalog::table_base* tbl = mk_bv_table(m, sig);
|
||||
datalog::table_base& table = *tbl;
|
||||
|
||||
datalog::table_fact row, row1, row2, row3;
|
||||
row.push_back(1);
|
||||
row.push_back(2);
|
||||
row.push_back(5);
|
||||
|
||||
// Group (1,2,*)
|
||||
row1 = row;
|
||||
row[2] = 6;
|
||||
row2 = row;
|
||||
row[2] = 5;
|
||||
row3 = row;
|
||||
|
||||
table.add_fact(row1);
|
||||
table.add_fact(row2);
|
||||
table.add_fact(row3);
|
||||
|
||||
// Group (1,3,*)
|
||||
row[1] = 3;
|
||||
row1 = row;
|
||||
row[2] = 7;
|
||||
row2 = row;
|
||||
row[2] = 4;
|
||||
row3 = row;
|
||||
|
||||
table.add_fact(row1);
|
||||
table.add_fact(row2);
|
||||
table.add_fact(row3);
|
||||
|
||||
table.display(std::cout);
|
||||
|
||||
unsigned_vector group_by(2);
|
||||
group_by[0] = 0;
|
||||
group_by[1] = 1;
|
||||
|
||||
datalog::table_min_fn * min_fn = m.mk_min_fn(table, group_by, 2);
|
||||
datalog::table_base * min_tbl = (*min_fn)(table);
|
||||
|
||||
min_tbl->display(std::cout);
|
||||
|
||||
row[1] = 2;
|
||||
row[2] = 5;
|
||||
SASSERT(min_tbl->contains_fact(row));
|
||||
|
||||
row[1] = 3;
|
||||
row[2] = 4;
|
||||
SASSERT(min_tbl->contains_fact(row));
|
||||
|
||||
dealloc(min_fn);
|
||||
min_tbl->deallocate();
|
||||
tbl->deallocate();
|
||||
}
|
||||
|
||||
void tst_dl_table() {
|
||||
test_dl_bitvector_table();
|
||||
test_table_min();
|
||||
}
|
||||
#else
|
||||
void tst_dl_table() {
|
||||
|
|
Loading…
Reference in a new issue