mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Add basic compiler support for min aggregation function

Browse source 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
This commit is contained in:
Alex Horn 2015-06-11 16:23:26 +01:00
parent c8a123b7dd
commit 8c097044e8
2 changed files with 66 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

48
src/muz/rel/dl_compiler.cpp
View file

@ -73,6 +73,12 @@ namespace datalog {
vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
}
void compiler::make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols,
const unsigned min_col, instruction_block & acc) {
target = get_register(m_reg_signatures[source], true, source);
acc.push_back(instruction::mk_min(source, target, group_by_cols, min_col));
}
void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) {
SASSERT(!removed_cols.empty());
@ -440,6 +446,30 @@ namespace datalog {
get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res);
}
void compiler::find_min_aggregates(const rule * r, ptr_vector<func_decl>& min_aggregates) {
unsigned ut_len = r->get_uninterpreted_tail_size();
unsigned ft_len = r->get_tail_size(); // full tail
func_decl * aggregate;
for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
aggregate = r->get_tail(tail_index)->get_decl();
if (dl_decl_plugin::is_aggregate(aggregate)) {
min_aggregates.push_back(aggregate);
}
}
}
bool compiler::prepare_min_aggregate(const func_decl * decl, const ptr_vector<func_decl>& min_aggregates,
unsigned_vector & group_by_cols, unsigned & min_col) {
for (unsigned i = 0; i < min_aggregates.size(); ++i) {
if (dl_decl_plugin::min_func_decl(min_aggregates[i]) == decl) {
group_by_cols = dl_decl_plugin::group_by_cols(min_aggregates[i]);
min_col = dl_decl_plugin::min_col(min_aggregates[i]);
return true;
}
}
return false;
}
void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs,
reg_idx delta_reg, bool use_widening, instruction_block & acc) {
@ -465,6 +495,12 @@ namespace datalog {
// whether to dealloc the previous result
bool dealloc = true;
// setup information for min aggregation
ptr_vector<func_decl> min_aggregates;
find_min_aggregates(r, min_aggregates);
unsigned_vector group_by_cols;
unsigned min_col;
if(pt_len == 2) {
reg_idx t1_reg=tail_regs[0];
reg_idx t2_reg=tail_regs[1];
@ -473,6 +509,14 @@ namespace datalog {
SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args());
SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args());
if (prepare_min_aggregate(a1->get_decl(), min_aggregates, group_by_cols, min_col)) {
make_min(t1_reg, single_res, group_by_cols, min_col, acc);
}
if (prepare_min_aggregate(a2->get_decl(), min_aggregates, group_by_cols, min_col)) {
make_min(t2_reg, single_res, group_by_cols, min_col, acc);
}
variable_intersection a1a2(m_context.get_manager());
a1a2.populate(a1,a2);
@ -514,6 +558,10 @@ namespace datalog {
single_res = tail_regs[0];
dealloc = false;
if (prepare_min_aggregate(a->get_decl(), min_aggregates, group_by_cols, min_col)) {
make_min(single_res, single_res, group_by_cols, min_col, acc);
}
SASSERT(m_reg_signatures[single_res].size() == a->get_num_args());
unsigned n=a->get_num_args();

18
src/muz/rel/dl_compiler.h
View file

@ -120,6 +120,22 @@ namespace datalog {
instruction_observer m_instruction_observer;
expr_free_vars m_free_vars;
/**
\brief Finds all the min aggregation functions in the premise of a given rule.
*/
static void find_min_aggregates(const rule * r, ptr_vector<func_decl>& min_aggregates);
/**
\brief Decides whether a predicate is subject to a min aggregation function.
If \c decl is subject to a min aggregation function, the output parameters are written
with the neccessary information.
\returns true if the output paramaters have been written
*/
static bool prepare_min_aggregate(const func_decl * decl, const ptr_vector<func_decl>& min_aggregates,
unsigned_vector & group_by_cols, unsigned & min_col);
/**
If true, the union operation on the underlying structure only provides the information
whether the updated relation has changed or not. In this case we do not get anything
@ -146,6 +162,8 @@ namespace datalog {
void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result,
bool reuse_t1, instruction_block & acc);
void make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols,
const unsigned min_col, instruction_block & acc);
void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars,
const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc);
void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,