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

feat(library/unifier): do not create a case-split for choice constraints that produce only one alternative

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 18:52:13 -07:00
parent 443022d840
commit 50e21586b0
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/unifier.cpp
View file

@ -799,9 +799,14 @@ struct unifier_fn {
auto r = rlist.pull(); auto r = rlist.pull();
justification j = mk_composite1(c.get_justification(), m_type_jst.second); justification j = mk_composite1(c.get_justification(), m_type_jst.second);
if (r) { if (r) {
justification a = mk_assumption_justification(m_next_assumption_idx); if (r->second.is_nil()) {
add_case_split(std::unique_ptr<case_split>(new choice_case_split(*this, m, m_type_jst.second, r->second))); // there is only one alternative
return process_choice_result(m, r->first, mk_composite1(j, a)); return process_choice_result(m, r->first, j);
} else {
justification a = mk_assumption_justification(m_next_assumption_idx);
add_case_split(std::unique_ptr<case_split>(new choice_case_split(*this, m, m_type_jst.second, r->second)));
return process_choice_result(m, r->first, mk_composite1(j, a));
}
} else { } else {
set_conflict(j); set_conflict(j);
return false; return false;