max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(util/fresh_name): add fresh_name_scope

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-06 14:53:05 -08:00
parent 8eb34a39cb
commit 1547d47387
2 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/util/fresh_name.cpp
View file

@ -91,6 +91,20 @@ name_generator mk_fresh_name_generator_child() {
return get_name_generator().mk_child();
}
fresh_name_scope::fresh_name_scope():
m_old(get_name_generator()) {
get_name_generator() = name_generator(*g_fresh);
}
fresh_name_scope::fresh_name_scope(name_generator const & g):
m_old(get_name_generator()) {
get_name_generator() = g;
}
fresh_name_scope::~fresh_name_scope() {
get_name_generator() = m_old;
}
void initialize_fresh_name() {
g_fresh = new name("_fresh");
}

8
src/util/fresh_name.h
View file

@ -45,6 +45,14 @@ void set_fresh_name_generator(name_generator const & g);
We use this operation to set the name_generator before we execute a task. */
name_generator mk_fresh_name_generator_child();
struct fresh_name_scope {
name_generator m_old;
public:
fresh_name_scope();
fresh_name_scope(name_generator const & g);
~fresh_name_scope();
};
void initialize_fresh_name();
void finalize_fresh_name();
}