mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Merge pull request #166 from hguenther/unstable

Browse source 
Improve filter_rules performance
This commit is contained in:
Nuno Lopes 2015-07-23 16:55:09 +01:00
commit 3d7785cc18
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/transforms/dl_mk_filter_rules.cpp
View file

@ -79,13 +79,13 @@ namespace datalog {
filter_key * key = alloc(filter_key, m); filter_key * key = alloc(filter_key, m);
mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred); mk_new_rule_tail(m, pred, non_local_vars, filter_domain, key->filter_args, key->new_pred);
func_decl * filter_decl = 0; filter_cache::obj_map_entry *entry = m_tail2filter.insert_if_not_there2(key, 0);
if (!m_tail2filter.find(key, filter_decl)) { func_decl*& filter_decl = entry->get_data().m_value;
if (!filter_decl) {
filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"), filter_decl = m_context.mk_fresh_head_predicate(pred->get_decl()->get_name(), symbol("filter"),
filter_domain.size(), filter_domain.c_ptr(), pred->get_decl()); filter_domain.size(), filter_domain.c_ptr(), pred->get_decl());
m_pinned.push_back(filter_decl); m_pinned.push_back(filter_decl);
m_tail2filter.insert(key, filter_decl);
app_ref filter_head(m); app_ref filter_head(m);
filter_head = m.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr()); filter_head = m.mk_app(filter_decl, key->filter_args.size(), key->filter_args.c_ptr());
app * filter_tail = key->new_pred; app * filter_tail = key->new_pred;