Refactor the Namer into two classes

4 files changed, 177 insertions, 152 deletions

diff --git a/Source/ModelViewer/BaseProvider.cs b/Source/ModelViewer/BaseProvider.cs
index 096bb35a..c4bae59e 100644
--- a/Source/ModelViewer/BaseProvider.cs
+++ b/Source/ModelViewer/BaseProvider.cs
@@ -30,7 +30,7 @@ namespace Microsoft.Boogie.ModelViewer.Base
 

     public IEnumerable<string> SortFields(IEnumerable<string> fields)

     {

-      return Namer.DefaultSortFields(fields);

+      return GlobalNamer.DefaultSortFields(fields);

     }

   }

 

diff --git a/Source/ModelViewer/DafnyProvider.cs b/Source/ModelViewer/DafnyProvider.cs
index fe2fd8a3..41d02a21 100644
--- a/Source/ModelViewer/DafnyProvider.cs
+++ b/Source/ModelViewer/DafnyProvider.cs
@@ -25,20 +25,19 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
         dm.states.Add(sn);

       }

       foreach (var s in dm.states) s.ComputeNames();

-      Namer.ComputeCanonicalNames(dm.states.Select(s => s.namer));

-      Namer.ComputeCanonicalNames(dm.states.Select(s => s.namer));

-      // Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

+      dm.gn.ComputeCanonicalNames();

       return dm.states;

     }

 

     public IEnumerable<string> SortFields(IEnumerable<string> fields)

     {

-      return Namer.DefaultSortFields(fields);

+      return GlobalNamer.DefaultSortFields(fields);

     }

   }

 

-  class DafnyModel

+  class DafnyModel : INamerCallbacks

   {

+    public readonly GlobalNamer gn;

     public readonly Model model;

     public readonly Model.Func f_heap_select, f_set_select, f_seq_length, f_seq_index, f_box, f_dim, f_index_field, f_multi_index_field;

     public readonly Dictionary<Model.Element, Model.Element[]> ArrayLengths = new Dictionary<Model.Element, Model.Element[]>();

@@ -47,6 +46,7 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
 

     public DafnyModel(Model m)

     {

+      gn = new GlobalNamer(this);

       model = m;

       f_heap_select = m.MkFunc("[3]", 3);

       f_set_select = m.MkFunc("[2]", 2);

@@ -193,21 +193,26 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       else

         return elt;

     }

+

+    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    {

+      return GlobalNamer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

+    }

   }

 

-  class StateNode : IState, INamerCallbacks

+  class StateNode : IState

   {

     internal readonly Model.CapturedState state;

     readonly string name;

     internal readonly DafnyModel dm;

     internal readonly List<VariableNode> vars = new List<VariableNode>();

-    internal readonly Namer namer;

+    internal readonly StateNamer namer;

     internal readonly int index;

     

     public StateNode(int i, DafnyModel parent, Model.CapturedState s)

     {

-      namer = new Namer(this);

       dm = parent;

+      namer = new StateNamer(dm.gn);

       state = s;

       index = i;

 

@@ -256,11 +261,6 @@ namespace Microsoft.Boogie.ModelViewer.Dafny
       }

     }

 

-    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

-    {

-      return Namer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

-    }

-

     internal void ComputeNames()

     {

       namer.ComputeNames(vars);

diff --git a/Source/ModelViewer/Namer.cs b/Source/ModelViewer/Namer.cs
index e1fb2bad..26c636c2 100644
--- a/Source/ModelViewer/Namer.cs
+++ b/Source/ModelViewer/Namer.cs
@@ -9,7 +9,7 @@ namespace Microsoft.Boogie.ModelViewer
   {

     internal Model.Element elt;

     internal List<IEdgeName> nodes = new List<IEdgeName>();

-    internal int score = Namer.maxScore;

+    internal int score = StateNamer.maxScore;

     internal string theName;

     internal bool unfolded;

     internal int stateIdx;

@@ -21,100 +21,18 @@ namespace Microsoft.Boogie.ModelViewer
     }

   }

 

-  public class Namer

