Automatically rewrite 'i in [a..b)' expressions

Created by @mschwerhoff on 2015-08-07 06:22
Last updated on 2015-08-07 06:23

Given the current sequence axiomatisation, expressions of the shape i in [a..b) are known to cause performance problems. Rewriting such expressions to a <= i && i < b is tempting, but not always wise. For example

• When inhaling a quantifier whose body has no expression other than i in [a..b) that can be used as a trigger, e.g.

     var x: Int
     inhale forall i: Int :: i in [0..10) ==> x > i
  

• When inhaling a quantifier for which i in [a..b) has been explicitly chosen as a trigger, e.g.

     var x: Int
     inhale forall i: Int :: {i in [0..10)} i in [0..10) && f(i) ==> x > i
     ...
     var i: Int
     inhale i in [0..10)
     exhale x > i
  

We should therefore carefully consider if we want to rewrite such expressions at all, or if we want to inform the user that they should consider rewriting them manually; and if we wanted to, when to rewrite them.

The issue names no files, tests, or entry points. Start by locating the sequence axiomatisation and the handling of i in [a..b) expressions, then determine when rewriting is sound and beneficial; done means an agreed rewriting policy or user guidance that addresses the supplied quantifier and trigger examples.