mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

revert wrong optimization for single-occurrence negative columns

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-08 11:52:00 -07:00
parent 716663b04a
commit 93fd36b5da
1 changed files with 1 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -869,7 +869,6 @@ namespace datalog {
bool & dealloc, instruction_block & acc) {
uint_set pos_vars;
u_map<expr*> neg_vars;
u_map<unsigned> occs;
ast_manager& m = m_context.get_manager();
unsigned pt_len = r->get_positive_tail_size();
unsigned ut_len = r->get_uninterpreted_tail_size();
@ -885,12 +884,6 @@ namespace datalog {
if (is_var(e)) {
unsigned idx = to_var(e)->get_idx();
neg_vars.insert(idx, e);
if (!occs.contains(idx)) {
occs.insert(idx, 1);
}
else {
occs.find(idx)++;
}
}
}
}
@ -901,15 +894,11 @@ namespace datalog {
pos_vars.insert(to_var(e)->get_idx());
}
}
// add negative variables that are not in positive, but only
// for variables that occur more than once.
// add negative variables that are not in positive
u_map<expr*>::iterator it = neg_vars.begin(), end = neg_vars.end();
for (; it != end; ++it) {
unsigned v = it->m_key;
expr* e = it->m_value;
if (occs.find(v) == 1) {
continue;
}
if (!pos_vars.contains(v)) {
single_res_expr.push_back(e);
reg_idx new_single_res;