+  public class GlobalNamer

   {

+    internal Dictionary<Model.Element, string> canonicalNames;

     INamerCallbacks cb;

-    internal const int maxScore = 10000;

-    List<EltName> eltNames = new List<EltName>();

-    Dictionary<Model.Element, EltName> unfoldings = new Dictionary<Model.Element, EltName>();

-    Dictionary<Model.Element, string> canonicalNames;

+    internal List<StateNamer> stateNamers = new List<StateNamer>();

 

-    public Namer(INamerCallbacks cb)

+    public GlobalNamer(INamerCallbacks cb)

     {

       this.cb = cb;

     }

 

-    EltName GetName(Model.Element elt)

-    {

-      EltName res;

-      if (unfoldings.TryGetValue(elt, out res))

-        return res;

-      res = new EltName(elt);

-      eltNames.Add(res);

-      unfoldings.Add(elt, res);

-      return res;

-    }

-

-    int EdgeNameScore(IEdgeName name)

-    {

-      return name.Dependencies.Select(e => GetName(e).score).Concat1(0).Max() + name.Score;

-    }

-

-    void ComputeBestName()

-    {

-      foreach (var n in eltNames) {

-        n.score = maxScore;

-        string s;

-        if (canonicalNames != null && canonicalNames.TryGetValue(n.elt, out s))

-          n.theName = s;

-      }

-

-      while (true) {

-        var changes = 0;

-        var thisElts = eltNames.ToArray();

-        foreach (var elt in thisElts) {

-          var newScore = elt.nodes.Select(EdgeNameScore).Concat1(int.MaxValue).Min();

-          if (newScore < elt.score) {

-            elt.score = newScore;

-            changes++;

-          }

-        }

-        if (changes == 0 && thisElts.Length == eltNames.Count)

-          break;

-      }

-      eltNames.Sort((x,y) => x.score - y.score);

-      foreach (var elt in eltNames) {

-        if (elt.nodes.Count > 0) {

-          elt.nodes.Sort((x, y) => EdgeNameScore(x) - EdgeNameScore(y));

-          elt.theName = elt.nodes[0].FullName();

-        }

-      }

-    }

-

-    void Unfold(IEnumerable<IDisplayNode> ns)

-    {

-      var workList = new Queue<IDisplayNode>(); // do BFS

-      ns.Iter(workList.Enqueue);

-

-      while (workList.Count > 0) {

-        var n = workList.Dequeue();

-

-        if (n.Element != null) {

-          var prev = GetName(n.Element);

-          prev.nodes.Add(n.Name);

-          if (prev.unfolded) // we've already been here

-            continue;

-          prev.unfolded = true;

-        }

-

-        if (!n.Expandable) return;

-

-        n.Expand().Iter(workList.Enqueue);

-      }

-    }

-

-    public void AddName(Model.Element elt, IEdgeName name)

-    {

-      var e = GetName(elt);

-      e.nodes.Add(name);

-    }

-

-    public void ComputeNames(IEnumerable<IDisplayNode> n)

-    {

-      Unfold(n);

-      ComputeBestName();

-    }

-

+    #region default namer callback implementations

     public static string DefaultCanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

     {

       if (edgeName == null)

@@ -175,14 +93,21 @@ namespace Microsoft.Boogie.ModelViewer
     public static IEnumerable<string> DefaultSortFields(IEnumerable<string> fields_)

     {

       var fields = new List<string>(fields_);

-      fields.Sort();

+      fields.Sort(CompareFields);

       return fields;

     }

+    #endregion

+

+    public void ComputeCanonicalNames()

+    {

+      for (int i = 0; i < 2; i++)

+        ComputeCanonicalNamesCore();

+    }

 

-    public static void ComputeCanonicalNames(IEnumerable<Namer> namers)

+    void ComputeCanonicalNamesCore()

     {

       var names = new Dictionary<Model.Element, EltName>();

-      var namersArr = namers.ToArray();

+      var namersArr = stateNamers.ToArray();

       for (int i = 0; i < namersArr.Length; ++i) {

         foreach (var n in namersArr[i].eltNames) {

           n.stateIdx = i;

@@ -201,24 +126,22 @@ namespace Microsoft.Boogie.ModelViewer
         string name = "";

         model = n.elt.Model;

         if (n.nodes.Count == 0) {

-          name = namersArr[0].cb.CanonicalBaseName(n.elt, null, 0);

+          name = cb.CanonicalBaseName(n.elt, null, 0);

           name = AppendIndex(usedNames, name);

         } else if (n.elt is Model.Boolean || n.elt is Model.Number)

           name = n.nodes[0].FullName();

         else {

-          name = namersArr[0].cb.CanonicalBaseName(n.elt, n.nodes[0], n.stateIdx);

+          name = cb.CanonicalBaseName(n.elt, n.nodes[0], n.stateIdx);

           name = AppendIndex(usedNames, name);

         }

         canonicals[n.elt] = name;

       }

 

-      for (int i = 0; i < namersArr.Length; ++i) {

-        namersArr[i].canonicalNames = canonicals;

-      }

+      canonicalNames = canonicals;

 

       foreach (var e in model.Elements) {

         if (!canonicals.ContainsKey(e)) {

-          var name = namersArr[0].cb.CanonicalBaseName(e, null, 0);

+          var name = cb.CanonicalBaseName(e, null, 0);

           canonicals[e] = AppendIndex(usedNames, name);

         }

       }

@@ -245,6 +168,102 @@ namespace Microsoft.Boogie.ModelViewer
         return res; // +" " + elt.ToString();

       return elt.ToString();

     }

+  }

+

+  public class StateNamer

+  {

+    GlobalNamer globalNamer;

+    internal const int maxScore = 10000;

+    internal List<EltName> eltNames = new List<EltName>();

+    Dictionary<Model.Element, EltName> unfoldings = new Dictionary<Model.Element, EltName>();

+

+

+    public StateNamer(GlobalNamer gn)

+    {

+      globalNamer = gn;

+      gn.stateNamers.Add(this);

+    }

+

+    EltName GetName(Model.Element elt)

+    {

+      EltName res;

+      if (unfoldings.TryGetValue(elt, out res))

+        return res;

+      res = new EltName(elt);

+      eltNames.Add(res);

+      unfoldings.Add(elt, res);

+      return res;

+    }

+

+    int EdgeNameScore(IEdgeName name)

+    {

+      return name.Dependencies.Select(e => GetName(e).score).Concat1(0).Max() + name.Score;

+    }

+

+    internal void ComputeBestName()

+    {

+      foreach (var n in eltNames) {

+        n.score = maxScore;

+        string s;

+        if (globalNamer.canonicalNames != null && globalNamer.canonicalNames.TryGetValue(n.elt, out s))

+          n.theName = s;

+      }

+

+      while (true) {

+        var changes = 0;

+        var thisElts = eltNames.ToArray();

+        foreach (var elt in thisElts) {

+          var newScore = elt.nodes.Select(EdgeNameScore).Concat1(int.MaxValue).Min();

+          if (newScore < elt.score) {

+            elt.score = newScore;

+            changes++;

+          }

+        }

+        if (changes == 0 && thisElts.Length == eltNames.Count)

+          break;

+      }

+      eltNames.Sort((x,y) => x.score - y.score);

+      foreach (var elt in eltNames) {

+        if (elt.nodes.Count > 0) {

+          elt.nodes.Sort((x, y) => EdgeNameScore(x) - EdgeNameScore(y));

+          elt.theName = elt.nodes[0].FullName();

+        }

+      }

+    }

+

+    void Unfold(IEnumerable<IDisplayNode> ns)

+    {

+      var workList = new Queue<IDisplayNode>(); // do BFS

+      ns.Iter(workList.Enqueue);

+

+      while (workList.Count > 0) {

+        var n = workList.Dequeue();

+

+        if (n.Element != null) {

+          var prev = GetName(n.Element);

+          prev.nodes.Add(n.Name);

+          if (prev.unfolded) // we've already been here

+            continue;

+          prev.unfolded = true;

+        }

+

+        if (!n.Expandable) return;

+

+        n.Expand().Iter(workList.Enqueue);

+      }

+    }

+

+    public void AddName(Model.Element elt, IEdgeName name)

+    {

+      var e = GetName(elt);

+      e.nodes.Add(name);

+    }

+

+    public void ComputeNames(IEnumerable<IDisplayNode> n)

+    {

+      Unfold(n);

+      ComputeBestName();

+    }

 

     public virtual string ElementName(Model.Element elt)

     {

@@ -255,6 +274,11 @@ namespace Microsoft.Boogie.ModelViewer
     {

       return GetName(elt).nodes;

     }

+

+    public virtual string CanonicalName(Model.Element elt)

+    {

+      return globalNamer.CanonicalName(elt);

+    }

   }

 

   public class EdgeName : IEdgeName

@@ -263,9 +287,9 @@ namespace Microsoft.Boogie.ModelViewer
 

     string formatFull, formatShort;

     Model.Element[] args;

-    Namer namer;

+    StateNamer namer;

 

-    public EdgeName(Namer n, string formatFull, string formatShort, params Model.Element[] args)

+    public EdgeName(StateNamer n, string formatFull, string formatShort, params Model.Element[] args)

     {

       this.namer = n;

       this.formatFull = formatFull;

@@ -274,7 +298,7 @@ namespace Microsoft.Boogie.ModelViewer
       Score = args.Length * 10;

     }

 

-    public EdgeName(Namer n, string formatBoth, params Model.Element[] args)

+    public EdgeName(StateNamer n, string formatBoth, params Model.Element[] args)

       : this(n, formatBoth, formatBoth, args)

     {

     }

diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index 9832bff1..8eb9f331 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -23,15 +23,13 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
         vm.states.Add(sn);

       }

       foreach (var s in vm.states) s.ComputeNames();

-      for (int i = 0; i < 1; i++) {

-        Namer.ComputeCanonicalNames(vm.states.Select(s => s.namer));

-      }

+      vm.gn.ComputeCanonicalNames();

       return vm.states;

     }

 

     public IEnumerable<string> SortFields(IEnumerable<string> fields)

     {

-      return Namer.DefaultSortFields(fields);

+      return GlobalNamer.DefaultSortFields(fields);

     }

 

   }

