diff options
Diffstat (limited to 'Source/ModelViewer/TreeSkeleton.cs')
-rw-r--r-- | Source/ModelViewer/TreeSkeleton.cs | 410 |
1 files changed, 205 insertions, 205 deletions
diff --git a/Source/ModelViewer/TreeSkeleton.cs b/Source/ModelViewer/TreeSkeleton.cs index 543788a8..c3dee44f 100644 --- a/Source/ModelViewer/TreeSkeleton.cs +++ b/Source/ModelViewer/TreeSkeleton.cs @@ -1,205 +1,205 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-namespace Microsoft.Boogie.ModelViewer
-{
- internal class SkeletonItem
- {
- readonly string name;
- readonly List<SkeletonItem> children = new List<SkeletonItem>();
- internal readonly IDisplayNode[] displayNodes;
- internal bool[] isPrimary;
- internal readonly SkeletonItem parent;
- internal readonly Main main;
- internal readonly int level;
- internal bool expanded, wasExpanded;
- internal bool isMatch;
-
- public void Iter(Action<SkeletonItem> handler)
- {
- handler(this);
- children.ForEach(u => u.Iter(handler));
- }
-
- public IEnumerable<SkeletonItem> RecChildren
- {
- get
- {
- if (expanded) {
- foreach (var c in children) {
- yield return c;
- foreach (var ch in c.RecChildren)
- yield return ch;
- }
- }
- }
- }
-
- public SkeletonItem[] PopulateRoot(IEnumerable<IState> states)
- {
- var i = 0;
- foreach (var s in states) {
- displayNodes[i++] = new ContainerNode<IDisplayNode>(this.name, x => x, s.Nodes);
- }
-
- return BfsExpand(this);
- }
-
- public SkeletonItem(Main m, int stateCount)
- {
- name = "";
- main = m;
- displayNodes = new IDisplayNode[stateCount];
- isPrimary = new bool[stateCount];
- }
-
- internal SkeletonItem(string n, SkeletonItem par)
- : this(par.main, par.displayNodes.Length)
- {
- parent = par;
- name = n;
- level = par.level + 1;
- }
-
- public bool Expandable
- {
- get {
- if (wasExpanded)
- return children.Count > 0;
- return displayNodes.Any(d => d != null && d.Children.Count() > 0);
- }
- }
-
- public bool Expanded
- {
- get { return expanded; }
- set
- {
- expanded = value;
- if (expanded)
- ComputeChildren();
- }
- }
-
- static SkeletonItem[] BfsExpand(SkeletonItem skel)
- {
- for (int i = 0; i < skel.displayNodes.Length; ++i)
- BfsExpandCore(skel, i);
-
- var workItems = new Stack<SkeletonItem>();
- var allNodes = new List<SkeletonItem>();
- workItems.Push(skel);
-
- while (workItems.Count > 0) {
- var s = workItems.Pop();
- if (!s.isPrimary.Any())
- continue;
- allNodes.Add(s);
- s.children.Iter(workItems.Push);
- }
-
- return allNodes.ToArray();
- }
-
- static void BfsExpandCore(SkeletonItem skel, int idx)
- {
- var visited = new HashSet<Model.Element>();
- var workItems = new Queue<SkeletonItem>();
-
- workItems.Enqueue(skel);
- while (workItems.Count > 0) {
- var s = workItems.Dequeue();
- if (s.displayNodes[idx] == null)
- continue;
- var e = s.displayNodes[idx].Element;
- s.isPrimary[idx] = true;
- if (e != null) {
- if (visited.Contains(e))
- continue;
- visited.Add(e);
- }
- s.ComputeChildren();
- s.children.Iter(workItems.Enqueue);
- }
- }
-
- private void ComputeChildren()
- {
- if (wasExpanded) return;
- wasExpanded = true;
-
- var created = new Dictionary<string, SkeletonItem>();
- var names = new List<IDisplayNode>();
- for (int i = 0; i < displayNodes.Length; ++i) {
- var dn = displayNodes[i];
- if (dn == null) continue;
- foreach (var child in dn.Children) {
- if (child.ViewLevel > main.viewOpts.ViewLevel)
- continue;
- SkeletonItem skelChild;
- var name = child.Name;
- if (!created.TryGetValue(name, out skelChild)) {
- skelChild = new SkeletonItem(child.Name, this);
- created.Add(name, skelChild);
- names.Add(child);
- }
- skelChild.displayNodes[i] = child;
- }
- }
-
- foreach (var name in main.LangModel.SortFields(names)) {
- children.Add(created[name]);
- }
- }
-
- public bool MatchesWords(string[] words, Model.Element[] elts, Model.Element eq, int stateId)
- {
- var node = displayNodes[stateId];
- if (node == null)
- return false;
- var s1 = LongName(stateId).ToLower();
- var s2 = node.Value.ToLower();
-
- if (eq != null && node.Element != eq)
- return false;
-
- foreach (var w in words) {
- if (!s1.Contains(w) && !s2.Contains(w))
- return false;
- }
-
- foreach (var e in elts) {
- if (!node.References.Contains(e))
- return false;
- }
-
- return true;
- }
-
- public string LongName(int stateId)
- {
- var parents = new List<IDisplayNode>();
- for (var curr = this; curr != null; curr = curr.parent) {
- if (curr.parent != null) // skip the root
- parents.Add(curr.displayNodes[stateId]);
- }
- parents.Reverse();
- return main.LangModel.PathName(parents);
- }
-
- public void SyncWith(Dictionary<SkeletonItem, SkeletonItem> mapping, SkeletonItem old)
- {
- mapping[old] = this;
- Expanded = old.Expanded;
- var oldCh = old.children.ToDictionary(c => c.name);
- foreach (var c in children) {
- SkeletonItem oc;
- if (oldCh.TryGetValue(c.name, out oc))
- c.SyncWith(mapping, oc);
- }
- }
- }
-
-}
+using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace Microsoft.Boogie.ModelViewer +{ + internal class SkeletonItem + { + readonly string name; + readonly List<SkeletonItem> children = new List<SkeletonItem>(); + internal readonly IDisplayNode[] displayNodes; + internal bool[] isPrimary; + internal readonly SkeletonItem parent; + internal readonly Main main; + internal readonly int level; + internal bool expanded, wasExpanded; + internal bool isMatch; + + public void Iter(Action<SkeletonItem> handler) + { + handler(this); + children.ForEach(u => u.Iter(handler)); + } + + public IEnumerable<SkeletonItem> RecChildren + { + get + { + if (expanded) { + foreach (var c in children) { + yield return c; + foreach (var ch in c.RecChildren) + yield return ch; + } + } + } + } + + public SkeletonItem[] PopulateRoot(IEnumerable<IState> states) + { + var i = 0; + foreach (var s in states) { + displayNodes[i++] = new ContainerNode<IDisplayNode>(this.name, x => x, s.Nodes); + } + + return BfsExpand(this); + } + + public SkeletonItem(Main m, int stateCount) + { + name = ""; + main = m; + displayNodes = new IDisplayNode[stateCount]; + isPrimary = new bool[stateCount]; + } + + internal SkeletonItem(string n, SkeletonItem par) + : this(par.main, par.displayNodes.Length) + { + parent = par; + name = n; + level = par.level + 1; + } + + public bool Expandable + { + get { + if (wasExpanded) + return children.Count > 0; + return displayNodes.Any(d => d != null && d.Children.Count() > 0); + } + } + + public bool Expanded + { + get { return expanded; } + set + { + expanded = value; + if (expanded) + ComputeChildren(); + } + } + + static SkeletonItem[] BfsExpand(SkeletonItem skel) + { + for (int i = 0; i < skel.displayNodes.Length; ++i) + BfsExpandCore(skel, i); + + var workItems = new Stack<SkeletonItem>(); + var allNodes = new List<SkeletonItem>(); + workItems.Push(skel); + + while (workItems.Count > 0) { + var s = workItems.Pop(); + if (!s.isPrimary.Any()) + continue; + allNodes.Add(s); + s.children.Iter(workItems.Push); + } + + return allNodes.ToArray(); + } + + static void BfsExpandCore(SkeletonItem skel, int idx) + { + var visited = new HashSet<Model.Element>(); + var workItems = new Queue<SkeletonItem>(); + + workItems.Enqueue(skel); + while (workItems.Count > 0) { + var s = workItems.Dequeue(); + if (s.displayNodes[idx] == null) + continue; + var e = s.displayNodes[idx].Element; + s.isPrimary[idx] = true; + if (e != null) { + if (visited.Contains(e)) + continue; + visited.Add(e); + } + s.ComputeChildren(); + s.children.Iter(workItems.Enqueue); + } + } + + private void ComputeChildren() + { + if (wasExpanded) return; + wasExpanded = true; + + var created = new Dictionary<string, SkeletonItem>(); + var names = new List<IDisplayNode>(); + for (int i = 0; i < displayNodes.Length; ++i) { + var dn = displayNodes[i]; + if (dn == null) continue; + foreach (var child in dn.Children) { + if (child.ViewLevel > main.viewOpts.ViewLevel) + continue; + SkeletonItem skelChild; + var name = child.Name; + if (!created.TryGetValue(name, out skelChild)) { + skelChild = new SkeletonItem(child.Name, this); + created.Add(name, skelChild); + names.Add(child); + } + skelChild.displayNodes[i] = child; + } + } + + foreach (var name in main.LangModel.SortFields(names)) { + children.Add(created[name]); + } + } + + public bool MatchesWords(string[] words, Model.Element[] elts, Model.Element eq, int stateId) + { + var node = displayNodes[stateId]; + if (node == null) + return false; + var s1 = LongName(stateId).ToLower(); + var s2 = node.Value.ToLower(); + + if (eq != null && node.Element != eq) + return false; + + foreach (var w in words) { + if (!s1.Contains(w) && !s2.Contains(w)) + return false; + } + + foreach (var e in elts) { + if (!node.References.Contains(e)) + return false; + } + + return true; + } + + public string LongName(int stateId) + { + var parents = new List<IDisplayNode>(); + for (var curr = this; curr != null; curr = curr.parent) { + if (curr.parent != null) // skip the root + parents.Add(curr.displayNodes[stateId]); + } + parents.Reverse(); + return main.LangModel.PathName(parents); + } + + public void SyncWith(Dictionary<SkeletonItem, SkeletonItem> mapping, SkeletonItem old) + { + mapping[old] = this; + Expanded = old.Expanded; + var oldCh = old.children.ToDictionary(c => c.name); + foreach (var c in children) { + SkeletonItem oc; + if (oldCh.TryGetValue(c.name, out oc)) + c.SyncWith(mapping, oc); + } + } + } + +} |