michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast/blast): avoid unnecessary calls to set_local_instances

Browse source 
This was producing a performance problem since the cache is invalidated/flushed
whenever we call this method.
This commit is contained in:
Leonardo de Moura 2015-11-13 10:08:29 -08:00
parent 0316412992
commit a7fdf5cc73
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/blast/blast.cpp
View file

@ -699,11 +699,16 @@ tmp_type_context * blastenv::mk_tmp_type_context() {
tmp_type_context * r;
if (m_tmp_ctx_pool.empty()) {
r = new tmp_tctx(m_env, m_ios, m_tmp_local_generator);
// Design decision: in the blast tactic, we only consider the instances that were
// available in initial goal provided to the blast tactic.
// So, we only need to setup the local instances when we create a new (temporary) type context.
// This is important since whenever we set the local instances the cache in at type context is
// invalidated.
r->set_local_instances(m_initial_context);
} else {
r = m_tmp_ctx_pool.back();
m_tmp_ctx_pool.pop_back();
}
r->set_local_instances(m_initial_context);
return r;
}