@@ -44,8 +42,9 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
     Map

   }

 

-  class VccModel

+  class VccModel : INamerCallbacks

   {

+    public readonly GlobalNamer gn;

     public readonly Model model;

     public readonly Model.Func f_ptr_to, f_phys_ptr_cast, f_spec_ptr_cast, f_mathint, f_local_value_is, f_spec_ptr_to, f_heap, f_select_field,

                                f_select_value, f_field, f_field_type, f_int_to_ptr, f_ptr_to_int, f_ptr, f_map_t;

@@ -54,6 +53,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

     public VccModel(Model m)

     {

+      gn = new GlobalNamer(this);

       model = m;

       f_ptr_to = m.MkFunc("$ptr_to", 1);

       f_spec_ptr_to = m.MkFunc("$spec_ptr_to", 1);

@@ -272,21 +272,52 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
 

       return result;

     }

+

+    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

+    {

+      var vm = this;

+      var name = GlobalNamer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

+

+      if (name.Contains("[") || name.Contains("'") || name.Contains("-"))

+        name = "";

+

+      if (name != "")

+        return name;

+

+      foreach (var tpl in elt.References) {

+        var fn = tpl.Func;

+        if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)

+          return "map";

+        if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)

+          return "map";

+      }

+

+      var fld = vm.f_field.TryEval(elt);

