mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 04:11:21 +00:00
Code Activity

dl_compiler: minor simplifications

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-05-27 17:07:18 +01:00
parent 9912b2cd67
commit b10f79a941
2 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -85,7 +85,7 @@ namespace datalog {
removed_cols.size(), removed_cols.c_ptr(), result)); removed_cols.size(), removed_cols.c_ptr(), result));
} }
void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, void compiler::make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
reg_idx & result, bool reuse, instruction_block & acc) { reg_idx & result, bool reuse, instruction_block & acc) {
relation_signature res_sig; relation_signature res_sig;
relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig); relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig);
@ -139,7 +139,7 @@ namespace datalog {
return r; return r;
} }
compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) { compiler::reg_idx compiler::get_single_column_register(const relation_sort s) {
relation_signature singl_sig; relation_signature singl_sig;
singl_sig.push_back(s); singl_sig.push_back(s);
return get_fresh_register(singl_sig); return get_fresh_register(singl_sig);
@ -165,7 +165,7 @@ namespace datalog {
} }
} }
void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val, void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort s, const relation_element val,
reg_idx & result, bool & dealloc, instruction_block & acc) { reg_idx & result, bool & dealloc, instruction_block & acc) {
reg_idx singleton_table; reg_idx singleton_table;
if(!m_constant_registers.find(s, val, singleton_table)) { if(!m_constant_registers.find(s, val, singleton_table)) {
@ -185,7 +185,7 @@ namespace datalog {
} }
} }
void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
bool & dealloc, instruction_block & acc) { bool & dealloc, instruction_block & acc) {
TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";); TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
@ -862,9 +862,11 @@ namespace datalog {
ast_manager& m = m_context.get_manager(); ast_manager& m = m_context.get_manager();
unsigned pt_len = r->get_positive_tail_size(); unsigned pt_len = r->get_positive_tail_size();
unsigned ut_len = r->get_uninterpreted_tail_size(); unsigned ut_len = r->get_uninterpreted_tail_size();
if (pt_len == ut_len) {
// no negated predicates
if (pt_len == ut_len)
return; return;
}
// populate negative variables: // populate negative variables:
for (unsigned i = pt_len; i < ut_len; ++i) { for (unsigned i = pt_len; i < ut_len; ++i) {
app * neg_tail = r->get_tail(i); app * neg_tail = r->get_tail(i);

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

@ -135,7 +135,7 @@ namespace datalog {
reg_idx get_fresh_register(const relation_signature & sig); reg_idx get_fresh_register(const relation_signature & sig);
reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r); reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r);
reg_idx get_single_column_register(const relation_sort & s); reg_idx get_single_column_register(const relation_sort s);
/** /**
\brief Allocate registers for predicates in \c pred and add them into the \c regs map. \brief Allocate registers for predicates in \c pred and add them into the \c regs map.
@ -150,7 +150,7 @@ namespace datalog {
const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc); 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, void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc); const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc);
void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, void make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
reg_idx & result, bool reuse, instruction_block & acc); reg_idx & result, bool reuse, instruction_block & acc);
/** /**
\brief Create add an union or widen operation and put it into \c acc. \brief Create add an union or widen operation and put it into \c acc.
@ -174,10 +174,10 @@ namespace datalog {
void make_dealloc_non_void(reg_idx r, instruction_block & acc); void make_dealloc_non_void(reg_idx r, instruction_block & acc);
void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort & s, const relation_element & val, void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val,
reg_idx & result, bool & dealloc, instruction_block & acc); reg_idx & result, bool & dealloc, instruction_block & acc);
void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
bool & dealloc, instruction_block & acc); bool & dealloc, instruction_block & acc);
void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result,
instruction_block & acc); instruction_block & acc);