Inline lets before trigger selection

[wilcoxjay]

Fixes #128.

When TriggerAnnotation.Annotate encounters a LetExpr, it now inlines the let using Translator.Substitute (which is now static to make it easy to call from outside the translator).

This improves trigger selection when there are lets inside a quantifier. There was even an (admittedly synthetic) existing test case in the test suite that ran into this problem!

Note that the inlined expression is only considered for the purposes of trigger selection. The rest of the pipeline continues to see the un-inlined expression.

I considered factoring Translator.Substitute out of the translator and into its own file (or into Cloner), but in the end I felt that it made sense to leave it there because of the scary comment about dropping parts of expressions that are only for well-formedness checks.

[RustanLeino]

Great feature. :) I'm also happy to see that Substitute could be made static.

I have one suggestion: Why not also support let expressions with multiple LHSs? I think this would come at almost no extra work, by simply calling the overloaded Substitute method (the one that takes a substMap).

[cpitclaudel]

Indeed, very nice. This should help with loop detection, too; as in this comment:

  // WISH: It might also be good to zeta-reduce before loop detection.
  assert forall x :: true || Q(x) || (var xx := x+1; Q(xx));

There was even an (admittedly synthetic) existing test case in the test suite that ran into this problem!
Well, it did have a WISH annotation, didn't it? :)

[wilcoxjay]

I added support for lets with multiple LHSs, as you suggested.

@cpitclaudel In that example, is the intention that after integrating let-inlining into loop detection, that a loop will be detected where it is not now?

[cpitclaudel]

Exactly.

[wilcoxjay]

I just added let inlining to loop detection as well, and it works on the tests. (The loop even gets rewritten correctly!)

[cpitclaudel]

Super! Very nice.