[Why3-club] record simplifications

Andrei Paskevich andrei at lri.fr
Mon Nov 19 17:28:34 CET 2012


On 16 November 2012 18:27, Johannes Kanig <kanig at adacore.com> wrote:
> On 11/16/2012 06:19 PM, Guillaume Melquiond wrote:
>> If I am not mistaken, that is precisely what src/transform/eval_match.ml
>> does. Except that it is only called by the WP, which would explain why
>> it fails for you. (But I am no expert.)

This is correct.

> Ah, I remember eval_match now, thanks. Is there a reason why that's not
> exported as a regular transformation?

No good one, as far as I can tell, except that for every goal coming
from WP it is already applied unconditionnaly. I think, we shall
export it, and it is also interesting to make it applicable to
premises, too. In this way, a universal quantifier on a record in a
lemma can be replaced with universal quantifiers on its fields,
helping an SMT prover to find the good triggers.

> Hardwiring it in the code would
> make it unflexible wrt. ordering of transformations - consider the
> inlining of "f" in the example.

Actually, eval_match, as used in Mlw_wp, is configured to inline
certain functions (namely, linear and non-recursive).

Best,
Andrei



More information about the Why3-club mailing list