Potentially combine well-definedness and exhale code for pure quantifiers.

[gauravpartha]

The pull request #457 changed the exhale implementation to perform well-definedness checks during the exhale instead of doing them before the exhale, which was required for a proper handling of permission introspection and also for more intuitive error messages.

This change opens up possibilities for reducing the amount of Boogie code that Carbon generates. For example, well-definedness checks need to execute unfolding operations and Carbon's exhale implementation also executes unfolding operations to gain more information. As a result, there are cases where the same unfolding is executed twice in the same context, which is unnecessary. Since the exhale and the well-definedness check are more closely tied together now, this duplication can be more easily avoided (which the new implementation also does).

The change does not implement all such optimizations.

For example, consider exhale forall i: Int :: e where e is a pure expression. Currently, the encoding of this case is the following:

wellDefinednessCheck(forall i: Int :: e)
if(*) {
  exhale e[i1/i] //Point P1: i1 is fresh
  assume false
}
assume (forall i: Int :: e)

In this case, the unfolding operations executed by the well-definedness check are not visible to the exhale at point P1 and thus the exhale needs to execute unfolding operations again. However, there is room for optimization here, because wellDefinednessCheck(forall i: Int :: e) is given by:

if(*) {
  wellDefinednessCheck(e[i1/i]) //i1 is fresh
  assume false;
}

So it seems that one can provide the following encoding for exhale forall i: Int :: e:

if(*) {
  wellDefinednessCheck(e[i1/i]) //i1 is fresh
  exhale(e[i1/i]) //Point P2
  assume false;
}
assume (forall i: Int :: e)

Now unfolding operations executed in the well-definedness check are available to the exhale at point P2 and thus the unfolding operations need not be executed by the exhale.

I am not completely sure whether the well-definedness check and exhale always do what I describe above for pure quantifiers, but if this is indeed the case, then it could make sense to implement this optimization.