mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 21:50:52 +00:00
Code Activity

Rename cache to m_cache

Browse source
This commit is contained in:
Arie Gurfinkel 2018-08-20 15:24:11 -04:00
parent 0516e6f21f
commit 24044429a7
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz/transforms/dl_mk_synchronize.cpp
View file

@ -80,13 +80,13 @@ namespace datalog {
symbol new_name = symbol(buffer.c_str()); symbol new_name = symbol(buffer.c_str());
if (!cache.contains(new_name)) { if (!m_cache.contains(new_name)) {
was_added = true; was_added = true;
func_decl* orig = decls_buf[0]; func_decl* orig = decls_buf[0];
// AG : is this ref counted // AG : is this ref counted
func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name, func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name,
symbol::null, domain.size(), domain.c_ptr(), orig); symbol::null, domain.size(), domain.c_ptr(), orig);
cache.insert(new_name, product_pred); m_cache.insert(new_name, product_pred);
} }
return; return;
} }
@ -235,8 +235,8 @@ namespace datalog {
} }
symbol name = symbol(buffer.c_str()); symbol name = symbol(buffer.c_str());
SASSERT(cache.contains(name)); SASSERT(m_cache.contains(name));
func_decl * pred = cache[name]; func_decl * pred = m_cache[name];
ptr_vector<expr> args; ptr_vector<expr> args;
args.resize(args_num); args.resize(args_num);

2
src/muz/transforms/dl_mk_synchronize.h
View file

@ -61,7 +61,7 @@ namespace datalog {
scoped_ptr<rule_dependencies> m_deps; scoped_ptr<rule_dependencies> m_deps;
scoped_ptr<rule_stratifier> m_stratifier; scoped_ptr<rule_stratifier> m_stratifier;
map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> cache; map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> m_cache;
bool is_recursive(rule &r, func_decl &decl) const; bool is_recursive(rule &r, func_decl &decl) const;
bool is_recursive(rule &r, expr &e) const; bool is_recursive(rule &r, expr &e) const;