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

fix(library/congr_lemma_manager): take resulting type into account when computing congruence lemma

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-07 11:16:15 -08:00
parent b89b4cb5f0
commit 559c5a26a3
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/congr_lemma_manager.cpp
View file

@ -148,12 +148,15 @@ public:
if (r != m_cache.end()) if (r != m_cache.end())
return optional<result>(r->second); return optional<result>(r->second);
fun_info finfo = m_fmanager.get(fn); fun_info finfo = m_fmanager.get(fn);
list<unsigned> const & result_deps = finfo.get_dependencies();
buffer<congr_arg_kind> kinds; buffer<congr_arg_kind> kinds;
buffer<param_info> pinfos; buffer<param_info> pinfos;
to_buffer(finfo.get_params_info(), pinfos); to_buffer(finfo.get_params_info(), pinfos);
kinds.resize(pinfos.size(), congr_arg_kind::Eq); kinds.resize(pinfos.size(), congr_arg_kind::Eq);
for (unsigned i = 0; i < pinfos.size(); i++) { for (unsigned i = 0; i < pinfos.size(); i++) {
if (pinfos[i].is_subsingleton()) { if (std::find(result_deps.begin(), result_deps.end(), i) != result_deps.end()) {
kinds[i] = congr_arg_kind::Fixed;
} else if (pinfos[i].is_subsingleton()) {
if (empty(pinfos[i].get_dependencies())) if (empty(pinfos[i].get_dependencies()))
kinds[i] = congr_arg_kind::Fixed; kinds[i] = congr_arg_kind::Fixed;
else else