Triggers not ideally chosen for generated predicate axioms

[viper-admin]

Created by @gauravpartha on 2019-11-20 16:59
Last updated on 2019-11-29 12:35

The translation of the Viperpredicate P(x: Ref) leads to the following two axioms that are generated on the Boogie side:

axiom (forall x: Ref, x2: Ref ::
  { P(x), P(x2) }
  P(x) == P(x2) ==> x == x2
);

axiom (forall x: Ref, x2: Ref ::
  { P#sm(x), P#sm(x2) }
  P#sm(x) == P#sm(x2) ==> x == x2
);

This is not ideal, because the corresponding triggers lead to a quadratic number of instantiations. It would be nice to get rid of this with an inverse function construction (similarly to how one usually encodes injectivity).

[viper-admin]

@fabiopakk on 2019-11-29 12:35:

• changed the assignee from (none) to @fabiopakk