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

fix(library/tactic/smt/smt_state): ematch_using should not fail when a ground fact was added but no instance

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-09 19:24:13 -08:00
parent a43b856086
commit 3acdcaef2c
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/tactic/smt/smt_state.cpp
View file

@ -850,6 +850,7 @@ vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj cons
smt_goal g = to_smt_goal(head(ss));
smt S(ctx, dcs, g);
S.internalize(target);
bool add_facts = false;
buffer<expr_pair> new_instances;
to_hinst_lemmas(hs).for_each([&](hinst_lemma const & lemma) {
if (lemma.m_num_mvars == 0 && lemma.m_num_uvars == 0) {
@ -858,12 +859,13 @@ vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj cons
std::tie(type, h) = preprocess_forward(ctx, dcs, g, type, h);
lean_trace(name({"smt", "ematch"}), scope_trace_env _(ctx.env(), ctx);
tout() << "new ground fact: " << type << "\n";);
add_facts = true;
S.add(type, h);
} else {
S.ematch_using(lemma, new_instances);
}
});
if (new_instances.empty())
if (!add_facts && new_instances.empty())
return mk_tactic_exception("ematch_using failed, no instance was produced", ts);
for (expr_pair const & p : new_instances) {
expr type = p.first;