From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/ModelViewer/TreeSkeleton.cs | 410 ++++++++++++++++++------------------- 1 file changed, 205 insertions(+), 205 deletions(-) (limited to 'Source/ModelViewer/TreeSkeleton.cs') 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 children = new List(); - 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 handler) - { - handler(this); - children.ForEach(u => u.Iter(handler)); - } - - public IEnumerable 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 states) - { - var i = 0; - foreach (var s in states) { - displayNodes[i++] = new ContainerNode(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(); - var allNodes = new List(); - 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(); - var workItems = new Queue(); - - 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(); - var names = new List(); - 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(); - 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 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 children = new List(); + 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 handler) + { + handler(this); + children.ForEach(u => u.Iter(handler)); + } + + public IEnumerable 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 states) + { + var i = 0; + foreach (var s in states) { + displayNodes[i++] = new ContainerNode(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(); + var allNodes = new List(); + 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(); + var workItems = new Queue(); + + 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(); + var names = new List(); + 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(); + 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 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); + } + } + } + +} -- cgit v1.2.3