+      if (fld != null) {

+        var tp = vm.f_field_type.TryEval(fld);

+        if (tp != null) {

+          return vm.TypeName(tp);

+        }

+      }

+

+      // return elt.ToString(); // for debugging

+      return "";

+    }

   }

 

-  class StateNode : IState, INamerCallbacks

+  class StateNode : IState

   {

     internal Model.CapturedState state;

     string name;

     internal VccModel vm;

     internal List<VariableNode> vars;

-    internal Namer namer;

+    internal StateNamer namer;

     internal int index;

     

     public StateNode(int i, VccModel parent, Model.CapturedState s)

     {

-      this.namer = new Namer(this);

       this.vm = parent;

+      this.namer = new StateNamer(vm.gn);

       state = s;

       index = i;

 

@@ -308,36 +339,6 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
       SetupVars();

     }

 

-    public string CanonicalBaseName(Model.Element elt, IEdgeName edgeName, int stateIdx)

-    {

-      var name = Namer.DefaultCanonicalBaseName(elt, edgeName, stateIdx);

-

-      if (name.Contains("[") || name.Contains("'") || name.Contains("-"))

-        name = "";

-

-      if (name != "")

-        return name;

-

-      foreach (var tpl in elt.References) {

-        var fn = tpl.Func;

-        if (fn.Name.StartsWith("$select.$map_t") && fn.Arity == 2 && tpl.Args[0] == elt)

-          return "map";

-        if (fn.Name.StartsWith("$int_to_map_t") && tpl.Result == elt)

-          return "map";

-      }

-

-      var fld = vm.f_field.TryEval(elt);

-      if (fld != null) {

-        var tp = vm.f_field_type.TryEval(fld);

-        if (tp != null) {

-          return vm.TypeName(tp);

-        }

-      }

-

-      // return elt.ToString(); // for debugging

-      return "";

-    }

-

     void SetupVars()

     {

       if (vars != null) return;