Sascha Boehme <[email protected]> wrote:
Hi,
Zitat von Ond?ej Kun?ar <[email protected]>:
But AVL-Trees were already broken in Isabelle's changeset
791157a4179a (ensured that rewr_conv rule t = "t == u" literally
not just modulo beta-eta) before Jasmin's changeset 34b0464d7eef.
It seems that the changeset fixing rewr_conv interacts with smt.
There is a goal which is the same goal before and after the change
- the term is really the same; no tricks like the pretty-printer
does beta-reduction.
And smt fails only after the change and it doesn't matter if the
pregenerated certificates are used. Somebody who understands smt
should take a look at how much the changeset with rewr_conv is
harmful to smt.
I do have an idea what might go wrong. I'll need to investigate it
further before committing a patch.
I found the explanation for the problem. It is indeed related to
Tobias's change in rewr_conv. The normalization code in the smt method
rewrites arithmetic constants (e.g. max) by replacing them with lambda
abstractions (e.g. %a b. if a > b then a else b) and not beta-reducing
the resulting terms. In a later step a conversion goes through the
terms and does further rewritings. Before Tobias' change, one
sub-conversion (a rewr_conv) in that process returns a beta-reduced
equation (reducing one of the above lambda abstractions), and hence
the left-hand side does not match anymore the term given to the
conversion. This causes an exception to be thrown by then_con.
Nevertheless, a surrounding conversion catches that exception and
tries something else resulting in a term that "by accident" looked as
expected. Now, after Tobias' change, the inner rewr_conv returns an
equation with unmodified left-hand side. The outer conversion that
previously catched the exception does not kick in and the result is
something different (and not what one would have expected). Summa
summarum, there is something severly broken in the normalization code
of the smt method, and Tobias' change of rewr_conv helped to discover
this flaw. This indicates that the changed rewr_conv behaves in a way
that causes fewer surprises for users and as such was an improvement
to the code.
I'll fix the normalization of the smt method.
Cheers,
Sascha
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
