1 files changed, 135 insertions, 0 deletions
diff --git a/Source/VCExpr/LetBindingSorter.cs b/Source/VCExpr/LetBindingSorter.cs
new file mode 100644
index 00000000..96eb0af2
--- /dev/null
+++ b/Source/VCExpr/LetBindingSorter.cs
@@ -0,0 +1,135 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using Microsoft.Contracts;
+using Microsoft.Basetypes;
+
+// Sort the bindings in a let-expression so that terms bound earlier do
+// not contain variables bound later
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+  // (argument is not used)
+  public class LetBindingSorter : MutatingVCExprVisitor<bool> {
+
+    private readonly FreeVariableCollector! FreeVarCollector =
+      new FreeVariableCollector ();
+
+    private List<VCExprVar!>! FreeVarsIn(VCExpr! expr) {
+      FreeVarCollector.Collect(expr);
+      List<VCExprVar!>! freeVars = new List<VCExprVar!> (FreeVarCollector.FreeTermVars.Keys);
+      FreeVarCollector.Reset();
+      return freeVars;
+    }
+
+    public LetBindingSorter(VCExpressionGenerator! gen) {
+      base(gen);
+    }
+
+    public override VCExpr! Visit(VCExprLet! node, bool arg) {
+      IDictionary<VCExprVar!, Binding!> boundVars =
+        new Dictionary<VCExprVar!, Binding!> ();
+
+      // recurse and collect the free variables in bound terms and formulae
+      foreach (VCExprLetBinding! binding in node) {
+        VCExpr! newE = Mutate(binding.E, arg);
+        Binding! b = new Binding (binding.V, newE, FreeVarsIn(newE));
+        boundVars.Add(b.V, b);
+      }
+
+      // generate the occurrence edges
+      foreach (KeyValuePair<VCExprVar!, Binding!> pair in boundVars) {
+        Binding! b = pair.Value;
+        foreach (VCExprVar! v in b.FreeVars) {
+          Binding b2;
+          if (boundVars.TryGetValue(v, out b2)) {
+            ((!)b2).Occurrences.Add(b);
+            b.InvOccurrencesNum = b.InvOccurrencesNum + 1;
+          }
+        }
+      }
+
+      // topological sort
+      Stack<Binding!> rootBindings = new Stack<Binding!> ();
+      foreach (KeyValuePair<VCExprVar!, Binding!> pair in boundVars)
+        if (pair.Value.InvOccurrencesNum == 0)
+          rootBindings.Push(pair.Value);
+
+      List<Binding!>! sortedBindings = new List<Binding!> ();
+      while (rootBindings.Count > 0) {
+        Binding! b = rootBindings.Pop();
+        sortedBindings.Add(b);
+        foreach (Binding! b2 in b.Occurrences) {
+          b2.InvOccurrencesNum = b2.InvOccurrencesNum - 1;
+          if (b2.InvOccurrencesNum == 0)
+            rootBindings.Push(b2);
+        }
+      }
+
+      if (exists{KeyValuePair<VCExprVar!, Binding!> pair in boundVars;
+                 pair.Value.InvOccurrencesNum > 0})
+        System.Diagnostics.Debug.Fail("Cyclic let-bindings");
+
+      assert node.Length == sortedBindings.Count;
+
+      // check which of the bindings can be dropped
+      VCExpr! newBody = Mutate(node.Body, arg);
+
+      IDictionary<VCExprVar!, VCExprVar!>! usedVars =
+        new Dictionary<VCExprVar!, VCExprVar!> ();
+      foreach (VCExprVar! v in FreeVarsIn(newBody))
+        if (!usedVars.ContainsKey(v))
+          usedVars.Add(v, v);
+
+      for (int i = sortedBindings.Count - 1; i >= 0; --i) {
+        if (usedVars.ContainsKey(sortedBindings[i].V)) {
+          foreach (VCExprVar! v in sortedBindings[i].FreeVars)
+            if (!usedVars.ContainsKey(v))
+              usedVars.Add(v, v);
+        } else {
+          sortedBindings.RemoveAt(i);
+        }
+      }
+
+      // assemble the resulting let-expression
+      List<VCExprLetBinding!>! newBindings = new List<VCExprLetBinding!> ();
+      foreach (Binding b in sortedBindings)
+        newBindings.Add(Gen.LetBinding(b.V, b.E));
+
+      return Gen.Let(newBindings, newBody);
+    }    
+
+    private class Binding {
+      public readonly VCExprVar! V;
+      public readonly VCExpr! E;
+      public readonly List<VCExprVar!>! FreeVars;
+
+      // list of all bound expression in which the variable V occurs
+      // (outgoing edges)
+      public readonly List<Binding>! Occurrences;
+
+      // number of variables that are bound in this let-expression
+      // and that occur in FreeVars
+      // (incoming edges)
+      public int InvOccurrencesNum;
+
+      public Binding(VCExprVar! v, VCExpr! e, List<VCExprVar!>! freeVars) {
+        this.V = v;
+        this.E = e;
+        this.FreeVars = freeVars;
+        this.Occurrences = new List<Binding> ();
+        this.InvOccurrencesNum = 0;
+      }
+    }
+
+  }
+
+}