mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-02-08 10:25:44 +01:00
commit ded635cd06
9 changed files with 113 additions and 111 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -33,7 +33,6 @@ namespace datalog {
void compiler::reset() {
m_pred_regs.reset();
m_new_reg = 0;
}
void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) {
@ -51,16 +50,16 @@ namespace datalog {
}
void compiler::make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result,
instruction_block & acc) {
bool reuse_t1, instruction_block & acc) {
relation_signature res_sig;
relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(),
vars.get_cols1(), vars.get_cols2(), res_sig);
result = get_fresh_register(res_sig);
result = get_register(res_sig, reuse_t1, t1);
acc.push_back(instruction::mk_join(t1, t2, vars.size(), vars.get_cols1(), vars.get_cols2(), result));
}
void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars,
const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc) {
relation_signature aux_sig;
relation_signature sig1 = m_reg_signatures[t1];
relation_signature sig2 = m_reg_signatures[t2];
@ -68,29 +67,29 @@ namespace datalog {
relation_signature res_sig;
relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.c_ptr(),
res_sig);
result = get_fresh_register(res_sig);
result = get_register(res_sig, reuse_t1, t1);
acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(),
vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
}
void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) {
SASSERT(!removed_cols.empty());
relation_signature res_sig;
relation_signature::from_project(m_reg_signatures[src], removed_cols.size(),
removed_cols.c_ptr(), res_sig);
result = get_fresh_register(res_sig);
result = get_register(res_sig, reuse, src);
acc.push_back(instruction::mk_filter_interpreted_and_project(src, cond,
removed_cols.size(), removed_cols.c_ptr(), result));
}
void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
reg_idx & result, instruction_block & acc) {
reg_idx & result, bool reuse, instruction_block & acc) {
relation_signature res_sig;
relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig);
result = get_fresh_register(res_sig);
result = get_register(res_sig, reuse, src);
acc.push_back(instruction::mk_select_equal_and_project(m_context.get_manager(),
src, val, col, result));
}
@ -115,12 +114,12 @@ namespace datalog {
}
void compiler::make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols,
reg_idx & result, instruction_block & acc) {
reg_idx & result, bool reuse, instruction_block & acc) {
SASSERT(col_cnt>0);
relation_signature res_sig;
relation_signature::from_project(m_reg_signatures[src], col_cnt, removed_cols, res_sig);
result = get_fresh_register(res_sig);
result = get_register(res_sig, reuse, src);
acc.push_back(instruction::mk_projection(src, col_cnt, removed_cols, result));
}
@ -132,6 +131,14 @@ namespace datalog {
return result;
}
compiler::reg_idx compiler::get_register(const relation_signature & sig, bool reuse, compiler::reg_idx r) {
if (!reuse)
return get_fresh_register(sig);
SASSERT(r != execution_context::void_register);
m_reg_signatures[r] = sig;
return r;
}
compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) {
relation_signature singl_sig;
singl_sig.push_back(s);
@ -169,11 +176,11 @@ namespace datalog {
}
if(src==execution_context::void_register) {
result = singleton_table;
dealloc = false;
SASSERT(dealloc == false);
}
else {
variable_intersection empty_vars(m_context.get_manager());
make_join(src, singleton_table, empty_vars, result, acc);
make_join(src, singleton_table, empty_vars, result, dealloc, acc);
dealloc = true;
}
}
@ -198,11 +205,11 @@ namespace datalog {
}
if(src == execution_context::void_register) {
result = total_table;
dealloc = false;
SASSERT(dealloc == false);
}
else {
variable_intersection empty_vars(m_context.get_manager());
make_join(src, total_table, empty_vars, result, acc);
make_join(src, total_table, empty_vars, result, dealloc, acc);
dealloc = true;
}
}
@ -221,7 +228,7 @@ namespace datalog {
void compiler::make_duplicate_column(reg_idx src, unsigned col, reg_idx & result,
instruction_block & acc) {
bool reuse, instruction_block & acc) {
relation_signature & src_sig = m_reg_signatures[src];
reg_idx single_col_reg;
@ -236,19 +243,20 @@ namespace datalog {
removed_cols.push_back(i);
}
}
make_projection(src, removed_cols.size(), removed_cols.c_ptr(), single_col_reg, acc);
make_projection(src, removed_cols.size(), removed_cols.c_ptr(), single_col_reg, false, acc);
}
variable_intersection vi(m_context.get_manager());
vi.add_pair(col, 0);
make_join(src, single_col_reg, vi, result, acc);
make_dealloc_non_void(single_col_reg, acc);
make_join(src, single_col_reg, vi, result, reuse, acc);
if (src_col_cnt != 1)
make_dealloc_non_void(single_col_reg, acc);
}
void compiler::make_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle,
reg_idx & result, instruction_block & acc) {
reg_idx & result, bool reuse, instruction_block & acc) {
relation_signature res_sig;
relation_signature::from_rename(m_reg_signatures[src], cycle_len, permutation_cycle, res_sig);
result = get_fresh_register(res_sig);
result = get_register(res_sig, reuse, src);
acc.push_back(instruction::mk_rename(src, cycle_len, permutation_cycle, result));
}
@ -301,12 +309,8 @@ namespace datalog {
new_src_col_offset.push_back(src_cols_to_remove.size());
}
if(!src_cols_to_remove.empty()) {
reg_idx new_curr;
make_projection(curr, src_cols_to_remove.size(), src_cols_to_remove.c_ptr(), new_curr, acc);
if (dealloc)
make_dealloc_non_void(curr, acc);
make_projection(curr, src_cols_to_remove.size(), src_cols_to_remove.c_ptr(), curr, dealloc, acc);
dealloc = true;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
//update ACK_BOUND_VAR references
@ -325,21 +329,15 @@ namespace datalog {
}
unsigned bound_column_index;
if(acis[i].kind!=ACK_UNBOUND_VAR || !handled_unbound.find(acis[i].var_index,bound_column_index)) {
reg_idx new_curr;
bool new_dealloc;
bound_column_index=curr_sig->size();
if(acis[i].kind==ACK_CONSTANT) {
make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, new_curr, new_dealloc, acc);
make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, curr, dealloc, acc);
}
else {
SASSERT(acis[i].kind==ACK_UNBOUND_VAR);
make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, new_curr, new_dealloc, acc);
make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, curr, dealloc, acc);
handled_unbound.insert(acis[i].var_index,bound_column_index);
}
if (dealloc)
make_dealloc_non_void(curr, acc);
dealloc = new_dealloc;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
SASSERT(bound_column_index==curr_sig->size()-1);
}
@ -357,12 +355,8 @@ namespace datalog {
used_cols.insert(col);
continue;
}
reg_idx new_curr;
make_duplicate_column(curr, col, new_curr, acc);
if (dealloc)
make_dealloc_non_void(curr, acc);
make_duplicate_column(curr, col, curr, dealloc, acc);
dealloc = true;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
unsigned bound_column_index=curr_sig->size()-1;
SASSERT((*curr_sig)[bound_column_index]==acis[i].domain);
@ -387,12 +381,8 @@ namespace datalog {
SASSERT(permutation.size()<=col_cnt); //this should not be an infinite loop
} while(next!=i);
reg_idx new_curr;
make_rename(curr, permutation.size(), permutation.c_ptr(), new_curr, acc);
if (dealloc)
make_dealloc_non_void(curr, acc);
make_rename(curr, permutation.size(), permutation.c_ptr(), curr, dealloc, acc);
dealloc = true;
curr=new_curr;
curr_sig = & m_reg_signatures[curr];
}
@ -491,10 +481,10 @@ namespace datalog {
get_local_indexes_for_projection(r, removed_cols);
if(removed_cols.empty()) {
make_join(t1_reg, t2_reg, a1a2, single_res, acc);
make_join(t1_reg, t2_reg, a1a2, single_res, false, acc);
}
else {
make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, acc);
make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, false, acc);
}
unsigned rem_index = 0;
@ -521,11 +511,11 @@ namespace datalog {
SASSERT(rem_index==rem_sz);
}
else if(pt_len==1) {
reg_idx t_reg=tail_regs[0];
app * a = r->get_tail(0);
SASSERT(m_reg_signatures[t_reg].size()==a->get_num_args());
single_res = tail_regs[0];
dealloc = false;
single_res = t_reg;
SASSERT(m_reg_signatures[single_res].size() == a->get_num_args());
unsigned n=a->get_num_args();
for(unsigned i=0; i<n; i++) {
@ -533,22 +523,14 @@ namespace datalog {
if(is_app(arg)) {
app * c = to_app(arg); //argument is a constant
SASSERT(m.is_value(c));
reg_idx new_reg;
make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc);
if(single_res!=t_reg) {
//since single_res is a local register, we deallocate it
make_dealloc_non_void(single_res, acc);
}
single_res = new_reg;
make_select_equal_and_project(single_res, c, single_res_expr.size(), single_res, dealloc, acc);
dealloc = true;
}
else {
SASSERT(is_var(arg));
single_res_expr.push_back(arg);
}
}
if(single_res==t_reg) {
dealloc = false;
}
}
else {
@ -556,6 +538,7 @@ namespace datalog {
//single_res register should never be used in this case
single_res=execution_context::void_register;
dealloc = false;
}
add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, dealloc, acc);
@ -635,14 +618,7 @@ namespace datalog {
} else {
// we have an unbound variable, so we add an unbound column for it
relation_sort unbound_sort = m_free_vars[v];
reg_idx new_reg;
bool new_dealloc;
make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
dealloc = new_dealloc;
filtered_res = new_reg;
make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, filtered_res, dealloc, acc);
src_col = single_res_expr.size();
single_res_expr.push_back(m.mk_var(v, unbound_sort));
@ -655,6 +631,12 @@ namespace datalog {
}
}
// add at least one column for the negative filter
if (pt_len != ut_len && filtered_res == execution_context::void_register) {
relation_signature empty_signature;
make_full_relation(head_pred, empty_signature, filtered_res, acc);
}
//enforce negative predicates
for (unsigned i = pt_len; i<ut_len; i++) {
app * neg_tail = r->get_tail(i);
@ -673,14 +655,7 @@ namespace datalog {
SASSERT(is_app(e));
relation_sort arg_sort;
m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
reg_idx new_reg;
bool new_dealloc;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
dealloc = new_dealloc;
filtered_res = new_reg;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), filtered_res, dealloc, acc);
t_cols.push_back(single_res_expr.size());
neg_cols.push_back(i);
@ -750,12 +725,8 @@ namespace datalog {
make_clone(filtered_res, filtered_res, acc);
acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed));
} else {
reg_idx new_reg;
std::sort(remove_columns.begin(), remove_columns.end());
make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, new_reg, acc);
if (dealloc)
make_dealloc_non_void(filtered_res, acc);
filtered_res = new_reg;
make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, filtered_res, dealloc, acc);
}
dealloc = true;
}
@ -892,7 +863,7 @@ namespace datalog {
ast_manager& m = m_context.get_manager();
unsigned pt_len = r->get_positive_tail_size();
unsigned ut_len = r->get_uninterpreted_tail_size();
if (pt_len == ut_len || pt_len == 0) {
if (pt_len == ut_len) {
return;
}
// populate negative variables:
@ -921,13 +892,7 @@ namespace datalog {
expr* e = it->m_value;
if (!pos_vars.contains(v)) {
single_res_expr.push_back(e);
reg_idx new_single_res;
bool new_dealloc;
make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), new_single_res, new_dealloc, acc);
if (dealloc)
make_dealloc_non_void(single_res, acc);
dealloc = new_dealloc;
single_res = new_single_res;
make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), single_res, dealloc, acc);
TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";);
}
}

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

