Merge quantifiers when triggers cannot otherwise be inferred

[viper-admin]

Created by @alexanderjsummers on 2015-09-08 13:00
Last updated on 2015-10-27 08:33

If two quantifiers are nested, as in:

forall x:T :: forall y:T :: p(x,y)

we might fail to infer triggers for the outer quantifier (no candidate terms mention only x), whereas we would succeed if we merged the quantifiers into:

forall x:T, y:T :: p(x,y)

This should be done (when triggers for the outer quantifier cannot otherwise be found)

Examples of this happening show up in the basic/domains.sil test case, in which these axioms are written:

#!silver

    axiom cons_length {
        forall x: T :: forall xs: List[T] :: length(cons(x, xs)) == (length(xs) + 1)
    }
    axiom nil_cons {
        forall z: T :: forall zs: List[T] :: cons(z, zs) != nil()
    }

See also #61

[viper-admin]

@alexanderjsummers on 2015-09-08 13:01:

• edited the description

[viper-admin]

@mschwerhoff on 2015-10-27 08:33:

• changed component from (none) to Triggers