@ -82,9 +82,11 @@ namespace datalog {
relation_sort domain; // domain of the column
assembling_column_kind kind; // "instruction" tag
unsigned source_column; // for ACK_BOUND_VAR
unsigned var_index; // for ACK_UNBOUND_VAR
relation_element constant; // for ACK_CONSTANT
union {
unsigned source_column; // for ACK_BOUND_VAR
unsigned var_index; // for ACK_UNBOUND_VAR
relation_element constant; // for ACK_CONSTANT
};
};
class instruction_observer : public instruction_block::instruction_observer {
@ -111,7 +113,6 @@ namespace datalog {
*/
instruction_block & m_top_level_code;
pred2idx m_pred_regs;
reg_idx m_new_reg;
vector<relation_signature> m_reg_signatures;
obj_pair_map<sort, app, reg_idx> m_constant_registers;
obj_pair_map<sort, decl, reg_idx> m_total_registers;
@ -133,6 +134,7 @@ namespace datalog {
bool compile_with_widening() const { return m_context.compile_with_widening(); }
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_single_column_register(const relation_sort & s);
/**
@ -143,21 +145,21 @@ namespace datalog {
void get_fresh_registers(const func_decl_set & preds, pred2idx & regs);
void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result,
instruction_block & acc);
bool reuse_t1, 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, 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,
const unsigned_vector & removed_cols, reg_idx & result, 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,
reg_idx & result, 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.
*/
void make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widening, instruction_block & acc);
void make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols,
reg_idx & result, instruction_block & acc);
reg_idx & result, bool reuse, instruction_block & acc);
void make_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle,
reg_idx & result, instruction_block & acc);
reg_idx & result, bool reuse, instruction_block & acc);
void make_clone(reg_idx src, reg_idx & result, instruction_block & acc);
/**
@ -183,7 +185,7 @@ namespace datalog {
void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr,
bool & dealloc, instruction_block& acc);
void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc);
void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, bool reuse, instruction_block & acc);
void ensure_predicate_loaded(func_decl * pred, instruction_block & acc);

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

@ -107,6 +107,13 @@ doc& doc_manager::fillX(doc& src) {
m.fillX(src.pos());
return src;
}
unsigned doc_manager::get_size_estimate_bytes(const doc& d) const {
return m.get_size_estimate_bytes(d.pos())
+ d.neg().get_size_estimate_bytes(m)
+ sizeof(doc);
}
bool doc_manager::set_and(doc& dst, doc const& src) {
// (A \ B) & (C \ D) = (A & C) \ (B u D)
if (!m.set_and(dst.pos(), src.pos())) return false;

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

@ -87,6 +87,7 @@ public:
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(); }
unsigned get_size_estimate_bytes(const doc& d) const;
doc* project(doc_manager& dstm, bit_vector const& to_delete, doc const& src);
bool well_formed(doc const& d) const;
bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
@ -326,6 +327,13 @@ public:
}
}
unsigned get_size_estimate_bytes(const M& m) const {
unsigned sz = sizeof(T*) * size();
for (unsigned i = 0; i < size(); ++i) {
sz += m.get_size_estimate_bytes(*m_elems[i]);
}
return sz;
}
};

7
src/muz/rel/rel_context.cpp
View file

@ -172,8 +172,6 @@ namespace datalog {
compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
TRACE("dl", m_code.display(m_ectx, tout); );
bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
if (time_limit || restart_time!=0) {
@ -628,11 +626,6 @@ namespace datalog {
m_code.make_annotations(m_ectx);
m_code.process_all_costs();
out << "\n--------------\n";
out << "Instructions\n";
m_code.display(m_ectx, out);
out << "\n--------------\n";
out << "Big relations\n";
m_ectx.report_big_relations(1000, out);

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

@ -57,6 +57,8 @@ public:
tbv* allocate(tbv const& bv, unsigned const* permutation);
void deallocate(tbv* bv);
unsigned get_size_estimate_bytes(const tbv&) const { return m.num_bytes(); }
void copy(tbv& dst, tbv const& src) const;
unsigned num_tbits() const { return m.num_bits()/2; }

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

@ -181,6 +181,10 @@ namespace datalog {
m_elems.display(dm, out); out << "\n";
}
unsigned udoc_relation::get_size_estimate_bytes() const {
return sizeof(*this) + m_elems.get_size_estimate_bytes(dm);
}
// -------------
udoc_plugin::udoc_plugin(relation_manager& rm):
@ -509,13 +513,27 @@ namespace datalog {
}
};
void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
for (unsigned i = 0; i < src.size(); ++i) {
doc* d = dm.allocate(src[i]);
if (dst.insert(dm, d)) {
bool deltaempty = delta ? delta->is_empty() : false;
if (dst.is_empty()) {
for (unsigned i = 0; i < src.size(); ++i) {
dst.push_back(dm.allocate(src[i]));
if (delta) {
delta->insert(dm, dm.allocate(src[i]));
if (deltaempty)
delta->push_back(dm.allocate(src[i]));
else
delta->insert(dm, dm.allocate(src[i]));
}
}
}
} else {
for (unsigned i = 0; i < src.size(); ++i) {
if (dst.insert(dm, dm.allocate(src[i])) && delta) {
if (deltaempty)
delta->push_back(dm.allocate(src[i]));
else
delta->insert(dm, dm.allocate(src[i]));
}
}
}
}
relation_union_fn * udoc_plugin::mk_union_fn(

1
src/muz/rel/udoc_relation.h
View file

@ -53,6 +53,7 @@ namespace datalog {
virtual void display(std::ostream& out) const;
virtual bool is_precise() const { return true; }
virtual unsigned get_size_estimate_rows() const { return m_elems.size(); }
virtual unsigned get_size_estimate_bytes() const;
doc_manager& get_dm() const { return dm; }
udoc const& get_udoc() const { return m_elems; }

6
src/util/debug.h
View file

@ -58,12 +58,18 @@ bool is_debug_enabled(const char * tag);
#define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
#define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
#ifdef Z3DEBUG
# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
#else
#if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable)
// only available in gcc >= 4.5 and in newer versions of clang
# define UNREACHABLE() __builtin_unreachable()
#elif defined(_MSC_VER)
# define UNREACHABLE() __assume(0)
#else
#define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
#endif
#endif
#define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)