From 5ed20852acfcaa61053972b8f9dd7d36b2d6c495 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Mon, 14 Jun 2021 21:43:59 -0700 Subject: [PATCH 01/60] added file for future unit tests --- TestProject1/DAGViewTest.cs | 13 +++++++++++++ TestProject1/SmallGraphs.cs | 10 ++++++++++ 2 files changed, 23 insertions(+) create mode 100644 TestProject1/DAGViewTest.cs create mode 100644 TestProject1/SmallGraphs.cs diff --git a/TestProject1/DAGViewTest.cs b/TestProject1/DAGViewTest.cs new file mode 100644 index 0000000..5d89b41 --- /dev/null +++ b/TestProject1/DAGViewTest.cs @@ -0,0 +1,13 @@ +using Microsoft.VisualStudio.TestTools.UnitTesting; + +namespace TestProject1 +{ + [TestClass] + public class UnitTest1 + { + [TestMethod] + public void TestMethod1() + { + } + } +} diff --git a/TestProject1/SmallGraphs.cs b/TestProject1/SmallGraphs.cs new file mode 100644 index 0000000..61adbc7 --- /dev/null +++ b/TestProject1/SmallGraphs.cs @@ -0,0 +1,10 @@ +using System; +using System.Collections.Generic; +using System.Text; + +namespace TestProject1 +{ + class Class1 + { + } +} From 02cd7ae16c7926e13bd78fbf2e94372af9881b7d Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 15 Jun 2021 13:41:42 -0700 Subject: [PATCH 02/60] changeg namespace --- TestProject1/DAGViewTest.cs | 8 ++++++-- TestProject1/SmallGraphs.cs | 12 ++++++++++-- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/TestProject1/DAGViewTest.cs b/TestProject1/DAGViewTest.cs index 5d89b41..414ac36 100644 --- a/TestProject1/DAGViewTest.cs +++ b/TestProject1/DAGViewTest.cs @@ -1,13 +1,17 @@ using Microsoft.VisualStudio.TestTools.UnitTesting; -namespace TestProject1 +namespace AxiomProfiler { [TestClass] - public class UnitTest1 + public class DAGViewTest { + static SmallGraphs graphs = new SmallGraphs(); + static AxiomProfiler axiomprofiler = new AxiomProfiler(); + [TestMethod] public void TestMethod1() { + Assert.AreEqual("a", graphs.graph1.Id); } } } diff --git a/TestProject1/SmallGraphs.cs b/TestProject1/SmallGraphs.cs index 61adbc7..c477784 100644 --- a/TestProject1/SmallGraphs.cs +++ b/TestProject1/SmallGraphs.cs @@ -1,10 +1,18 @@ using System; using System.Collections.Generic; -using System.Text; +using System.Linq; +using Microsoft.Msagl.Drawing; +using AxiomProfiler; namespace TestProject1 { - class Class1 + class SmallGraphs { + public Node graph1; + + public SmallGraphs() + { + graph1 = new Node("a"); + } } } From ec133f7968f8f402fa3318972ef21d623164a58a Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 15 Jun 2021 14:35:57 -0700 Subject: [PATCH 03/60] added/changed specs and todo --- source/DAGView.cs | 168 +++++++++++----------------------------------- 1 file changed, 40 insertions(+), 128 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index ebf073f..9e20583 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -468,6 +468,9 @@ private void sourceTreeButton_Click(object sender, EventArgs e) redrawGraph(); } + // This functions and it's helper functions are properlly explain in + //https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing + // helper functions were originally private, but changing to public was needed to unit testing private void pathExplanationButton_Click(object sender, EventArgs e) { if (previouslySelectedNode == null) @@ -540,152 +543,55 @@ private void pathExplanationButton_Click(object sender, EventArgs e) private static readonly double outlierThreshold = 0.3; private static readonly double incomingEdgePenalizationFactor = 0.5; - /// - /// Assigns a score to instantiation paths based on the predicted likelyhood that it conatins a matching loop. - /// - /// Higher values indicate a higher likelyhood of the path containing a matching loop. - /// All constants were determined experimentally. + // Return a score where + // - having longer length recieves a higher score + // - having less covered children recieves a higher score + // - having shorter pattern recieved a higher score private static double InstantiationPathScoreFunction(InstantiationPath instantiationPath, bool eliminatePrefix, bool eliminatePostfix) { - //There may be some "outiers" before or after a matching loop. - //We first identify quantifiers that occur at most outlierThreshold times as often as the most common quantifier in the path... - var statistics = instantiationPath.Statistics(); - var eliminationTreshhold = (statistics == null || !statistics.Any()) ? 1 : - Math.Max(statistics.Max(dp => dp.Item2) * outlierThreshold, 1); - var nonEliminatableQuantifiers = new HashSet>(statistics - .Where(dp => dp.Item2 > eliminationTreshhold) - .Select(dp => dp.Item1)); - - //...find the longest contigous subsequence that does not contain eliminatable quantifiers... - var pathInstantiations = instantiationPath.getInstantiations(); - var instantiations = pathInstantiations.Zip(pathInstantiations.Skip(1), (prev, next) => !next.bindingInfo.IsPatternMatch() ? - Enumerable.Repeat(Tuple.Create(next.Quant, null, null), 1) : - next.bindingInfo.bindings.Where(kv => prev.concreteBody.isSubterm(kv.Value.Item2.id)) - .Select(kv => Tuple.Create(next.Quant, next.bindingInfo.fullPattern, kv.Key))).ToArray(); - - var maxStartIndex = 0; - var maxLength = 0; - var lastMaxStartIndex = 0; - - var firstKept = nonEliminatableQuantifiers.Any(q => q.Item1 == pathInstantiations.First().Quant && q.Item2 == pathInstantiations.First().bindingInfo.fullPattern); - var curStartIndex = firstKept ? 0 : 1; - var curLength = firstKept ? 1 : 0; - for (var i = 0; i < instantiations.Count(); ++i) - { - if (instantiations[i].Any(q => nonEliminatableQuantifiers.Contains(q))) - { - ++curLength; - } - else - { - if (curLength > maxLength) - { - maxStartIndex = curStartIndex; - lastMaxStartIndex = curStartIndex; - maxLength = curLength; - } - else if (curLength == maxLength) - { - lastMaxStartIndex = curStartIndex; - } - curStartIndex = i + 2; - curLength = 0; - } - } - if (curLength > maxLength) - { - maxStartIndex = curStartIndex; - lastMaxStartIndex = curStartIndex; - maxLength = curLength; - } - else if (curLength == maxLength) - { - lastMaxStartIndex = curStartIndex; - } - - //...and eliminate the prefix/postfix of that subsequence - var remainingStart = eliminatePrefix ? maxStartIndex : 0; - var remainingLength = (eliminatePostfix ? lastMaxStartIndex + maxLength : instantiations.Count()) - remainingStart; - var remainingInstantiations = instantiationPath.getInstantiations().ToList().GetRange(remainingStart, remainingLength); - - if (remainingInstantiations.Count() == 0) return -1; - - var remainingPath = new InstantiationPath(); - foreach (var inst in remainingInstantiations) - { - remainingPath.append(inst); - } - - /* We count the number of incoming edges (responsible instantiations that are not part of the path) and penalize them. - * This ensures that we choose the best path. E.g. in the triangular case (A -> B, A -> C, B -> C) we want to choose A -> B -> C - * and not A -> B which would have an incoming edge (B -> C). - */ - var numberIncomingEdges = 0; - foreach (var inst in remainingInstantiations) - { - numberIncomingEdges += inst.ResponsibleInstantiations.Where(i => !instantiationPath.getInstantiations().Contains(i)).Count(); - } - - /* the score is given by the number of remaining instantiations devided by the number of remaining quantifiers - * which is an approximation for the number of repetitions of a matching loop occuring in that path. - */ - return (remainingPath.Length() - numberIncomingEdges * incomingEdgePenalizationFactor) / remainingPath.NumberOfDistinctQuantifierFingerprints(); + // TODO + return 0.0; } // For performance reasons we cannot score all possible paths. Instead we score segments of length 8 and // build a path from the best segments. private static readonly int pathSegmentSize = 8; - private InstantiationPath BestDownPath(Node node) + + // Described in https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing + // Get all down patterns, + // extent them to max(3, lcm(length of patterns)), + // score them and sort by score + // extend to top 5 path fully + // score and sort the fully extended path + // return the best one + public InstantiationPath BestDownPath(Node node) { - var curNode = node; - var curPath = new InstantiationPath(); - curPath.append((Instantiation)node.UserData); - while (curNode.OutEdges.Any()) - { - curPath = AllDownPaths(curPath, curNode, pathSegmentSize).OrderByDescending(path => InstantiationPathScoreFunction(path, false, true)).First(); - curNode = graph.FindNode(curPath.getInstantiations().Last().uniqueID); - } - return curPath; + // TODO + return null; } - private InstantiationPath BestUpPath(Node node, InstantiationPath downPath) + // Similar to BestDownPath but up + public InstantiationPath BestUpPath(Node node, InstantiationPath downPath) { - var curNode = node; - var curPath = downPath; - while (curNode.InEdges.Any()) - { - curPath = AllUpPaths(curPath, curNode, pathSegmentSize).OrderByDescending(path => - { - path.appendWithOverlap(downPath); - return InstantiationPathScoreFunction(path, true, true); - }).First(); - curNode = graph.FindNode(curPath.getInstantiations().First().uniqueID); - } - return curPath; + // TODO + return null; } - private static IEnumerable AllDownPaths(InstantiationPath basePath, Node node, int nodesToGo) - { - if (nodesToGo <= 0 || !node.OutEdges.Any()) return Enumerable.Repeat(basePath, 1); - return node.OutEdges.SelectMany(e => { - var copy = new InstantiationPath(basePath); - copy.append((Instantiation)e.TargetNode.UserData); - return AllDownPaths(copy, e.TargetNode, nodesToGo - 1); - }); + // Return all down patterns found with the bound + public static List> AllDownPattern(Node node, int bound) + { + // TODO + return null; } - private static IEnumerable AllUpPaths(InstantiationPath basePath, Node node, int nodesToGo) - { - if (nodesToGo <= 0 || !node.InEdges.Any()) return Enumerable.Repeat(basePath, 1); - return node.InEdges.SelectMany(e => { - var copy = new InstantiationPath(basePath); - copy.prepend((Instantiation)e.SourceNode.UserData); - return AllUpPaths(copy, e.SourceNode, nodesToGo - 1); - }); + public static List> AllUpPattern(Node node, int bound) + { + // TODO + return null; } - private static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable> loop, Node node, InstantiationPath downPath) + public static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable> loop, Node node, InstantiationPath downPath) { var nodeInst = (Instantiation)node.UserData; if (!loop.Any(inst => inst.Item1 == nodeInst.Quant && inst.Item2 == nodeInst.bindingInfo.fullPattern)) return null; @@ -696,6 +602,12 @@ private static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable> loop, Node node, InstantiationPath downPath) + { + //TODO + return null; + } + private static InstantiationPath ExtendPathUpwardsWithInstantiations(InstantiationPath path, IEnumerable> instantiations, Node node) { if (!instantiations.Any()) return path; From 7c9a9e4c39dd50550da9908017769d88e44cb25e Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 15 Jun 2021 21:51:31 -0700 Subject: [PATCH 04/60] added methods used to creat nodes for testing --- TestProject1/TestGraphs.cs | 47 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 TestProject1/TestGraphs.cs diff --git a/TestProject1/TestGraphs.cs b/TestProject1/TestGraphs.cs new file mode 100644 index 0000000..b4355e9 --- /dev/null +++ b/TestProject1/TestGraphs.cs @@ -0,0 +1,47 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Msagl.Drawing; +using AxiomProfiler; + +namespace AxiomProfiler +{ + // A visulization and explination for the test graphs can be found here + // https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing + class TestGraphs + { + public List Quants; // Quantifiers used in unit tests + public QuantifierModel.BindingInfo Info; // BindingInfo used to make nodes + public Graph graph1; + + public TestGraphs() + { + InitQuantsAndInfo(); + + } + + // initialize 9 quantifiers + private void InitQuantsAndInfo() + { + // initialize Quants + for (int i = 0; i < 9; i++) + { + Quants.Add(new QuantifierModel.Quantifier()); + Quants[i].PrintName = i.ToString(); + } + // initialize Info, with meaningless arguments + QuantifierModel.Term[] args = new QuantifierModel.Term[0]; + QuantifierModel.Term Term = new QuantifierModel.Term("a", args); + Info = new QuantifierModel.BindingInfo(Quants[0], args, args); + } + + private Node MakeNode(String nodeId, int quant) + { + Node node = new Node(nodeId); + QuantifierModel.Instantiation Inst = new QuantifierModel.Instantiation(Info, "a"); + Inst.Quant = Quants[quant]; + node.UserData = Inst; + return node; + } + } +} From 5d421665fb7a208527c3b893721df87c5f16e006 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Wed, 16 Jun 2021 09:27:18 -0700 Subject: [PATCH 05/60] removed test files with wrong framework --- TestProject1/DAGViewTest.cs | 17 -------------- TestProject1/SmallGraphs.cs | 18 -------------- TestProject1/TestGraphs.cs | 47 ------------------------------------- 3 files changed, 82 deletions(-) delete mode 100644 TestProject1/DAGViewTest.cs delete mode 100644 TestProject1/SmallGraphs.cs delete mode 100644 TestProject1/TestGraphs.cs diff --git a/TestProject1/DAGViewTest.cs b/TestProject1/DAGViewTest.cs deleted file mode 100644 index 414ac36..0000000 --- a/TestProject1/DAGViewTest.cs +++ /dev/null @@ -1,17 +0,0 @@ -using Microsoft.VisualStudio.TestTools.UnitTesting; - -namespace AxiomProfiler -{ - [TestClass] - public class DAGViewTest - { - static SmallGraphs graphs = new SmallGraphs(); - static AxiomProfiler axiomprofiler = new AxiomProfiler(); - - [TestMethod] - public void TestMethod1() - { - Assert.AreEqual("a", graphs.graph1.Id); - } - } -} diff --git a/TestProject1/SmallGraphs.cs b/TestProject1/SmallGraphs.cs deleted file mode 100644 index c477784..0000000 --- a/TestProject1/SmallGraphs.cs +++ /dev/null @@ -1,18 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Microsoft.Msagl.Drawing; -using AxiomProfiler; - -namespace TestProject1 -{ - class SmallGraphs - { - public Node graph1; - - public SmallGraphs() - { - graph1 = new Node("a"); - } - } -} diff --git a/TestProject1/TestGraphs.cs b/TestProject1/TestGraphs.cs deleted file mode 100644 index b4355e9..0000000 --- a/TestProject1/TestGraphs.cs +++ /dev/null @@ -1,47 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Microsoft.Msagl.Drawing; -using AxiomProfiler; - -namespace AxiomProfiler -{ - // A visulization and explination for the test graphs can be found here - // https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing - class TestGraphs - { - public List Quants; // Quantifiers used in unit tests - public QuantifierModel.BindingInfo Info; // BindingInfo used to make nodes - public Graph graph1; - - public TestGraphs() - { - InitQuantsAndInfo(); - - } - - // initialize 9 quantifiers - private void InitQuantsAndInfo() - { - // initialize Quants - for (int i = 0; i < 9; i++) - { - Quants.Add(new QuantifierModel.Quantifier()); - Quants[i].PrintName = i.ToString(); - } - // initialize Info, with meaningless arguments - QuantifierModel.Term[] args = new QuantifierModel.Term[0]; - QuantifierModel.Term Term = new QuantifierModel.Term("a", args); - Info = new QuantifierModel.BindingInfo(Quants[0], args, args); - } - - private Node MakeNode(String nodeId, int quant) - { - Node node = new Node(nodeId); - QuantifierModel.Instantiation Inst = new QuantifierModel.Instantiation(Info, "a"); - Inst.Quant = Quants[quant]; - node.UserData = Inst; - return node; - } - } -} From ea50c76039279670745d04b5dc798bac08345d79 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Wed, 16 Jun 2021 09:33:21 -0700 Subject: [PATCH 06/60] test files with correct framework --- UnitTestProject1/TestGraphs.cs | 58 ++++++++++ UnitTestProject1/UnitTest1.cs | 38 ++++++ UnitTestProject1/UnitTestProject1.csproj | 140 +++++++++++++++++++++++ 3 files changed, 236 insertions(+) create mode 100644 UnitTestProject1/TestGraphs.cs create mode 100644 UnitTestProject1/UnitTest1.cs create mode 100644 UnitTestProject1/UnitTestProject1.csproj diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs new file mode 100644 index 0000000..41517ff --- /dev/null +++ b/UnitTestProject1/TestGraphs.cs @@ -0,0 +1,58 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Msagl.Drawing; +using AxiomProfiler; +using AxiomProfiler.QuantifierModel; + +namespace UnitTestProject1 +{ + // A visulization and explination for the test graphs can be found here + // https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing + class TestGraphs + { + public List Quants = new List(); // Quantifiers used in unit tests + public BindingInfo Info; // BindingInfo used to make nodes + public Graph graph1; + public Node node1; + public TestGraphs() + { + InitQuantsAndInfo(); + MakeGraph1(); + node1 = new Node("a"); + } + + // initialize 9 quantifiers + private void InitQuantsAndInfo() + { + // initialize Quants + for (int i = 0; i < 9; i++) + { + Quants.Add(new Quantifier()); + Quants[i].PrintName = i.ToString(); + } + // initialize Info, with meaningless arguments + Term[] args = new Term[0]; + Term Term = new Term("a", args); + Info = new BindingInfo(Quants[0], args, args); + } + + // function that make of node with Id = nodeId, + // and UserDate = a instantiation with quantifier quant + private Node MakeNode(String nodeId, int quant) + { + Node node = new Node(nodeId); + Instantiation Inst = new Instantiation(Info, "a"); + Inst.Quant = Quants[quant]; + node.UserData = Inst; + return node; + } + + //Graph one is graph containing only one node + private void MakeGraph1() + { + graph1 = new Graph(); + graph1.AddNode(MakeNode("A", 0)); + } + } +} diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs new file mode 100644 index 0000000..87905c0 --- /dev/null +++ b/UnitTestProject1/UnitTest1.cs @@ -0,0 +1,38 @@ +using Microsoft.VisualStudio.TestTools.UnitTesting; +using System; +using System.Collections.Generic; +using System.Windows.Forms; +using AxiomProfiler; +using AxiomProfiler.QuantifierModel; +using System; +using System.Collections.Generic; +using System.Linq; +using System.Windows.Forms; +using System.Threading.Tasks; +using Microsoft.Msagl.Core.Routing; +using Microsoft.Msagl.GraphViewerGdi; +using Microsoft.Msagl.Drawing; +using Microsoft.Msagl.Layout.Layered; +using AxiomProfiler.QuantifierModel; + + +namespace UnitTestProject1 +{ + // This test file is created to test some of pathExplanationButton_Click's helper functions + // AllDownPatterns + [TestClass] + public class DAGViewTest + { + static TestGraphs Graphs = new TestGraphs(); + + // The following are tests for AllDownPatterns + + [TestMethod] + public void TestAllDownPatterns1() + { + List> result = DAGView.AllDownPattern(Graphs.graph1.FindNode("a"), 8); + Assert.AreEqual(0, result.Count); + //Assert.AreEqual("a", Graphs.node1.Id); + } + } +} diff --git a/UnitTestProject1/UnitTestProject1.csproj b/UnitTestProject1/UnitTestProject1.csproj new file mode 100644 index 0000000..90cd595 --- /dev/null +++ b/UnitTestProject1/UnitTestProject1.csproj @@ -0,0 +1,140 @@ + + + + + + Debug + AnyCPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC} + Library + Properties + UnitTestProject1 + UnitTestProject1 + v4.5 + 512 + {3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC} + 15.0 + $(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion) + $(ProgramFiles)\Common Files\microsoft shared\VSTT\$(VisualStudioVersion)\UITestExtensionPackages + False + UnitTest + + + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + + + + true + bin\x86\Debug\ + DEBUG;TRACE + full + x86 + 7.3 + prompt + + + bin\x86\Release\ + TRACE + true + pdbonly + x86 + 7.3 + prompt + + + true + bin\x64\Debug\ + DEBUG;TRACE + full + x64 + 7.3 + prompt + + + bin\x64\Release\ + TRACE + true + pdbonly + x64 + 7.3 + prompt + + + + False + ..\lib\Msagl\Microsoft.Msagl.dll + + + False + ..\lib\Msagl\Microsoft.Msagl.Drawing.dll + + + False + ..\lib\Msagl\Microsoft.Msagl.GraphViewerGdi.dll + + + ..\lib\Msagl\Microsoft.Msagl.WpfGraphControl.dll + + + ..\source\packages\MSTest.TestFramework.2.1.2\lib\net45\Microsoft.VisualStudio.TestPlatform.TestFramework.dll + + + ..\source\packages\MSTest.TestFramework.2.1.2\lib\net45\Microsoft.VisualStudio.TestPlatform.TestFramework.Extensions.dll + + + + + + + + + + + + + + + + + + + + + + + + + + {29651769-4a5f-4c7f-baa7-4064ba38324d} + AxiomProfiler + + + + + + + This project references NuGet package(s) that are missing on this computer. Use NuGet Package Restore to download them. For more information, see http://go.microsoft.com/fwlink/?LinkID=322105. The missing file is {0}. + + + + + + \ No newline at end of file From 9c057d83961fee7fea6f8f8f9c5f452f2b686882 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Wed, 16 Jun 2021 17:52:39 -0700 Subject: [PATCH 07/60] change some some function names --- UnitTestProject1/UnitTest1.cs | 2 +- source/DAGView.cs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 87905c0..3ef2eaa 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -30,7 +30,7 @@ public class DAGViewTest [TestMethod] public void TestAllDownPatterns1() { - List> result = DAGView.AllDownPattern(Graphs.graph1.FindNode("a"), 8); + List> result = DAGView.AllDownPatterns(Graphs.graph1.FindNode("a"), 8); Assert.AreEqual(0, result.Count); //Assert.AreEqual("a", Graphs.node1.Id); } diff --git a/source/DAGView.cs b/source/DAGView.cs index 9e20583..8413912 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -579,13 +579,13 @@ public InstantiationPath BestUpPath(Node node, InstantiationPath downPath) } // Return all down patterns found with the bound - public static List> AllDownPattern(Node node, int bound) + public static List> AllDownPatterns(Node node, int bound) { // TODO return null; } - public static List> AllUpPattern(Node node, int bound) + public static List> AllUpPatterns(Node node, int bound) { // TODO return null; From e409638d4717e13951d8012364782598748b3824 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Wed, 16 Jun 2021 22:22:16 -0700 Subject: [PATCH 08/60] AllDownPatterns implmeneted, untested --- UnitTestProject1/UnitTest1.cs | 2 +- source/DAGView.cs | 50 +++++++++++++++++++++++++++++++++-- 2 files changed, 49 insertions(+), 3 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 3ef2eaa..2f83c39 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -30,7 +30,7 @@ public class DAGViewTest [TestMethod] public void TestAllDownPatterns1() { - List> result = DAGView.AllDownPatterns(Graphs.graph1.FindNode("a"), 8); + List> result = DAGView.AllDownPatterns(Graphs.graph1.FindNode("A"), 8); Assert.AreEqual(0, result.Count); //Assert.AreEqual("a", Graphs.node1.Id); } diff --git a/source/DAGView.cs b/source/DAGView.cs index 8413912..f6c1a83 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -580,9 +580,55 @@ public InstantiationPath BestUpPath(Node node, InstantiationPath downPath) // Return all down patterns found with the bound public static List> AllDownPatterns(Node node, int bound) + { + List> Patterns = new List>(); + Quantifier Target = ((Instantiation) node.UserData).Quant; + List CurPattern = new List(); + CurPattern.Add(Target); + Tuple> CurPair = new Tuple>(node, CurPattern); + List>> PathStack= new List>>(); + PathStack.Add(CurPair); + Node CurNode, Child; + Quantifier ChildQuant; + Dictionary seen = new Dictionary(); + + while(PathStack.Count > 0) + { + CurPair = PathStack[PathStack.Count - 1]; + PathStack.RemoveAt(PathStack.Count - 1); + CurNode = CurPair.Item1; + CurPattern = CurPair.Item2; + if (CurPattern.Count > bound) break; + foreach (Edge edge in CurNode.Edges) + { + Child = edge.TargetNode; + ChildQuant = ((Instantiation) Child.UserData).Quant; + if (ChildQuant.Equals(Target)) + { + if (!Patterns.Contains(CurPattern)) + { + Patterns.Add(CurPattern); + } + } else + { + List NewPattern = new List(CurPattern); + NewPattern.Add(ChildQuant); + PathStack.Add(new Tuple>(Child, NewPattern)); + } + } + } + return Patterns; + } + + // Helper function for AllDownPatterns and AllUpPatterns + private string PatternToString(List Pattern) { - // TODO - return null; + string s = ""; + foreach (Quantifier Quant in Pattern) + { + s += Quant.PrintName; + } + return s; } public static List> AllUpPatterns(Node node, int bound) From 9d6516a918399eedfdf1a95ac7d1e218e8f9ab0a Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Thu, 17 Jun 2021 20:08:09 -0700 Subject: [PATCH 09/60] Added Graph to test AllDownPatterns --- UnitTestProject1/TestGraphs.cs | 42 ++++++++++++++++++++++++++++++---- UnitTestProject1/UnitTest1.cs | 22 +++++++++++++++++- 2 files changed, 59 insertions(+), 5 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index 41517ff..10db356 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -9,24 +9,28 @@ namespace UnitTestProject1 { // A visulization and explination for the test graphs can be found here // https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing + // Some graphs class TestGraphs { public List Quants = new List(); // Quantifiers used in unit tests public BindingInfo Info; // BindingInfo used to make nodes public Graph graph1; - public Node node1; + public Graph graph2; + + // Constructor + // Mkae the graphs needsed for testing public TestGraphs() { InitQuantsAndInfo(); MakeGraph1(); - node1 = new Node("a"); + MakeGraph2(); } // initialize 9 quantifiers private void InitQuantsAndInfo() { // initialize Quants - for (int i = 0; i < 9; i++) + for (int i = 0; i < 10; i++) { Quants.Add(new Quantifier()); Quants[i].PrintName = i.ToString(); @@ -48,11 +52,41 @@ private Node MakeNode(String nodeId, int quant) return node; } - //Graph one is graph containing only one node + // Graph1 is graph containing only one node private void MakeGraph1() { graph1 = new Graph(); graph1.AddNode(MakeNode("A", 0)); } + + // Graph2 + private void MakeGraph2() + { + graph2 = new Graph(); + graph2.AddNode(MakeNode("A", 0)); + graph2.AddNode(MakeNode("B", 1)); + graph2.AddNode(MakeNode("C", 2)); + graph2.AddNode(MakeNode("D", 3)); + graph2.AddNode(MakeNode("E", 4)); + graph2.AddNode(MakeNode("F", 5)); + graph2.AddNode(MakeNode("G", 6)); + graph2.AddNode(MakeNode("H", 7)); + graph2.AddNode(MakeNode("I", 8)); + graph2.AddNode(MakeNode("J", 9)); + graph2.AddNode(MakeNode("K", 0)); + graph2.AddNode(MakeNode("L", 0)); + graph2.AddNode(MakeNode("M", 0)); + graph2.AddNode(MakeNode("N", 1)); + char prev = 'A'; + for (char c = 'C'; c <= 'K'; c++) + { + graph2.AddEdge(prev.ToString(), c.ToString()); + prev = c; + } + graph2.AddEdge("A", "B"); + graph2.AddEdge("B", "L"); + graph2.AddEdge("L", "N"); + graph2.AddEdge("A", "M"); + } } } diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 2f83c39..f668d91 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -27,12 +27,32 @@ public class DAGViewTest // The following are tests for AllDownPatterns + // TestAllDownPatterns1 + // Travial Case where the node has no dependent nodes [TestMethod] public void TestAllDownPatterns1() { List> result = DAGView.AllDownPatterns(Graphs.graph1.FindNode("A"), 8); Assert.AreEqual(0, result.Count); - //Assert.AreEqual("a", Graphs.node1.Id); + } + + // Test on bigger graph with minimum bound + [TestMethod] + public void TestAllDownPattern2() + { + List> result = DAGView.AllDownPatterns(Graphs.graph2.FindNode("A"), 1); + Assert.AreEqual(1, result.Count); + Assert.AreEqual(Graphs.Quants[0], result[0][0]); + } + + // Test on bigger graph with default bound + [TestMethod] + public void TestAllDownPattern3() + { + List> result = DAGView.AllDownPatterns(Graphs.graph2.FindNode("A"), 8); + List expected = new List() { Graphs.Quants[0] }; + Console.WriteLine(result.Count.ToString()); + Assert.AreEqual(2, result.Count); } } } From 921ce16589eaa7f73a1bbef23980e93f700a5582 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 18 Jun 2021 13:08:58 -0700 Subject: [PATCH 10/60] improved test cases for AllDownPatterns --- UnitTestProject1/TestGraphs.cs | 9 +++++++++ UnitTestProject1/UnitTest1.cs | 6 ++++-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index 10db356..d58c282 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -52,6 +52,15 @@ private Node MakeNode(String nodeId, int quant) return node; } + public static bool ContainPattern(ref List> patterns, ref List pattern) + { + for (int i = 0; i < patterns.Count; i++) + { + if (patterns[i].SequenceEqual(pattern)) return true; + } + return false; + } + // Graph1 is graph containing only one node private void MakeGraph1() { diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index f668d91..023b119 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -50,9 +50,11 @@ public void TestAllDownPattern2() public void TestAllDownPattern3() { List> result = DAGView.AllDownPatterns(Graphs.graph2.FindNode("A"), 8); - List expected = new List() { Graphs.Quants[0] }; - Console.WriteLine(result.Count.ToString()); + List expected1 = new List() { Graphs.Quants[0] }; + List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1]}; Assert.AreEqual(2, result.Count); + Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected1)); + Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected2)); } } } From 3fc2d3e06b18d009685c985ba25d9fc91db33da6 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 18 Jun 2021 13:17:17 -0700 Subject: [PATCH 11/60] AllDownPatterns debugges --- source/DAGView.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index f6c1a83..a785538 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -599,7 +599,7 @@ public static List> AllDownPatterns(Node node, int bound) CurNode = CurPair.Item1; CurPattern = CurPair.Item2; if (CurPattern.Count > bound) break; - foreach (Edge edge in CurNode.Edges) + foreach (Edge edge in CurNode.OutEdges) { Child = edge.TargetNode; ChildQuant = ((Instantiation) Child.UserData).Quant; From 876b375c26569bd8bf2a3eef44381eb653b272a8 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 18 Jun 2021 17:55:17 -0700 Subject: [PATCH 12/60] added test graph 3 --- UnitTestProject1/TestGraphs.cs | 22 ++++++++++++++++++++-- UnitTestProject1/UnitTest1.cs | 12 +++++++++++- 2 files changed, 31 insertions(+), 3 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index d58c282..885fa04 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -14,8 +14,7 @@ class TestGraphs { public List Quants = new List(); // Quantifiers used in unit tests public BindingInfo Info; // BindingInfo used to make nodes - public Graph graph1; - public Graph graph2; + public Graph graph1, graph2, graph3; // Constructor // Mkae the graphs needsed for testing @@ -24,6 +23,7 @@ public TestGraphs() InitQuantsAndInfo(); MakeGraph1(); MakeGraph2(); + MakeGraph3(); } // initialize 9 quantifiers @@ -97,5 +97,23 @@ private void MakeGraph2() graph2.AddEdge("L", "N"); graph2.AddEdge("A", "M"); } + + private void MakeGraph3() + { + graph3 = new Graph(); + graph3.AddNode(MakeNode("A", 0)); + graph3.AddNode(MakeNode("B", 1)); + graph3.AddNode(MakeNode("C", 1)); + graph3.AddNode(MakeNode("D", 0)); + graph3.AddNode(MakeNode("E", 0)); + graph3.AddNode(MakeNode("F", 0)); + graph3.AddNode(MakeNode("G", 0)); + graph3.AddEdge("A", "B"); + graph3.AddEdge("A", "C"); + graph3.AddEdge("B", "D"); + graph3.AddEdge("B", "E"); + graph3.AddEdge("C", "F"); + graph3.AddEdge("C", "G"); + } } } diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 023b119..3713042 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -51,10 +51,20 @@ public void TestAllDownPattern3() { List> result = DAGView.AllDownPatterns(Graphs.graph2.FindNode("A"), 8); List expected1 = new List() { Graphs.Quants[0] }; - List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1]}; + List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; Assert.AreEqual(2, result.Count); Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected1)); Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected2)); } + + // Test that AllDownPatterns return unique patterns + [TestMethod] + public void TestAllDownPattern4() + { + List> result = DAGView.AllDownPatterns(Graphs.graph3.FindNode("A"), 8); + List expected = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + Assert.AreEqual(1, result.Count); + Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected)); + } } } From 479a6370db1b23c3a45e71f0036f735caedd2a75 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 18 Jun 2021 18:01:31 -0700 Subject: [PATCH 13/60] refactoed ContainPattern to DAGView.cs --- UnitTestProject1/TestGraphs.cs | 9 --------- source/DAGView.cs | 11 ++++++++++- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index 885fa04..112d8c8 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -52,15 +52,6 @@ private Node MakeNode(String nodeId, int quant) return node; } - public static bool ContainPattern(ref List> patterns, ref List pattern) - { - for (int i = 0; i < patterns.Count; i++) - { - if (patterns[i].SequenceEqual(pattern)) return true; - } - return false; - } - // Graph1 is graph containing only one node private void MakeGraph1() { diff --git a/source/DAGView.cs b/source/DAGView.cs index a785538..4932600 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -605,7 +605,7 @@ public static List> AllDownPatterns(Node node, int bound) ChildQuant = ((Instantiation) Child.UserData).Quant; if (ChildQuant.Equals(Target)) { - if (!Patterns.Contains(CurPattern)) + if (!ContainPattern(ref Patterns, ref CurPattern)) { Patterns.Add(CurPattern); } @@ -675,6 +675,15 @@ private static InstantiationPath ExtendPathUpwardsWithInstantiations(Instantiati return bestPath; } + public static bool ContainPattern(ref List> patterns, ref List pattern) + { + for (int i = 0; i < patterns.Count; i++) + { + if (patterns[i].SequenceEqual(pattern)) return true; + } + return false; + } + private void highlightPath(InstantiationPath path) { if (previouslySelectedNode != null || highlightedNodes.Count != 0) From c6e2a450455ae02a5cf4cb48c5d4369c8628226d Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 18 Jun 2021 18:04:17 -0700 Subject: [PATCH 14/60] removed unecessary 'using' tags' --- UnitTestProject1/TestGraphs.cs | 2 -- UnitTestProject1/UnitTest1.cs | 18 +++--------------- 2 files changed, 3 insertions(+), 17 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index 112d8c8..6d1a345 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -1,8 +1,6 @@ using System; using System.Collections.Generic; -using System.Linq; using Microsoft.Msagl.Drawing; -using AxiomProfiler; using AxiomProfiler.QuantifierModel; namespace UnitTestProject1 diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 3713042..dff3b21 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -1,20 +1,8 @@ using Microsoft.VisualStudio.TestTools.UnitTesting; using System; using System.Collections.Generic; -using System.Windows.Forms; using AxiomProfiler; using AxiomProfiler.QuantifierModel; -using System; -using System.Collections.Generic; -using System.Linq; -using System.Windows.Forms; -using System.Threading.Tasks; -using Microsoft.Msagl.Core.Routing; -using Microsoft.Msagl.GraphViewerGdi; -using Microsoft.Msagl.Drawing; -using Microsoft.Msagl.Layout.Layered; -using AxiomProfiler.QuantifierModel; - namespace UnitTestProject1 { @@ -53,8 +41,8 @@ public void TestAllDownPattern3() List expected1 = new List() { Graphs.Quants[0] }; List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; Assert.AreEqual(2, result.Count); - Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected1)); - Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected2)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected2)); } // Test that AllDownPatterns return unique patterns @@ -64,7 +52,7 @@ public void TestAllDownPattern4() List> result = DAGView.AllDownPatterns(Graphs.graph3.FindNode("A"), 8); List expected = new List() { Graphs.Quants[0], Graphs.Quants[1] }; Assert.AreEqual(1, result.Count); - Assert.IsTrue(TestGraphs.ContainPattern(ref result, ref expected)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); } } } From 5e07ee7af26ab101cf3286373fffe25afbd94e1c Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 19 Jun 2021 15:13:42 -0700 Subject: [PATCH 15/60] created test cases for ExtendDownWards --- UnitTestProject1/TestGraphs.cs | 20 ++++--- UnitTestProject1/UnitTest1.cs | 95 ++++++++++++++++++++++++++++++++-- source/DAGView.cs | 5 +- 3 files changed, 106 insertions(+), 14 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index 6d1a345..ce87005 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -12,7 +12,7 @@ class TestGraphs { public List Quants = new List(); // Quantifiers used in unit tests public BindingInfo Info; // BindingInfo used to make nodes - public Graph graph1, graph2, graph3; + public Graph graph1, graph2, graph3, graph4; // Constructor // Mkae the graphs needsed for testing @@ -95,14 +95,18 @@ private void MakeGraph3() graph3.AddNode(MakeNode("C", 1)); graph3.AddNode(MakeNode("D", 0)); graph3.AddNode(MakeNode("E", 0)); - graph3.AddNode(MakeNode("F", 0)); - graph3.AddNode(MakeNode("G", 0)); + graph3.AddNode(MakeNode("F", 1)); + graph3.AddNode(MakeNode("G", 1)); + graph3.AddNode(MakeNode("H", 0)); + graph3.AddNode(MakeNode("I", 0)); graph3.AddEdge("A", "B"); graph3.AddEdge("A", "C"); - graph3.AddEdge("B", "D"); - graph3.AddEdge("B", "E"); - graph3.AddEdge("C", "F"); - graph3.AddEdge("C", "G"); + graph3.AddEdge("C", "D"); + graph3.AddEdge("C", "E"); + graph3.AddEdge("E", "F"); + graph3.AddEdge("E", "G"); + graph3.AddEdge("G", "H"); + graph3.AddEdge("G", "I"); } - } + } } diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index dff3b21..053f166 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -3,18 +3,17 @@ using System.Collections.Generic; using AxiomProfiler; using AxiomProfiler.QuantifierModel; +using Microsoft.Msagl.Drawing; namespace UnitTestProject1 { // This test file is created to test some of pathExplanationButton_Click's helper functions // AllDownPatterns [TestClass] - public class DAGViewTest + public class AllDownPatternsTest { static TestGraphs Graphs = new TestGraphs(); - // The following are tests for AllDownPatterns - // TestAllDownPatterns1 // Travial Case where the node has no dependent nodes [TestMethod] @@ -29,8 +28,9 @@ public void TestAllDownPatterns1() public void TestAllDownPattern2() { List> result = DAGView.AllDownPatterns(Graphs.graph2.FindNode("A"), 1); + List expected = new List() { Graphs.Quants[0] }; Assert.AreEqual(1, result.Count); - Assert.AreEqual(Graphs.Quants[0], result[0][0]); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); } // Test on bigger graph with default bound @@ -55,4 +55,91 @@ public void TestAllDownPattern4() Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); } } + + [TestClass] + public class ExtendDownardsWithPattern + { + static TestGraphs Graphs = new TestGraphs(); + + // trivial case graph with one node a a pattern + [TestMethod] + public void TestExtenDownwardsWithPattern1() + { + List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List result = + DAGView.ExtendDownwards(Graphs.graph1.FindNode("A"), ref pattern, 10); + Assert.AreEqual(1, result.Count); + } + + // small pattern with bound larger then the path + // on graph 2, with pattern [Quantifier 0] + [TestMethod] + public void TestExtendDownwardsWithPattern2() + { + List pattern = new List() { Graphs.Quants[0]}; + List result = + DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, 3); + List expected = new List() { "A", "M" }; + Assert.AreEqual(expected.Count, result.Count); + for (int i = 0; i < expected.Count; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + } + + // Pattern of size 2 and bound of size 4 (the entire path) + // on graph2, with the pattern [Quantifier 0, Quantifier 1] + [TestMethod] + public void TestExtendDownwardsWithPattern3() + { + List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List result = + DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, 4); + List expected = new List() { "A", "B", "L", "N" }; + Assert.AreEqual(expected.Count, result.Count); + for (int i = 0; i < expected.Count; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + } + + // Pattern of size 9, but bound to 6 (won't complete a cycle) + // on graph2, with the pattern + // [Quantifier 0, Quantifier 2, Quantifier3, ... , Quantifier 9] + [TestMethod] + public void TestExtendDownWardsWithPattern3() + { + List pattern = + new List() { Graphs.Quants[0], Graphs.Quants[2], Graphs.Quants[3], + Graphs.Quants[4], Graphs.Quants[5], Graphs.Quants[6], Graphs.Quants[7], + Graphs.Quants[8], Graphs.Quants[9]}; + List result = + DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, 6); + List expected = new List() { "A", "C", "D", "E", "F", "G" }; + Assert.AreEqual(expected.Count, result.Count); + for (int i= 0; i < expected.Count; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + } + + // Pattern of size 2, bound of 10 + // on grpah 3 with the patter [Quantifier 0, Quantifier 1] + // For ever node, if possible, always choose a child that can be extended one more time. + [TestMethod] + public void TestExtendDownWardsWithPattern4() + { + List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List result = + DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, 10); + List expected = + new List() { "A", "C", "E", "G" }; + Assert.AreEqual(5, result.Count); + for (int i = 0; i < 4; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + Assert.IsTrue((result[4].Id == "H") | (result[4].Id == "I")); + } + } } diff --git a/source/DAGView.cs b/source/DAGView.cs index 4932600..813023f 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -648,10 +648,11 @@ public static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable> loop, Node node, InstantiationPath downPath) + public static List ExtendDownwards(Node node, ref List Pattern, int bound) { + List path = new List(); //TODO - return null; + return path; } private static InstantiationPath ExtendPathUpwardsWithInstantiations(InstantiationPath path, IEnumerable> instantiations, Node node) From 1fc8686890731075e1ef8e600437515f8bbeffbd Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 19 Jun 2021 15:32:12 -0700 Subject: [PATCH 16/60] add unlimited case for ExtendDownwards --- UnitTestProject1/UnitTest1.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 053f166..0e9da09 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -123,7 +123,7 @@ public void TestExtendDownWardsWithPattern3() } } - // Pattern of size 2, bound of 10 + // Pattern of size 2, bound of -1 (unlimited, goes as further as it can) // on grpah 3 with the patter [Quantifier 0, Quantifier 1] // For ever node, if possible, always choose a child that can be extended one more time. [TestMethod] @@ -131,7 +131,7 @@ public void TestExtendDownWardsWithPattern4() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; List result = - DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, 10); + DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, -1); List expected = new List() { "A", "C", "E", "G" }; Assert.AreEqual(5, result.Count); From 5100f7c547ea8246f5a2b5ba404044d26948a024 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 19 Jun 2021 17:03:56 -0700 Subject: [PATCH 17/60] typo fix --- UnitTestProject1/UnitTest1.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 0e9da09..16ab00e 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -125,7 +125,7 @@ public void TestExtendDownWardsWithPattern3() // Pattern of size 2, bound of -1 (unlimited, goes as further as it can) // on grpah 3 with the patter [Quantifier 0, Quantifier 1] - // For ever node, if possible, always choose a child that can be extended one more time. + // For every node, if possible, always choose a child that can be extended one more time. [TestMethod] public void TestExtendDownWardsWithPattern4() { From 5963a12ebe0ae27a9e0084cff460e5f5b1cd9d7e Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 09:25:53 -0700 Subject: [PATCH 18/60] ExtendDownwards implemented --- UnitTestProject1/UnitTest1.cs | 2 +- source/DAGView.cs | 35 +++++++++++++++++++++++++++++++++-- 2 files changed, 34 insertions(+), 3 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 16ab00e..c1416b1 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -131,7 +131,7 @@ public void TestExtendDownWardsWithPattern4() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; List result = - DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, -1); + DAGView.ExtendDownwards(Graphs.graph3.FindNode("A"), ref pattern, -1); List expected = new List() { "A", "C", "E", "G" }; Assert.AreEqual(5, result.Count); diff --git a/source/DAGView.cs b/source/DAGView.cs index 813023f..0a04c6a 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -650,8 +650,39 @@ public static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable ExtendDownwards(Node node, ref List Pattern, int bound) { - List path = new List(); - //TODO + List path = new List() { node }; + Node LastNode = node, CurNode, Child, Grandchild; + int PatternIndex = 0, NextQuant; + bool HaveGoodChild = false; + while(true) + { + LoopBegin: + PatternIndex = (PatternIndex + 1) % Pattern.Count; + CurNode = path[path.Count - 1]; + HaveGoodChild = false; + if ((bound > 0) & (path.Count == bound)) break; + foreach (Edge edge in CurNode.OutEdges) + { + Child = edge.TargetNode; + if (((Instantiation) Child.UserData).Quant.PrintName == Pattern[PatternIndex].PrintName) + { + HaveGoodChild = true; + LastNode = Child; + NextQuant = (PatternIndex + 1) % Pattern.Count; + foreach (Edge edge2 in Child.OutEdges) + { + Grandchild = edge2.TargetNode; + if (((Instantiation) Grandchild.UserData).Quant.PrintName == Pattern[NextQuant].PrintName) + { + path.Add(Child); + goto LoopBegin; + } + } + } + } + if (HaveGoodChild) path.Add(LastNode); + break; + } return path; } From b4ef1ea4429b4298df0d018bcbc6da40559cd715 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 10:02:09 -0700 Subject: [PATCH 19/60] Test cases added for AllUpPatterns --- UnitTestProject1/TestGraphs.cs | 58 ++++++++++++++++++++++++++++++++-- UnitTestProject1/UnitTest1.cs | 47 +++++++++++++++++++++++++++ source/DAGView.cs | 14 ++------ 3 files changed, 105 insertions(+), 14 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index ce87005..ac7962a 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -12,7 +12,7 @@ class TestGraphs { public List Quants = new List(); // Quantifiers used in unit tests public BindingInfo Info; // BindingInfo used to make nodes - public Graph graph1, graph2, graph3, graph4; + public Graph graph1, graph2, graph3, graph4, graph5; // Constructor // Mkae the graphs needsed for testing @@ -22,6 +22,8 @@ public TestGraphs() MakeGraph1(); MakeGraph2(); MakeGraph3(); + MakeGraph4(); + MakeGraph5(); } // initialize 9 quantifiers @@ -108,5 +110,57 @@ private void MakeGraph3() graph3.AddEdge("G", "H"); graph3.AddEdge("G", "I"); } - } + + private void MakeGraph4() + { + graph4 = new Graph(); + graph4.AddNode(MakeNode("A", 0)); + graph4.AddNode(MakeNode("B", 1)); + graph4.AddNode(MakeNode("C", 2)); + graph4.AddNode(MakeNode("D", 3)); + graph4.AddNode(MakeNode("E", 4)); + graph4.AddNode(MakeNode("F", 5)); + graph4.AddNode(MakeNode("G", 6)); + graph4.AddNode(MakeNode("H", 7)); + graph4.AddNode(MakeNode("I", 8)); + graph4.AddNode(MakeNode("J", 9)); + graph4.AddNode(MakeNode("K", 0)); + graph4.AddNode(MakeNode("L", 0)); + graph4.AddNode(MakeNode("M", 0)); + graph2.AddNode(MakeNode("N", 1)); + char prev = 'K'; + for (char c = 'J'; c >= 'C'; c--) + { + graph4.AddEdge(prev.ToString(), c.ToString()); + prev = c; + } + graph4.AddEdge("C", "A"); + graph4.AddEdge("B", "A"); + graph4.AddEdge("L", "B"); + graph4.AddEdge("N", "L"); + graph4.AddEdge("M", "A"); + } + + private void MakeGraph5() + { + graph5 = new Graph(); + graph5.AddNode(MakeNode("A", 0)); + graph5.AddNode(MakeNode("B", 1)); + graph5.AddNode(MakeNode("C", 1)); + graph5.AddNode(MakeNode("D", 0)); + graph5.AddNode(MakeNode("E", 0)); + graph5.AddNode(MakeNode("F", 1)); + graph5.AddNode(MakeNode("G", 1)); + graph5.AddNode(MakeNode("H", 0)); + graph5.AddNode(MakeNode("I", 0)); + graph5.AddEdge("B", "A"); + graph5.AddEdge("C", "A"); + graph5.AddEdge("D", "C"); + graph5.AddEdge("E", "C"); + graph5.AddEdge("F", "E"); + graph5.AddEdge("G", "E"); + graph5.AddEdge("H", "G"); + graph5.AddEdge("I", "G"); + } + } } diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index c1416b1..44a7ab7 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -142,4 +142,51 @@ public void TestExtendDownWardsWithPattern4() Assert.IsTrue((result[4].Id == "H") | (result[4].Id == "I")); } } + + // similar tests with AllDownPattern but with reversed graph + [TestClass] + public class AllUpPatternsTest + { + static TestGraphs Graphs = new TestGraphs(); + + // Travial Case where the node has no dependent nodes + [TestMethod] + public void TestAllUpPatterns1() + { + List> result = DAGView.AllDownPatterns(Graphs.graph1.FindNode("A"), 8); + Assert.AreEqual(0, result.Count); + } + + // Test on bigger graph with minimum bound + [TestMethod] + public void TestAllUpPattern2() + { + List> result = DAGView.AllUpPatterns(Graphs.graph4.FindNode("A"), 1); + List expected = new List() { Graphs.Quants[0] }; + Assert.AreEqual(1, result.Count); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); + } + + // Test on bigger graph with default bound + [TestMethod] + public void TestAllUpPattern3() + { + List> result = DAGView.AllUpPatterns(Graphs.graph4.FindNode("A"), 8); + List expected1 = new List() { Graphs.Quants[0] }; + List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + Assert.AreEqual(2, result.Count); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected2)); + } + + // Test that AllDownPatterns return unique patterns + [TestMethod] + public void TestAllUpPattern4() + { + List> result = DAGView.AllUpPatterns(Graphs.graph5.FindNode("A"), 8); + List expected = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + Assert.AreEqual(1, result.Count); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); + } + } } diff --git a/source/DAGView.cs b/source/DAGView.cs index 0a04c6a..97e6148 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -620,21 +620,11 @@ public static List> AllDownPatterns(Node node, int bound) return Patterns; } - // Helper function for AllDownPatterns and AllUpPatterns - private string PatternToString(List Pattern) - { - string s = ""; - foreach (Quantifier Quant in Pattern) - { - s += Quant.PrintName; - } - return s; - } - public static List> AllUpPatterns(Node node, int bound) { + List> patterns = new List>(); // TODO - return null; + return patterns; } public static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable> loop, Node node, InstantiationPath downPath) From 971e0fb0e9f9ed6c99cf93bf431452c31453135a Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 10:10:58 -0700 Subject: [PATCH 20/60] AllUpPatterns implemented --- source/DAGView.cs | 41 +++++++++++++++++++++++++++++++++++++---- 1 file changed, 37 insertions(+), 4 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 97e6148..3529178 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -590,7 +590,6 @@ public static List> AllDownPatterns(Node node, int bound) PathStack.Add(CurPair); Node CurNode, Child; Quantifier ChildQuant; - Dictionary seen = new Dictionary(); while(PathStack.Count > 0) { @@ -622,9 +621,43 @@ public static List> AllDownPatterns(Node node, int bound) public static List> AllUpPatterns(Node node, int bound) { - List> patterns = new List>(); - // TODO - return patterns; + List> Patterns = new List>(); + Quantifier Target = ((Instantiation)node.UserData).Quant; + List CurPattern = new List(); + CurPattern.Add(Target); + Tuple> CurPair = new Tuple>(node, CurPattern); + List>> PathStack = new List>>(); + PathStack.Add(CurPair); + Node CurNode, Child; + Quantifier ChildQuant; + + while (PathStack.Count > 0) + { + CurPair = PathStack[PathStack.Count - 1]; + PathStack.RemoveAt(PathStack.Count - 1); + CurNode = CurPair.Item1; + CurPattern = CurPair.Item2; + if (CurPattern.Count > bound) break; + foreach (Edge edge in CurNode.InEdges) + { + Child = edge.SourceNode; + ChildQuant = ((Instantiation)Child.UserData).Quant; + if (ChildQuant.Equals(Target)) + { + if (!ContainPattern(ref Patterns, ref CurPattern)) + { + Patterns.Add(CurPattern); + } + } + else + { + List NewPattern = new List(CurPattern); + NewPattern.Add(ChildQuant); + PathStack.Add(new Tuple>(Child, NewPattern)); + } + } + } + return Patterns; } public static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable> loop, Node node, InstantiationPath downPath) From 9c0389cab3e618e43a4268a60f2562ede9286b0a Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 10:15:20 -0700 Subject: [PATCH 21/60] naming fixes --- UnitTestProject1/UnitTest1.cs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 44a7ab7..e88dd32 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -57,13 +57,13 @@ public void TestAllDownPattern4() } [TestClass] - public class ExtendDownardsWithPattern + public class ExtendDownards { static TestGraphs Graphs = new TestGraphs(); // trivial case graph with one node a a pattern [TestMethod] - public void TestExtenDownwardsWithPattern1() + public void TestExtenDownwards1() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; List result = @@ -74,7 +74,7 @@ public void TestExtenDownwardsWithPattern1() // small pattern with bound larger then the path // on graph 2, with pattern [Quantifier 0] [TestMethod] - public void TestExtendDownwardsWithPattern2() + public void TestExtendDownwards2() { List pattern = new List() { Graphs.Quants[0]}; List result = @@ -90,7 +90,7 @@ public void TestExtendDownwardsWithPattern2() // Pattern of size 2 and bound of size 4 (the entire path) // on graph2, with the pattern [Quantifier 0, Quantifier 1] [TestMethod] - public void TestExtendDownwardsWithPattern3() + public void TestExtendDownwards3() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; List result = @@ -107,7 +107,7 @@ public void TestExtendDownwardsWithPattern3() // on graph2, with the pattern // [Quantifier 0, Quantifier 2, Quantifier3, ... , Quantifier 9] [TestMethod] - public void TestExtendDownWardsWithPattern3() + public void TestExtendDownWards4() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[2], Graphs.Quants[3], @@ -127,7 +127,7 @@ public void TestExtendDownWardsWithPattern3() // on grpah 3 with the patter [Quantifier 0, Quantifier 1] // For every node, if possible, always choose a child that can be extended one more time. [TestMethod] - public void TestExtendDownWardsWithPattern4() + public void TestExtendDownWards5() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; List result = From 8a31b1d11bcf1e31c8fb24818c2eb619afd746e4 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 10:19:53 -0700 Subject: [PATCH 22/60] tests added for ExtendUpwards --- UnitTestProject1/UnitTest1.cs | 89 +++++++++++++++++++++++++++++++++++ source/DAGView.cs | 78 +++--------------------------- 2 files changed, 95 insertions(+), 72 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index e88dd32..07f28ec 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -189,4 +189,93 @@ public void TestAllUpPattern4() Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); } } + + // Similar to ExtendDownwards, but up + [TestClass] + public class ExtendUpwards + { + static TestGraphs Graphs = new TestGraphs(); + + // trivial case graph with one node a a pattern + [TestMethod] + public void TestExtenUpwards1() + { + List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List result = + DAGView.ExtendUpwards(Graphs.graph1.FindNode("A"), ref pattern, 10); + Assert.AreEqual(1, result.Count); + } + + // small pattern with bound larger then the path + // on graph 2, with pattern [Quantifier 0] + [TestMethod] + public void TestExtendUpards2() + { + List pattern = new List() { Graphs.Quants[0] }; + List result = + DAGView.ExtendUpwards(Graphs.graph2.FindNode("A"), ref pattern, 3); + List expected = new List() { "A", "M" }; + Assert.AreEqual(expected.Count, result.Count); + for (int i = 0; i < expected.Count; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + } + + // Pattern of size 2 and bound of size 4 (the entire path) + // on graph2, with the pattern [Quantifier 0, Quantifier 1] + [TestMethod] + public void TestExtendUpwards3() + { + List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List result = + DAGView.ExtendUpwards(Graphs.graph2.FindNode("A"), ref pattern, 4); + List expected = new List() { "A", "B", "L", "N" }; + Assert.AreEqual(expected.Count, result.Count); + for (int i = 0; i < expected.Count; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + } + + // Pattern of size 9, but bound to 6 (won't complete a cycle) + // on graph2, with the pattern + // [Quantifier 0, Quantifier 2, Quantifier3, ... , Quantifier 9] + [TestMethod] + public void TestExtendUpWards4() + { + List pattern = + new List() { Graphs.Quants[0], Graphs.Quants[2], Graphs.Quants[3], + Graphs.Quants[4], Graphs.Quants[5], Graphs.Quants[6], Graphs.Quants[7], + Graphs.Quants[8], Graphs.Quants[9]}; + List result = + DAGView.ExtendUpwards(Graphs.graph2.FindNode("A"), ref pattern, 6); + List expected = new List() { "A", "C", "D", "E", "F", "G" }; + Assert.AreEqual(expected.Count, result.Count); + for (int i = 0; i < expected.Count; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + } + + // Pattern of size 2, bound of -1 (unlimited, goes as further as it can) + // on grpah 3 with the patter [Quantifier 0, Quantifier 1] + // For every node, if possible, always choose a child that can be extended one more time. + [TestMethod] + public void TestExtendUpWards5() + { + List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List result = + DAGView.ExtendUpwards(Graphs.graph3.FindNode("A"), ref pattern, -1); + List expected = + new List() { "A", "C", "E", "G" }; + Assert.AreEqual(5, result.Count); + for (int i = 0; i < 4; i++) + { + Assert.AreEqual(expected[i], result[i].Id); + } + Assert.IsTrue((result[4].Id == "H") | (result[4].Id == "I")); + } + } + } diff --git a/source/DAGView.cs b/source/DAGView.cs index 3529178..25dfd43 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -486,48 +486,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) try { #endif - _z3AxiomProfiler.DisplayMessage("Finding best path for generalization..."); - - // building path downwards: - var bestDownPath = BestDownPath(previouslySelectedNode); - InstantiationPath bestUpPath; - if (bestDownPath.TryGetLoop(out var loop)) - { - bestUpPath = ExtendPathUpwardsWithLoop(loop, previouslySelectedNode, bestDownPath); - if (bestUpPath == null) - { - bestUpPath = BestUpPath(previouslySelectedNode, bestDownPath); - } - } - else - { - bestUpPath = BestUpPath(previouslySelectedNode, bestDownPath); - } - - List toRemove; - if (bestUpPath.TryGetCyclePath(out var cyclePath)) - { - highlightPath(cyclePath); - _z3AxiomProfiler.UpdateSync(cyclePath); - toRemove = cyclePath.GetInstnationsUnusedInGeneralization(); - } - else - { - highlightPath(bestUpPath); - _z3AxiomProfiler.UpdateSync(bestUpPath); - toRemove = bestUpPath.GetInstnationsUnusedInGeneralization(); - } - - // Stop highlighting nodes that weren't used in the generalization. - foreach (var inst in toRemove) - { - var node = graph.FindNode(inst.uniqueID); - if (node != null) - { - formatNode(node); - } - } - _viewer.Invalidate(); + // TODO #if !DEBUG } catch (Exception exception) @@ -660,17 +619,6 @@ public static List> AllUpPatterns(Node node, int bound) return Patterns; } - public static InstantiationPath ExtendPathUpwardsWithLoop(IEnumerable> loop, Node node, InstantiationPath downPath) - { - var nodeInst = (Instantiation)node.UserData; - if (!loop.Any(inst => inst.Item1 == nodeInst.Quant && inst.Item2 == nodeInst.bindingInfo.fullPattern)) return null; - loop = loop.Reverse().RepeatIndefinietly(); - loop = loop.SkipWhile(inst => inst.Item1 != nodeInst.Quant || inst.Item2 != nodeInst.bindingInfo.fullPattern); - var res = ExtendPathUpwardsWithInstantiations(new InstantiationPath(), loop, node); - res.appendWithOverlap(downPath); - return res; - } - public static List ExtendDownwards(Node node, ref List Pattern, int bound) { List path = new List() { node }; @@ -709,25 +657,11 @@ public static List ExtendDownwards(Node node, ref List Pattern return path; } - private static InstantiationPath ExtendPathUpwardsWithInstantiations(InstantiationPath path, IEnumerable> instantiations, Node node) - { - if (!instantiations.Any()) return path; - var instantiation = instantiations.First(); - var nodeInst = (Instantiation)node.UserData; - if (instantiation.Item1 != nodeInst.Quant || instantiation.Item2 != nodeInst.bindingInfo.fullPattern) return path; - var extendedPath = new InstantiationPath(path); - extendedPath.prepend(nodeInst); - var bestPath = extendedPath; - var remainingInstantiations = instantiations.Skip(1); - foreach (var predecessor in node.InEdges) - { - var candidatePath = ExtendPathUpwardsWithInstantiations(extendedPath, remainingInstantiations, predecessor.SourceNode); - if (candidatePath.Length() > bestPath.Length()) - { - bestPath = candidatePath; - } - } - return bestPath; + public static List ExtendUpwards(Node node, ref List Pattern, int bound) + { + List path = new List() { node }; + // TODO + return path; } public static bool ContainPattern(ref List> patterns, ref List pattern) From b11d3abfb7995e5cd65ea074dc03c16ec3ce3932 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 10:24:15 -0700 Subject: [PATCH 23/60] test case error fixes --- UnitTestProject1/UnitTest1.cs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 07f28ec..4210d2d 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -213,7 +213,7 @@ public void TestExtendUpards2() { List pattern = new List() { Graphs.Quants[0] }; List result = - DAGView.ExtendUpwards(Graphs.graph2.FindNode("A"), ref pattern, 3); + DAGView.ExtendUpwards(Graphs.graph4.FindNode("A"), ref pattern, 3); List expected = new List() { "A", "M" }; Assert.AreEqual(expected.Count, result.Count); for (int i = 0; i < expected.Count; i++) @@ -229,7 +229,7 @@ public void TestExtendUpwards3() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; List result = - DAGView.ExtendUpwards(Graphs.graph2.FindNode("A"), ref pattern, 4); + DAGView.ExtendUpwards(Graphs.graph4.FindNode("A"), ref pattern, 4); List expected = new List() { "A", "B", "L", "N" }; Assert.AreEqual(expected.Count, result.Count); for (int i = 0; i < expected.Count; i++) @@ -249,7 +249,7 @@ public void TestExtendUpWards4() Graphs.Quants[4], Graphs.Quants[5], Graphs.Quants[6], Graphs.Quants[7], Graphs.Quants[8], Graphs.Quants[9]}; List result = - DAGView.ExtendUpwards(Graphs.graph2.FindNode("A"), ref pattern, 6); + DAGView.ExtendUpwards(Graphs.graph4.FindNode("A"), ref pattern, 6); List expected = new List() { "A", "C", "D", "E", "F", "G" }; Assert.AreEqual(expected.Count, result.Count); for (int i = 0; i < expected.Count; i++) @@ -266,7 +266,7 @@ public void TestExtendUpWards5() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; List result = - DAGView.ExtendUpwards(Graphs.graph3.FindNode("A"), ref pattern, -1); + DAGView.ExtendUpwards(Graphs.graph5.FindNode("A"), ref pattern, -1); List expected = new List() { "A", "C", "E", "G" }; Assert.AreEqual(5, result.Count); From 4ba70808eeb66559d5bcedf2b5c70c98660825ba Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 10:59:55 -0700 Subject: [PATCH 24/60] ExtendUpwards implemented --- UnitTestProject1/TestGraphs.cs | 2 +- source/DAGView.cs | 100 ++++++++++++++++++++++----------- 2 files changed, 69 insertions(+), 33 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index ac7962a..e540f27 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -127,7 +127,7 @@ private void MakeGraph4() graph4.AddNode(MakeNode("K", 0)); graph4.AddNode(MakeNode("L", 0)); graph4.AddNode(MakeNode("M", 0)); - graph2.AddNode(MakeNode("N", 1)); + graph4.AddNode(MakeNode("N", 1)); char prev = 'K'; for (char c = 'J'; c >= 'C'; c--) { diff --git a/source/DAGView.cs b/source/DAGView.cs index 25dfd43..faa5b39 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -1,17 +1,16 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Windows.Forms; -using System.Threading.Tasks; +using AxiomProfiler.QuantifierModel; using Microsoft.Msagl.Core.Routing; -using Microsoft.Msagl.GraphViewerGdi; using Microsoft.Msagl.Drawing; +using Microsoft.Msagl.GraphViewerGdi; using Microsoft.Msagl.Layout.Layered; -using AxiomProfiler.QuantifierModel; +using System; +using System.Collections.Generic; +using System.Linq; +using System.Threading.Tasks; +using System.Windows.Forms; using Color = Microsoft.Msagl.Drawing.Color; using MouseButtons = System.Windows.Forms.MouseButtons; using Size = System.Drawing.Size; -using AxiomProfiler.Utilities; namespace AxiomProfiler { @@ -159,8 +158,8 @@ private void redrawGraph_Click(object sender, EventArgs e) } private Color getColor(Quantifier quant) - { - //Hard coded colors for generating screenshots for the paper + { + //Hard coded colors for generating screenshots for the paper /*switch (quant.Qid) { case "sortedness": return Color.Green; @@ -168,14 +167,14 @@ private Color getColor(Quantifier quant) return Color.Yellow; case "injectivity": return Color.Purple; - default:*/ - if (!colorMap.TryGetValue(quant, out var color)) - { - color = colors.OrderBy(c => colorMap.Values.Count(used => used == c)).First(); - colorMap[quant] = color; - } - - return color; + default:*/ + if (!colorMap.TryGetValue(quant, out var color)) + { + color = colors.OrderBy(c => colorMap.Values.Count(used => used == c)).First(); + colorMap[quant] = color; + } + + return color; //} } @@ -491,8 +490,8 @@ private void pathExplanationButton_Click(object sender, EventArgs e) } catch (Exception exception) { - _z3AxiomProfiler.DisplayMessage($"An exception was thrown. Please report this bug to viper@inf.ethz.ch.\nDescription of the exception: {exception.Message}"); - Console.WriteLine(exception); + _z3AxiomProfiler.DisplayMessage($"An exception was thrown. Please report this bug to viper@inf.ethz.ch.\nDescription of the exception: {exception.Message}"); + Console.WriteLine(exception); } #endif }); @@ -539,18 +538,18 @@ public InstantiationPath BestUpPath(Node node, InstantiationPath downPath) // Return all down patterns found with the bound public static List> AllDownPatterns(Node node, int bound) - { + { List> Patterns = new List>(); - Quantifier Target = ((Instantiation) node.UserData).Quant; + Quantifier Target = ((Instantiation)node.UserData).Quant; List CurPattern = new List(); CurPattern.Add(Target); Tuple> CurPair = new Tuple>(node, CurPattern); - List>> PathStack= new List>>(); + List>> PathStack = new List>>(); PathStack.Add(CurPair); Node CurNode, Child; Quantifier ChildQuant; - while(PathStack.Count > 0) + while (PathStack.Count > 0) { CurPair = PathStack[PathStack.Count - 1]; PathStack.RemoveAt(PathStack.Count - 1); @@ -560,14 +559,15 @@ public static List> AllDownPatterns(Node node, int bound) foreach (Edge edge in CurNode.OutEdges) { Child = edge.TargetNode; - ChildQuant = ((Instantiation) Child.UserData).Quant; + ChildQuant = ((Instantiation)Child.UserData).Quant; if (ChildQuant.Equals(Target)) { if (!ContainPattern(ref Patterns, ref CurPattern)) { Patterns.Add(CurPattern); } - } else + } + else { List NewPattern = new List(CurPattern); NewPattern.Add(ChildQuant); @@ -625,17 +625,17 @@ public static List ExtendDownwards(Node node, ref List Pattern Node LastNode = node, CurNode, Child, Grandchild; int PatternIndex = 0, NextQuant; bool HaveGoodChild = false; - while(true) + while (true) { - LoopBegin: + LoopBegin: PatternIndex = (PatternIndex + 1) % Pattern.Count; CurNode = path[path.Count - 1]; HaveGoodChild = false; if ((bound > 0) & (path.Count == bound)) break; foreach (Edge edge in CurNode.OutEdges) - { + { Child = edge.TargetNode; - if (((Instantiation) Child.UserData).Quant.PrintName == Pattern[PatternIndex].PrintName) + if (((Instantiation)Child.UserData).Quant.PrintName == Pattern[PatternIndex].PrintName) { HaveGoodChild = true; LastNode = Child; @@ -643,7 +643,7 @@ public static List ExtendDownwards(Node node, ref List Pattern foreach (Edge edge2 in Child.OutEdges) { Grandchild = edge2.TargetNode; - if (((Instantiation) Grandchild.UserData).Quant.PrintName == Pattern[NextQuant].PrintName) + if (((Instantiation)Grandchild.UserData).Quant.PrintName == Pattern[NextQuant].PrintName) { path.Add(Child); goto LoopBegin; @@ -660,7 +660,43 @@ public static List ExtendDownwards(Node node, ref List Pattern public static List ExtendUpwards(Node node, ref List Pattern, int bound) { List path = new List() { node }; - // TODO + Node LastNode = node, CurNode, Child, Grandchild; + int PatternIndex = 0, NextQuant; + bool HaveGoodChild = false; + while (true) + { + LoopBegin: + PatternIndex = (PatternIndex + 1) % Pattern.Count; + CurNode = path[path.Count - 1]; + Console.WriteLine("d " + CurNode.Id); + HaveGoodChild = false; + if ((bound > 0) & (path.Count == bound)) break; + foreach (Edge edge in CurNode.InEdges) + { + Child = edge.SourceNode; + Console.WriteLine("dd " + Child.Id); + if (((Instantiation)Child.UserData).Quant.PrintName == Pattern[PatternIndex].PrintName) + { + HaveGoodChild = true; + LastNode = Child; + NextQuant = (PatternIndex + 1) % Pattern.Count; + foreach (Edge edge2 in Child.InEdges) + { + Grandchild = edge2.SourceNode; + Console.WriteLine(((Instantiation)Grandchild.UserData).Quant.PrintName); + Console.WriteLine("ddd " + Grandchild.Id); + if (((Instantiation)Grandchild.UserData).Quant.PrintName == Pattern[NextQuant].PrintName) + { + Console.WriteLine("dddd "); + path.Add(Child); + goto LoopBegin; + } + } + } + } + if (HaveGoodChild) path.Add(LastNode); + break; + } return path; } From 0a11c3516b7d6eaee473680d18a6fb9011b6c1a5 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 20 Jun 2021 11:06:15 -0700 Subject: [PATCH 25/60] clean up and rename some variables --- source/DAGView.cs | 29 ++++++++++++----------------- 1 file changed, 12 insertions(+), 17 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index faa5b39..23932eb 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -587,7 +587,7 @@ public static List> AllUpPatterns(Node node, int bound) Tuple> CurPair = new Tuple>(node, CurPattern); List>> PathStack = new List>>(); PathStack.Add(CurPair); - Node CurNode, Child; + Node CurNode, Parent; Quantifier ChildQuant; while (PathStack.Count > 0) @@ -599,8 +599,8 @@ public static List> AllUpPatterns(Node node, int bound) if (CurPattern.Count > bound) break; foreach (Edge edge in CurNode.InEdges) { - Child = edge.SourceNode; - ChildQuant = ((Instantiation)Child.UserData).Quant; + Parent = edge.SourceNode; + ChildQuant = ((Instantiation)Parent.UserData).Quant; if (ChildQuant.Equals(Target)) { if (!ContainPattern(ref Patterns, ref CurPattern)) @@ -612,7 +612,7 @@ public static List> AllUpPatterns(Node node, int bound) { List NewPattern = new List(CurPattern); NewPattern.Add(ChildQuant); - PathStack.Add(new Tuple>(Child, NewPattern)); + PathStack.Add(new Tuple>(Parent, NewPattern)); } } } @@ -660,7 +660,7 @@ public static List ExtendDownwards(Node node, ref List Pattern public static List ExtendUpwards(Node node, ref List Pattern, int bound) { List path = new List() { node }; - Node LastNode = node, CurNode, Child, Grandchild; + Node LastNode = node, CurNode, Parent, Grandparent; int PatternIndex = 0, NextQuant; bool HaveGoodChild = false; while (true) @@ -668,27 +668,22 @@ public static List ExtendUpwards(Node node, ref List Pattern, LoopBegin: PatternIndex = (PatternIndex + 1) % Pattern.Count; CurNode = path[path.Count - 1]; - Console.WriteLine("d " + CurNode.Id); HaveGoodChild = false; if ((bound > 0) & (path.Count == bound)) break; foreach (Edge edge in CurNode.InEdges) { - Child = edge.SourceNode; - Console.WriteLine("dd " + Child.Id); - if (((Instantiation)Child.UserData).Quant.PrintName == Pattern[PatternIndex].PrintName) + Parent = edge.SourceNode; + if (((Instantiation)Parent.UserData).Quant.PrintName == Pattern[PatternIndex].PrintName) { HaveGoodChild = true; - LastNode = Child; + LastNode = Parent; NextQuant = (PatternIndex + 1) % Pattern.Count; - foreach (Edge edge2 in Child.InEdges) + foreach (Edge edge2 in Parent.InEdges) { - Grandchild = edge2.SourceNode; - Console.WriteLine(((Instantiation)Grandchild.UserData).Quant.PrintName); - Console.WriteLine("ddd " + Grandchild.Id); - if (((Instantiation)Grandchild.UserData).Quant.PrintName == Pattern[NextQuant].PrintName) + Grandparent = edge2.SourceNode; + if (((Instantiation)Grandparent.UserData).Quant.PrintName == Pattern[NextQuant].PrintName) { - Console.WriteLine("dddd "); - path.Add(Child); + path.Add(Parent); goto LoopBegin; } } From 829bb1b8aeb36e75fecd4998d2036efe4b8f87d9 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Mon, 21 Jun 2021 09:12:00 -0700 Subject: [PATCH 26/60] added CustomPathComparer, deleted bestuppath and bestdownpath --- source/DAGView.cs | 32 ++++++-------------------------- 1 file changed, 6 insertions(+), 26 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 23932eb..01a028b 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -501,11 +501,12 @@ private void pathExplanationButton_Click(object sender, EventArgs e) private static readonly double outlierThreshold = 0.3; private static readonly double incomingEdgePenalizationFactor = 0.5; - // Return a score where - // - having longer length recieves a higher score - // - having less covered children recieves a higher score - // - having shorter pattern recieved a higher score - private static double InstantiationPathScoreFunction(InstantiationPath instantiationPath, bool eliminatePrefix, bool eliminatePostfix) + // Custom comparer used to sort a list of tuple { + // the tuple will be consist of (length of path, number of uncovered children, length of pattern) + // - having longer length is preferred + // - having less covered children is preferred + // - having shorter pattern is preferred + private static double CustomPathComparer(InstantiationPath instantiationPath, bool eliminatePrefix, bool eliminatePostfix) { // TODO return 0.0; @@ -515,27 +516,6 @@ private static double InstantiationPathScoreFunction(InstantiationPath instantia // build a path from the best segments. private static readonly int pathSegmentSize = 8; - - // Described in https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing - // Get all down patterns, - // extent them to max(3, lcm(length of patterns)), - // score them and sort by score - // extend to top 5 path fully - // score and sort the fully extended path - // return the best one - public InstantiationPath BestDownPath(Node node) - { - // TODO - return null; - } - - // Similar to BestDownPath but up - public InstantiationPath BestUpPath(Node node, InstantiationPath downPath) - { - // TODO - return null; - } - // Return all down patterns found with the bound public static List> AllDownPatterns(Node node, int bound) { From 9c23ee4f3536278a343b90ad06f451aa2df5284d Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 22 Jun 2021 20:20:57 -0700 Subject: [PATCH 27/60] tests added for CustomPathComparer --- UnitTestProject1/UnitTest1.cs | 106 +++++++++++++++++++++++++++++++++- source/DAGView.cs | 13 +++-- 2 files changed, 112 insertions(+), 7 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 4210d2d..09fecd1 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -192,7 +192,7 @@ public void TestAllUpPattern4() // Similar to ExtendDownwards, but up [TestClass] - public class ExtendUpwards + public class ExtendUpwardsTest { static TestGraphs Graphs = new TestGraphs(); @@ -278,4 +278,108 @@ public void TestExtendUpWards5() } } + // Tests for the CustomPathComparer + [TestClass] + public class CustompathComparerTestClass + { + // tuple where + // item1 is the length of a pth + // item2 is the nubmer of uncovered children + // item3 is the length of pattern + // item 4 is reference to the pattern + static Tuple t0 = new Tuple(1, 0, 1, 0); + static Tuple t1 = new Tuple(1, 0, 5, 1); + static Tuple t2 = new Tuple(10, 15, 3, 2); + static Tuple t3 = new Tuple(8, 8, 3, 3); + static Tuple t4 = new Tuple(8, 0, 3, 4); + static Tuple t5 = new Tuple(6, 8, 3, 5); + static Tuple t6 = new Tuple(7, 3, 3, 6); + static Tuple t7 = new Tuple(7, 3, 3, 7); + + public bool HelperFunction(Tuple path1, Tuple path2) + { + // check path 2 does not have size lager than path1 + if (path2.Item1 > path1.Item1) return false; + if (path2.Item1 < path1.Item1) return true; + + // If path1 and 2 have the same size, + // check path2 has more uncovered children than path1 + if (path2.Item2 < path1.Item2) return false; + if (path2.Item2 > path1.Item2) return true; + + // if path2 and path1 have the number of uncovered childre + // check path2 has longer or equal pattern size than path1 + if (path2.Item3 >= path1.Item3) return true; + return false; + } + + // travial case + // list of length 1 + [TestMethod] + public void TestCustomPathComparer1() + { + List> testList = new List>() { t0 }; + testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + for (int i = 1; i < testList.Count; i++) + { + Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); + } + } + + // test case where there are only 2 elements, t3 and t5 + // where the only difference in t3 and t5 is the length (and reference) + [TestMethod] + public void TestCustomComparer2() + { + List> testList = + new List>() { t3, t5 }; + testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + for (int i = 0; i < testList.Count; i++) + { + Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); + } + } + + // testcase where there are only 2 elements, t3, t4 + // where the only difference is the number of children uncovered + [TestMethod] + public void TestCustomComparer3() + { + List> testList = + new List>() { t3, t4 }; + testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + for (int i = 0; i < testList.Count; i++) + { + Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); + } + } + + // testcase where there are only 2 elements t0, t1 + // where the only difference is the length of pattern + [TestMethod] + public void TestCustomComparer4() + { + List> testList = + new List>() { t0, t1 }; + testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + for (int i = 0; i < testList.Count; i++) + { + Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); + } + } + + // testcase where there are many elements + [TestMethod] + public void TestCustomComparer5() + { + List> testList = + new List>() { t0, t1, t2, t3, t4, t5, t6, t7 }; + testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + for (int i = 0; i < testList.Count; i++) + { + Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); + } + } + } + } diff --git a/source/DAGView.cs b/source/DAGView.cs index 01a028b..38d1159 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -467,6 +467,10 @@ private void sourceTreeButton_Click(object sender, EventArgs e) redrawGraph(); } + // For performance reasons we cannot score all possible paths. Instead we score segments of length 8 and + // build a path from the best segments. + private static readonly int pathSegmentSize = 8; + // This functions and it's helper functions are properlly explain in //https://docs.google.com/document/d/1SJspfBecgkVT9U8xC-MvQ_NPDTGVfg0yqq7YjJ3ma2s/edit?usp=sharing // helper functions were originally private, but changing to public was needed to unit testing @@ -484,7 +488,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) #if !DEBUG try { -#endif +#endif // TODO #if !DEBUG } @@ -506,15 +510,12 @@ private void pathExplanationButton_Click(object sender, EventArgs e) // - having longer length is preferred // - having less covered children is preferred // - having shorter pattern is preferred - private static double CustomPathComparer(InstantiationPath instantiationPath, bool eliminatePrefix, bool eliminatePostfix) + public static int CustomPathComparer(ref Tuple elem1, ref Tuple elem2) { // TODO - return 0.0; + return 0; } - // For performance reasons we cannot score all possible paths. Instead we score segments of length 8 and - // build a path from the best segments. - private static readonly int pathSegmentSize = 8; // Return all down patterns found with the bound public static List> AllDownPatterns(Node node, int bound) From 6701353cfc7aa67a139b000877faf2e5315f6713 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 22 Jun 2021 21:27:52 -0700 Subject: [PATCH 28/60] CustomPathComparer unit test error fix --- UnitTestProject1/UnitTest1.cs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 09fecd1..5d01fe6 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -334,7 +334,7 @@ public void TestCustomComparer2() List> testList = new List>() { t3, t5 }; testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - for (int i = 0; i < testList.Count; i++) + for (int i = 1; i < testList.Count; i++) { Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); } @@ -348,7 +348,7 @@ public void TestCustomComparer3() List> testList = new List>() { t3, t4 }; testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - for (int i = 0; i < testList.Count; i++) + for (int i = 1; i < testList.Count; i++) { Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); } @@ -362,7 +362,7 @@ public void TestCustomComparer4() List> testList = new List>() { t0, t1 }; testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - for (int i = 0; i < testList.Count; i++) + for (int i = 1; i < testList.Count; i++) { Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); } @@ -375,7 +375,7 @@ public void TestCustomComparer5() List> testList = new List>() { t0, t1, t2, t3, t4, t5, t6, t7 }; testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - for (int i = 0; i < testList.Count; i++) + for (int i = 1; i < testList.Count; i++) { Assert.IsTrue(HelperFunction(testList[i - 1], testList[i])); } From ce0e1b3b0e89a681257b12a04cdfda8324db10db Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 22 Jun 2021 21:28:44 -0700 Subject: [PATCH 29/60] CustomPathCompater implemented --- source/DAGView.cs | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 38d1159..a6df8aa 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -511,8 +511,21 @@ private void pathExplanationButton_Click(object sender, EventArgs e) // - having less covered children is preferred // - having shorter pattern is preferred public static int CustomPathComparer(ref Tuple elem1, ref Tuple elem2) - { - // TODO + { + // If elem1 has longer path length return -1 + // which mean elem1 is smaller than elem2, since list sort are in ascending order by default + if (elem1.Item1 > elem2.Item1) return -1; + if (elem1.Item1 < elem2.Item1) return 1; + + // if elem1 has less covered children than elem2 return -1 + if (elem1.Item2 < elem2.Item2) return -1; + if (elem1.Item2 > elem2.Item2) return 1; + + // if elem1 has shorter pattern length return -1 + if (elem1.Item3 < elem2.Item3) return -1; + if (elem1.Item3 > elem2.Item3) return 1; + + return 0; } From 6fa2cb83536b5132bd19bab9e7c5e466b533c4e6 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Wed, 23 Jun 2021 13:48:28 -0700 Subject: [PATCH 30/60] new pathExplanationButton_click implemented --- UnitTestProject1/UnitTest1.cs | 3 + source/DAGView.cs | 130 ++++++++++++++++++++++++++++++++-- 2 files changed, 129 insertions(+), 4 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index 5d01fe6..f92fe36 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -299,16 +299,19 @@ public class CustompathComparerTestClass public bool HelperFunction(Tuple path1, Tuple path2) { // check path 2 does not have size lager than path1 + // path1 should have longer path if (path2.Item1 > path1.Item1) return false; if (path2.Item1 < path1.Item1) return true; // If path1 and 2 have the same size, // check path2 has more uncovered children than path1 + // path one should have less uncovered children if (path2.Item2 < path1.Item2) return false; if (path2.Item2 > path1.Item2) return true; // if path2 and path1 have the number of uncovered childre // check path2 has longer or equal pattern size than path1 + // path1 should have shorter pattern size if (path2.Item3 >= path1.Item3) return true; return false; } diff --git a/source/DAGView.cs b/source/DAGView.cs index a6df8aa..1dcd91f 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -489,7 +489,83 @@ private void pathExplanationButton_Click(object sender, EventArgs e) try { #endif - // TODO + List> downPatterns = AllDownPatterns(previouslySelectedNode, pathSegmentSize); + List> extendedPaths = new List>(); + List pathPatternSize = new List(); + List downPath, upPath; + List pattern; + // if there are down patterns we only look at down patterns + // other wise we look at up patterns + if (downPatterns.Count > 0) + { + int size = FindSize(ref downPatterns); + List> pathStats = new List>(); + for (int i = 0; i < downPatterns.Count; i++) + { + // had to assign a new list for pattern and new path + // because apperently c# can't use ref on elements of a list + pattern = downPatterns[i]; + downPath = ExtendDownwards(previouslySelectedNode, ref pattern, size); + pathStats.Add(GetPathInfo(ref downPath, downPatterns[i].Count, i)); + } + // ussing our custom comparer + pathStats.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + // only take the top 30; + for (int i = 0; (i < pathStats.Count) && (i < 30); i++) + { + pattern = downPatterns[pathStats[i].Item4]; + downPath = ExtendDownwards(previouslySelectedNode, ref pattern, -1); + pattern.Reverse(1, pattern.Count-1); + upPath = ExtendUpwards(previouslySelectedNode, ref pattern, -1); + upPath.Reverse(); + upPath.RemoveAt(upPath.Count - 1); + upPath.AddRange(downPath); + pathPatternSize.Add(pattern.Count); + extendedPaths.Add(upPath); + } + } else + { + List> upPatterns = AllUpPatterns(previouslySelectedNode, pathSegmentSize); + int size = FindSize(ref upPatterns); + List> pathStats = new List>(); + for (int i = 0; i < upPatterns.Count; i++) + { + pattern = upPatterns[i]; + upPath = ExtendUpwards(previouslySelectedNode, ref pattern, size); + upPath.Reverse(); + pathStats.Add(GetPathInfo(ref upPath, pattern.Count, i)); + } + // ussing our custom comparer + pathStats.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + // only take the top 30; + for (int i = 0; (i < pathStats.Count) && (i < 30); i++) + { + pattern = upPatterns[pathStats[i].Item4]; + upPath = ExtendUpwards(previouslySelectedNode, ref pattern, -1); + upPath.Reverse(); + pattern.Reverse(1, pattern.Count-1); + downPath = ExtendDownwards(previouslySelectedNode, ref pattern, -1); + upPath.RemoveAt(upPath.Count-1); + upPath.AddRange(downPath); + extendedPaths.Add(upPath); + pathPatternSize.Add(pattern.Count); + } + } + List> extendedPathStat = new List>(); + for (int i = 0; i < extendedPaths.Count; i++) + { + upPath = extendedPaths[i]; + extendedPathStat.Add(GetPathInfo(ref upPath, pathPatternSize[i], i)); + } + extendedPathStat.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + InstantiationPath InstPath = new InstantiationPath(); + foreach (Node node in extendedPaths[extendedPathStat[0].Item4]) + { + InstPath.append((Instantiation) node.UserData); + } + highlightPath(InstPath); + _z3AxiomProfiler.UpdateSync(InstPath); + _viewer.Invalidate(); #if !DEBUG } catch (Exception exception) @@ -501,9 +577,55 @@ private void pathExplanationButton_Click(object sender, EventArgs e) }); } - // These factors were determined experimentally - private static readonly double outlierThreshold = 0.3; - private static readonly double incomingEdgePenalizationFactor = 0.5; + // helper function to return the size we want + // max of (3 * longest pattern, LCM(of length of patterns)) + public static int FindSize(ref List> pattern) + { + int ThreeTimesLongest = 0; + int LCM = 1; + for (int i = 0; i < pattern.Count; i++) + { + ThreeTimesLongest = Math.Max(ThreeTimesLongest, 2 * pattern[i].Count); + LCM = (LCM * pattern[i].Count) / CalcGCD(LCM, pattern[i].Count); + } + return Math.Max(ThreeTimesLongest, LCM); + } + + // helper function to calculat GCD + public static int CalcGCD(int a, int b) + { + if (b == 0) return a; + if (b > a) return CalcGCD(b, a); + return CalcGCD(b, a % b); + } + + // helper function to return info about a path + // tuple of + // path legnth, + // number of uncovered childre, + // pattern length, + // reference to the pattern / or reference to a path) + public static Tuple GetPathInfo(ref List path, int patternLength, int reference) + { + int pathLength = path.Count; + int patterLegnth = patternLength; + int uncoveredChildren = 0; + Node child; + List seen = new List(); + foreach (Node node in path) + { + foreach (Edge edge in node.OutEdges) + { + child = edge.TargetNode; + if (!seen.Contains(child) && !path.Contains(child)) + { + uncoveredChildren++; + seen.Add(child); + } + } + } + return new Tuple(pathLength, uncoveredChildren, patternLength, reference); + } // Custom comparer used to sort a list of tuple { // the tuple will be consist of (length of path, number of uncovered children, length of pattern) From 1cde62c896a5924a3fd33a4dfbbf7e24e59df478 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 27 Jun 2021 15:47:01 -0700 Subject: [PATCH 31/60] bug fix, when there are no pattern --- source/DAGView.cs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 1dcd91f..c5c7398 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -494,6 +494,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) List pathPatternSize = new List(); List downPath, upPath; List pattern; + InstantiationPath InstPath = new InstantiationPath(); // if there are down patterns we only look at down patterns // other wise we look at up patterns if (downPatterns.Count > 0) @@ -526,6 +527,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) } else { List> upPatterns = AllUpPatterns(previouslySelectedNode, pathSegmentSize); + if (upPatterns.Count == 0) goto NoPattern; int size = FindSize(ref upPatterns); List> pathStats = new List>(); for (int i = 0; i < upPatterns.Count; i++) @@ -558,12 +560,15 @@ private void pathExplanationButton_Click(object sender, EventArgs e) extendedPathStat.Add(GetPathInfo(ref upPath, pathPatternSize[i], i)); } extendedPathStat.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - InstantiationPath InstPath = new InstantiationPath(); foreach (Node node in extendedPaths[extendedPathStat[0].Item4]) { - InstPath.append((Instantiation) node.UserData); + InstPath.append((Instantiation)node.UserData); } highlightPath(InstPath); + goto FoundPattern; + NoPattern: + InstPath.append((Instantiation) previouslySelectedNode.UserData); + FoundPattern: _z3AxiomProfiler.UpdateSync(InstPath); _viewer.Invalidate(); #if !DEBUG From 32a3a5a65682450605faed6d2f4c263ae975728c Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 6 Aug 2021 12:06:34 -0700 Subject: [PATCH 32/60] bug fix for find path, added test case --- UnitTestProject1/TestGraphs.cs | 27 ++++++++++++++++++- UnitTestProject1/UnitTest1.cs | 48 ++++++++++++++++++++++++++++++++++ source/DAGView.cs | 2 +- 3 files changed, 75 insertions(+), 2 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index e540f27..0912fd3 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -12,7 +12,7 @@ class TestGraphs { public List Quants = new List(); // Quantifiers used in unit tests public BindingInfo Info; // BindingInfo used to make nodes - public Graph graph1, graph2, graph3, graph4, graph5; + public Graph graph1, graph2, graph3, graph4, graph5, graph6; // Constructor // Mkae the graphs needsed for testing @@ -24,6 +24,7 @@ public TestGraphs() MakeGraph3(); MakeGraph4(); MakeGraph5(); + MakeGraph6(); } // initialize 9 quantifiers @@ -162,5 +163,29 @@ private void MakeGraph5() graph5.AddEdge("H", "G"); graph5.AddEdge("I", "G"); } + + private void MakeGraph6() + { + graph6 = new Graph(); + graph6.AddNode(MakeNode("A", 0)); + graph6.AddNode(MakeNode("B", 0)); + graph6.AddNode(MakeNode("C", 1)); + graph6.AddNode(MakeNode("D", 0)); + graph6.AddNode(MakeNode("E", 1)); + graph6.AddNode(MakeNode("F", 0)); + graph6.AddNode(MakeNode("G", 1)); + graph6.AddNode(MakeNode("H", 0)); + + graph6.AddEdge("A", "B"); + graph6.AddEdge("B", "C"); + graph6.AddEdge("B", "D"); + graph6.AddEdge("C", "D"); + graph6.AddEdge("D", "E"); + graph6.AddEdge("D", "F"); + graph6.AddEdge("E", "F"); + graph6.AddEdge("F", "G"); + graph6.AddEdge("F", "H"); + graph6.AddEdge("G", "H"); + } } } diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index f92fe36..b70e29c 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -54,6 +54,17 @@ public void TestAllDownPattern4() Assert.AreEqual(1, result.Count); Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); } + + // To test graph 6 + public void TestAllDownPattern5() + { + List> result = DAGView.AllDownPatterns(Graphs.graph6.FindNode("B"), 8); + List expected1 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List expected2 = new List() { Graphs.Quants[0] }; + Assert.AreEqual(2, result.Count); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected2)); + } } [TestClass] @@ -385,4 +396,41 @@ public void TestCustomComparer5() } } + // additional test on graph6 + [TestClass] + public class AdditionalGraph6Test + { + static TestGraphs Graphs = new TestGraphs(); + + // when node B is selected + [TestMethod] + public void AdditionalTest1() + { + List pattern1 = new List() { Graphs.Quants[0] }; + List pattern2 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List> patterns = new List>() { pattern1, pattern2 }; + + List downPath1 = DAGView.ExtendDownwards(Graphs.graph6.FindNode("B"), ref pattern1, -1); + pattern1.Reverse(1, pattern1.Count - 1); + List path1 = DAGView.ExtendUpwards(Graphs.graph6.FindNode("B"), ref pattern1, -1); + path1.Reverse(); + path1.RemoveAt(path1.Count - 1); + path1.AddRange(downPath1); + + List downPath2 = DAGView.ExtendDownwards(Graphs.graph6.FindNode("B"), ref pattern2, -1); + pattern2.Reverse(1, pattern2.Count - 1); + List path2 = DAGView.ExtendUpwards(Graphs.graph6.FindNode("B"), ref pattern2, -1); + path2.Reverse(); + path2.RemoveAt(path2.Count - 1); + path2.AddRange(downPath2); + + Tuple info1 = DAGView.GetPathInfo(ref path1, 1, 1); + Tuple info2 = DAGView.GetPathInfo(ref path2, 2, 2); + + List> infos = new List>() { info1, info2 }; + infos.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + + Assert.AreEqual(2, infos[0].Item4); + } + } } diff --git a/source/DAGView.cs b/source/DAGView.cs index c5c7398..e13102c 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -676,7 +676,7 @@ public static List> AllDownPatterns(Node node, int bound) PathStack.RemoveAt(PathStack.Count - 1); CurNode = CurPair.Item1; CurPattern = CurPair.Item2; - if (CurPattern.Count > bound) break; + if (CurPattern.Count > bound) continue; foreach (Edge edge in CurNode.OutEdges) { Child = edge.TargetNode; From 962771d40c881e33f1ba31e1042311de69f8a827 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 6 Aug 2021 16:44:21 -0700 Subject: [PATCH 33/60] DAGView, UI and naming change, path is no referred as subgraph --- source/DAGView.Designer.cs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/source/DAGView.Designer.cs b/source/DAGView.Designer.cs index eb0a8e8..0baa240 100644 --- a/source/DAGView.Designer.cs +++ b/source/DAGView.Designer.cs @@ -29,7 +29,7 @@ protected override void Dispose(bool disposing) private void InitializeComponent() { this.panel1 = new System.Windows.Forms.Panel(); - this.pathExplanationButton = new System.Windows.Forms.Button(); + this.subgraphExplanationButton = new System.Windows.Forms.Button(); this.sourceTreeButton = new System.Windows.Forms.Button(); this.redrawCompleteGraphButton = new System.Windows.Forms.Button(); this.showChainButton = new System.Windows.Forms.Button(); @@ -46,7 +46,7 @@ private void InitializeComponent() // this.panel1.Anchor = ((System.Windows.Forms.AnchorStyles)(((System.Windows.Forms.AnchorStyles.Top | System.Windows.Forms.AnchorStyles.Left) | System.Windows.Forms.AnchorStyles.Right))); - this.panel1.Controls.Add(this.pathExplanationButton); + this.panel1.Controls.Add(this.subgraphExplanationButton); this.panel1.Controls.Add(this.sourceTreeButton); this.panel1.Controls.Add(this.redrawCompleteGraphButton); this.panel1.Controls.Add(this.showChainButton); @@ -62,13 +62,13 @@ private void InitializeComponent() // // pathExplanationButton // - this.pathExplanationButton.Location = new System.Drawing.Point(295, 32); - this.pathExplanationButton.Name = "pathExplanationButton"; - this.pathExplanationButton.Size = new System.Drawing.Size(75, 23); - this.pathExplanationButton.TabIndex = 7; - this.pathExplanationButton.Text = "Explain Path"; - this.pathExplanationButton.UseVisualStyleBackColor = true; - this.pathExplanationButton.Click += new System.EventHandler(this.pathExplanationButton_Click); + this.subgraphExplanationButton.Location = new System.Drawing.Point(295, 32); + this.subgraphExplanationButton.Name = "pathExplanationButton"; + this.subgraphExplanationButton.Size = new System.Drawing.Size(104, 23); + this.subgraphExplanationButton.TabIndex = 7; + this.subgraphExplanationButton.Text = "Explain Subgraph"; + this.subgraphExplanationButton.UseVisualStyleBackColor = true; + this.subgraphExplanationButton.Click += new System.EventHandler(this.pathExplanationButton_Click); // // sourceTreeButton // @@ -183,6 +183,6 @@ private void InitializeComponent() private System.Windows.Forms.Button showChainButton; private System.Windows.Forms.Button redrawCompleteGraphButton; private System.Windows.Forms.Button sourceTreeButton; - private System.Windows.Forms.Button pathExplanationButton; + private System.Windows.Forms.Button subgraphExplanationButton; } } \ No newline at end of file From 710b7ef40afbf6ac481b358c8c81525d6169e2be Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 6 Aug 2021 17:47:36 -0700 Subject: [PATCH 34/60] created InstantiationSubgraph class --- source/DAGView.cs | 2 +- .../QuantifierModel/InstantiationSubgraph.cs | 31 +++++++++++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 source/QuantifierModel/InstantiationSubgraph.cs diff --git a/source/DAGView.cs b/source/DAGView.cs index e13102c..9af6d99 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -569,7 +569,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) NoPattern: InstPath.append((Instantiation) previouslySelectedNode.UserData); FoundPattern: - _z3AxiomProfiler.UpdateSync(InstPath); + // _z3AxiomProfiler.UpdateSync(InstPath); _viewer.Invalidate(); #if !DEBUG } diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs new file mode 100644 index 0000000..95d33f8 --- /dev/null +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -0,0 +1,31 @@ +using System.Collections.Generic; +using System.Drawing; +using System.Linq; +using AxiomProfiler.CycleDetection; +using AxiomProfiler.PrettyPrinting; +using System; +using AxiomProfiler.Utilities; +using Microsoft.Msagl.Drawing; +namespace AxiomProfiler.QuantifierModel +{ + class InstantiationSubgraph + { + private readonly List> subgraphInstantiations; + private int cycleSize; + public InstantiationSubgraph(ref List> subgraph, int size) + { + cycleSize = size; + subgraphInstantiations = new List>(); + foreach (List cycle in subgraph) + { + if (cycle.Count != cycleSize) break; + List cycleInstantiations = new List(); + foreach (Node node in cycle) + { + cycleInstantiations.Add((Instantiation)(node.UserData)); + } + subgraphInstantiations.Add(cycleInstantiations); + } + } + } +} From 8f7ef38662685b48921a57bf56b5711bc64c6f2f Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 7 Aug 2021 11:18:27 -0700 Subject: [PATCH 35/60] created class InstantiationSungraph --- .../QuantifierModel/InstantiationSubgraph.cs | 297 +++++++++++++++++- 1 file changed, 296 insertions(+), 1 deletion(-) diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs index 95d33f8..c8fcb33 100644 --- a/source/QuantifierModel/InstantiationSubgraph.cs +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -8,7 +8,7 @@ using Microsoft.Msagl.Drawing; namespace AxiomProfiler.QuantifierModel { - class InstantiationSubgraph + class InstantiationSubgraph : IPrintable { private readonly List> subgraphInstantiations; private int cycleSize; @@ -27,5 +27,300 @@ public InstantiationSubgraph(ref List> subgraph, int size) subgraphInstantiations.Add(cycleInstantiations); } } + + // To generate the info panel content + public void InfoPanelText(InfoPanelContent content, PrettyPrintFormat format) + { + if (subgraphInstantiations.Count < 3) + { + PrintPathInfo(content, format);; + } else + { + PrintCycleInfo(content, format); + } + } + + + // When there is no repeating cycle + // only take the first cycle even when there are two + // Requires the subgraph to be a path + public void PrintPathInfo(InfoPanelContent content, PrettyPrintFormat format) + { + content.switchFormat(PrintConstants.TitleFont, PrintConstants.defaultTextColor); + content.Append("Path explanation:"); + content.switchToDefaultFormat(); + content.Append("\n\nLength: " + cycleSize).Append('\n'); + + printPreamble(content, false); + int termNumbering = printPathHead(content, format, subgraphInstantiations[0][0]); + + for (int i = 1; i < cycleSize; i++) + { + termNumbering = printInstantiationWithPredecessor(content, format, + subgraphInstantiations[0][i], subgraphInstantiations[0][i-1], termNumbering); + } + + content.switchToDefaultFormat(); + content.Append("\n\nThis instantiation yields:\n\n"); + subgraphInstantiations[0][cycleSize-1].concreteBody.PrettyPrint(content, format); + } + + + // Preamble, gives information on how to interpret info panel + private void printPreamble(InfoPanelContent content, bool withGen) + { + content.Append("\nHighlighted terms are "); + content.switchFormat(PrintConstants.DefaultFont, PrintConstants.patternMatchColor); + content.Append("matched"); + content.switchToDefaultFormat(); + content.Append(" or "); + content.switchFormat(PrintConstants.DefaultFont, PrintConstants.equalityColor); + content.Append("matched using equality"); + content.switchToDefaultFormat(); + content.Append(" or "); + content.switchFormat(PrintConstants.DefaultFont, PrintConstants.blameColor); + content.Append("blamed"); + content.switchToDefaultFormat(); + content.Append(" or "); + content.switchFormat(PrintConstants.DefaultFont, PrintConstants.bindColor); + content.Append("bound"); + content.switchToDefaultFormat(); + if (withGen) + { + content.Append(" or "); + content.switchFormat(PrintConstants.DefaultFont, PrintConstants.generalizationColor); + content.Append("generalized"); + content.switchToDefaultFormat(); + content.Append(".\n\""); + content.switchFormat(PrintConstants.DefaultFont, PrintConstants.generalizationColor); + content.Append(">...<"); + content.switchToDefaultFormat(); + content.Append("\" indicates that a generalization is hidden below the max term depth"); + } + content.Append(".\n"); + } + + private int printPathHead(InfoPanelContent content, PrettyPrintFormat format, Instantiation current) + { + var termNumbering = 1; + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nStarting from the following term(s):\n\n"); + content.switchToDefaultFormat(); + current.tempHighlightBlameBindTerms(format); + var blameTerms = current.bindingInfo.getDistinctBlameTerms(); + var distinctBlameTerms = blameTerms + .Where(req => current.bindingInfo.equalities.Keys.All(k => current.bindingInfo.bindings[k].Item2 != req)); + + foreach (var distinctBlameTerm in distinctBlameTerms) + { + if (!format.termNumbers.TryGetValue(distinctBlameTerm, out var termNumber)) + { + termNumber = termNumbering; + ++termNumbering; + format.termNumbers[distinctBlameTerm] = termNumber; + } + var numberingString = $"({termNumber}) "; + content.Append(numberingString); + distinctBlameTerm.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + content.Append("\n\n"); + } + + if (current.bindingInfo.equalities.Count > 0) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nRelevant equalities:\n\n"); + content.switchToDefaultFormat(); + + format.printContextSensitive = false; + foreach (var equality in current.bindingInfo.equalities) + { + var effectiveTerm = current.bindingInfo.bindings[equality.Key].Item2; + foreach (var term in equality.Value.Select(t => t.Item2).Distinct(Term.semanticTermComparer)) + { + EqualityExplanation explanation; +#if !DEBUG + try + { +#endif + explanation = current.bindingInfo.EqualityExplanations.First(ee => ee.source.id == term.id && ee.target.id == effectiveTerm.id); +#if !DEBUG + } + catch (Exception) + { + explanation = new TransitiveEqualityExplanation(term, effectiveTerm, new EqualityExplanation[0]); + } +#endif + if (!format.equalityNumbers.TryGetValue(explanation, out var eeNumber)) + { + eeNumber = termNumbering; + ++termNumbering; + format.equalityNumbers[explanation] = eeNumber; + } + if (format.ShowEqualityExplanations) + { + explanation.PrettyPrint(content, format, eeNumber); + } + else + { + var numberingString = $"({eeNumber}) "; + content.switchToDefaultFormat(); + content.Append(numberingString); + var indentString = $"¦{String.Join("", Enumerable.Repeat(" ", numberingString.Length - 1))}"; + term.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + content.Append($"\n{indentString}= (explanation omitted)\n{indentString}"); + effectiveTerm.PrettyPrint(content, format, numberingString.Length); + } + content.Append("\n\n"); + } + } + format.printContextSensitive = true; + + current.bindingInfo.PrintEqualitySubstitution(content, format); + } + + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nApplication of "); + content.Append(current.Quant.PrintName); + content.switchToDefaultFormat(); + content.Append("\n\n"); + + try + { + current.Quant.BodyTerm.PrettyPrint(content, format); + } + catch (Exception) + { + content.Append("Exception was thrown while printing the body of the quantifier\n"); + + } + content.switchToDefaultFormat(); + format.restoreAllOriginalRules(); + return termNumbering; + } + + private int printInstantiationWithPredecessor(InfoPanelContent content, PrettyPrintFormat format, + Instantiation current, Instantiation previous, int termNumbering) + { + current.tempHighlightBlameBindTerms(format); + + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\n\nThis instantiation yields:\n\n"); + content.switchToDefaultFormat(); + + if (!format.termNumbers.TryGetValue(previous.concreteBody, out var termNumber)) + { + termNumber = termNumbering; + ++termNumbering; + format.termNumbers[previous.concreteBody] = termNumber; + } + + var numberingString = $"({termNumber}) "; + content.Append($"{numberingString}"); + previous.concreteBody.PrettyPrint(content, format, numberingString.Length); + + // Other prerequisites: + var otherRequiredTerms = current.bindingInfo.getDistinctBlameTerms() + .FindAll(term => current.bindingInfo.equalities.Any(eq => current.bindingInfo.bindings[eq.Key].Item2 == term) || + !previous.concreteBody.isSubterm(term)).ToList(); + if (otherRequiredTerms.Count > 0) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\n\nTogether with the following term(s):"); + content.switchToDefaultFormat(); + foreach (var distinctBlameTerm in otherRequiredTerms) + { + if (!format.termNumbers.TryGetValue(distinctBlameTerm, out termNumber)) + { + termNumber = termNumbering; + ++termNumbering; + format.termNumbers[distinctBlameTerm] = termNumber; + } + + numberingString = $"({termNumber}) "; + content.Append($"\n\n{numberingString}"); + distinctBlameTerm.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + } + } + + if (current.bindingInfo.equalities.Count > 0) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\n\nRelevant equalities:\n\n"); + content.switchToDefaultFormat(); + + format.printContextSensitive = false; + foreach (var equality in current.bindingInfo.equalities) + { + var effectiveTerm = current.bindingInfo.bindings[equality.Key].Item2; + foreach (var term in equality.Value.Select(t => t.Item2).Distinct(Term.semanticTermComparer)) + { + EqualityExplanation explanation; +#if !DEBUG + try + { +#endif + explanation = current.bindingInfo.EqualityExplanations.First(ee => ee.source.id == term.id && ee.target.id == effectiveTerm.id); +#if !DEBUG + } + catch (Exception) + { + explanation = new TransitiveEqualityExplanation(term, effectiveTerm, new EqualityExplanation[0]); + } +#endif + if (!format.equalityNumbers.TryGetValue(explanation, out var eeNumber)) + { + eeNumber = termNumbering; + ++termNumbering; + format.equalityNumbers[explanation] = eeNumber; + } + if (format.ShowEqualityExplanations) + { + explanation.PrettyPrint(content, format, eeNumber); + } + else + { + numberingString = $"({eeNumber}) "; + content.switchToDefaultFormat(); + content.Append(numberingString); + var indentString = $"¦{String.Join("", Enumerable.Repeat(" ", numberingString.Length - 1))}"; + term.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + content.Append($"\n{indentString}= (explanation omitted)\n{indentString}"); + effectiveTerm.PrettyPrint(content, format, numberingString.Length); + } + content.Append("\n\n"); + } + } + format.printContextSensitive = true; + + current.bindingInfo.PrintEqualitySubstitution(content, format); + } + + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\n\nApplication of "); + content.Append(current.Quant.PrintName); + content.switchToDefaultFormat(); + content.Append("\n\n"); + try + { + current.Quant.BodyTerm.PrettyPrint(content, format); + } + catch (Exception) + { + content.Append("Exception was thrown while printing the body of the quantifier\n"); + } + content.switchToDefaultFormat(); + format.restoreAllOriginalRules(); + return termNumbering; + } + + // When a cycle repeats atleat 3 times + public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) + { + // TODO + } } } From bb0733157ad7f8eb31c459065d8e4e708465d687 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 7 Aug 2021 14:21:16 -0700 Subject: [PATCH 36/60] declared find subgraph function --- source/DAGView.cs | 73 ++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 63 insertions(+), 10 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 9af6d99..f5c5815 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -494,7 +494,9 @@ private void pathExplanationButton_Click(object sender, EventArgs e) List pathPatternSize = new List(); List downPath, upPath; List pattern; - InstantiationPath InstPath = new InstantiationPath(); + List> subgraph; + int cycleSize = 1; + int positionOfSelectedNode = 0; // if there are down patterns we only look at down patterns // other wise we look at up patterns if (downPatterns.Count > 0) @@ -520,6 +522,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) upPath = ExtendUpwards(previouslySelectedNode, ref pattern, -1); upPath.Reverse(); upPath.RemoveAt(upPath.Count - 1); + positionOfSelectedNode = upPath.Count; upPath.AddRange(downPath); pathPatternSize.Add(pattern.Count); extendedPaths.Add(upPath); @@ -548,6 +551,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) pattern.Reverse(1, pattern.Count-1); downPath = ExtendDownwards(previouslySelectedNode, ref pattern, -1); upPath.RemoveAt(upPath.Count-1); + positionOfSelectedNode = upPath.Count; upPath.AddRange(downPath); extendedPaths.Add(upPath); pathPatternSize.Add(pattern.Count); @@ -560,16 +564,17 @@ private void pathExplanationButton_Click(object sender, EventArgs e) extendedPathStat.Add(GetPathInfo(ref upPath, pathPatternSize[i], i)); } extendedPathStat.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - foreach (Node node in extendedPaths[extendedPathStat[0].Item4]) - { - InstPath.append((Instantiation)node.UserData); - } - highlightPath(InstPath); + // send to FindSubgrpah() to construct subgraph from the path + subgraph = FindSubgraph(extendedPaths[extendedPathStat[0].Item4], extendedPathStat[0].Item3, positionOfSelectedNode); + cycleSize = extendedPathStat[0].Item3; goto FoundPattern; - NoPattern: - InstPath.append((Instantiation) previouslySelectedNode.UserData); - FoundPattern: - // _z3AxiomProfiler.UpdateSync(InstPath); + NoPattern: + // subgrpah consisit of only the selcted node + List path = new List() { previouslySelectedNode }; + subgraph = new List>() { path }; + FoundPattern: + InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, cycleSize); + _z3AxiomProfiler.UpdateSync(instSubgraph); _viewer.Invalidate(); #if !DEBUG } @@ -838,5 +843,53 @@ private void highlightPath(InstantiationPath path) } _viewer.Invalidate(); } + + public static List> FindSubgraph(List path, int cycleSize, int pos) + { + int repetition = path.Count / cycleSize; + List> subgraph = new List>(); + if (repetition < 3) + { + // less than means it doesn't count as matching loop, + // so we'll only look at the first cycle + List newPath = new List(); + for (int i = 0; i < cycleSize; i++) + { + newPath.Add(path[i]); + } + subgraph.Add(newPath); + } else if ((repetition < 4) || (pos < cycleSize)) + { + // Condition 1: + // since we also want the substrucutre to repeat atleast 3 times, + // and we start checking from the second one, there needs to be atleast 4 repetitions. + // Condition 2: + // if the user selected some node in the first cycle, it is unclear how we can bound it + // so we won't bother find the repeating strucutre + // Consi + int counter = 0; + List cycle = new List(); + for (int i = 0; i < path.Count; i++) + { + if (counter >= cycleSize) + { + subgraph.Add(cycle); + cycle = new List() { path[i] }; + } + else + { + cycle.Add(path[i]); + } + counter++; + } + subgraph.Add(cycle); + } else + { + // TODO + } + + + return subgraph; + } } } From c18e4be0b27f1d65da535175aee3ff9a73564bd8 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 7 Aug 2021 14:49:58 -0700 Subject: [PATCH 37/60] update sln and csproj --- source/AxiomProfiler.csproj | 1 + source/AxiomProfiler.sln | 42 +++++++++++++++++++++++++++++++++++-- 2 files changed, 41 insertions(+), 2 deletions(-) diff --git a/source/AxiomProfiler.csproj b/source/AxiomProfiler.csproj index 18492c2..015aa88 100644 --- a/source/AxiomProfiler.csproj +++ b/source/AxiomProfiler.csproj @@ -160,6 +160,7 @@ + diff --git a/source/AxiomProfiler.sln b/source/AxiomProfiler.sln index 03e1fdc..e930696 100644 --- a/source/AxiomProfiler.sln +++ b/source/AxiomProfiler.sln @@ -1,22 +1,60 @@ Microsoft Visual Studio Solution File, Format Version 12.00 -# Visual Studio 15 -VisualStudioVersion = 15.0.27703.1 +# Visual Studio Version 16 +VisualStudioVersion = 16.0.31321.278 MinimumVisualStudioVersion = 10.0.40219.1 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AxiomProfiler", "AxiomProfiler.csproj", "{29651769-4A5F-4C7F-BAA7-4064BA38324D}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "UnitTestProject1", "..\UnitTestProject1\UnitTestProject1.csproj", "{6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug Default|Any CPU = Debug Default|Any CPU + Debug Default|x64 = Debug Default|x64 + Debug Default|x86 = Debug Default|x86 Debug|Any CPU = Debug|Any CPU + Debug|x64 = Debug|x64 + Debug|x86 = Debug|x86 Release|Any CPU = Release|Any CPU + Release|x64 = Release|x64 + Release|x86 = Release|x86 EndGlobalSection GlobalSection(ProjectConfigurationPlatforms) = postSolution {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug Default|Any CPU.ActiveCfg = Debug Default|Any CPU {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug Default|Any CPU.Build.0 = Debug Default|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug Default|x64.ActiveCfg = Debug Default|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug Default|x64.Build.0 = Debug Default|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug Default|x86.ActiveCfg = Debug Default|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug Default|x86.Build.0 = Debug Default|Any CPU {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug|Any CPU.ActiveCfg = Debug|Any CPU {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug|Any CPU.Build.0 = Debug|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug|x64.ActiveCfg = Debug|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug|x64.Build.0 = Debug|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug|x86.ActiveCfg = Debug|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Debug|x86.Build.0 = Debug|Any CPU {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Release|Any CPU.ActiveCfg = Release|Any CPU {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Release|Any CPU.Build.0 = Release|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Release|x64.ActiveCfg = Release|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Release|x64.Build.0 = Release|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Release|x86.ActiveCfg = Release|Any CPU + {29651769-4A5F-4C7F-BAA7-4064BA38324D}.Release|x86.Build.0 = Release|Any CPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug Default|Any CPU.ActiveCfg = Debug|Any CPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug Default|Any CPU.Build.0 = Debug|Any CPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug Default|x64.ActiveCfg = Debug|x64 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug Default|x64.Build.0 = Debug|x64 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug Default|x86.ActiveCfg = Debug|x86 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug Default|x86.Build.0 = Debug|x86 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug|Any CPU.Build.0 = Debug|Any CPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug|x64.ActiveCfg = Debug|x64 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug|x64.Build.0 = Debug|x64 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug|x86.ActiveCfg = Debug|x86 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Debug|x86.Build.0 = Debug|x86 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Release|Any CPU.ActiveCfg = Release|Any CPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Release|Any CPU.Build.0 = Release|Any CPU + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Release|x64.ActiveCfg = Release|x64 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Release|x64.Build.0 = Release|x64 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Release|x86.ActiveCfg = Release|x86 + {6FB6598F-E98A-4F89-A1B9-580BFA97C4BC}.Release|x86.Build.0 = Release|x86 EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE From 8dbc609da34654b8830a50cc601057b1fdbcd26d Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 7 Aug 2021 14:54:28 -0700 Subject: [PATCH 38/60] property file for unit test --- UnitTestProject1/Properties/AssemblyInfo.cs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 UnitTestProject1/Properties/AssemblyInfo.cs diff --git a/UnitTestProject1/Properties/AssemblyInfo.cs b/UnitTestProject1/Properties/AssemblyInfo.cs new file mode 100644 index 0000000..91ed501 --- /dev/null +++ b/UnitTestProject1/Properties/AssemblyInfo.cs @@ -0,0 +1,20 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +[assembly: AssemblyTitle("UnitTestProject1")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("")] +[assembly: AssemblyProduct("UnitTestProject1")] +[assembly: AssemblyCopyright("Copyright © 2021")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +[assembly: ComVisible(false)] + +[assembly: Guid("6fb6598f-e98a-4f89-a1b9-580bfa97c4bc")] + +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] From 117dd6cef6ef7099a1b7ab990ca479dcf0848d04 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sat, 7 Aug 2021 15:51:25 -0700 Subject: [PATCH 39/60] pattern can have multiple occurences of the same quant --- UnitTestProject1/TestGraphs.cs | 74 ++++++++++++++++++------ UnitTestProject1/UnitTest1.cs | 102 ++++++++++++++++----------------- source/DAGView.cs | 37 +++++++----- 3 files changed, 127 insertions(+), 86 deletions(-) diff --git a/UnitTestProject1/TestGraphs.cs b/UnitTestProject1/TestGraphs.cs index 0912fd3..0a952f9 100644 --- a/UnitTestProject1/TestGraphs.cs +++ b/UnitTestProject1/TestGraphs.cs @@ -12,7 +12,7 @@ class TestGraphs { public List Quants = new List(); // Quantifiers used in unit tests public BindingInfo Info; // BindingInfo used to make nodes - public Graph graph1, graph2, graph3, graph4, graph5, graph6; + public Graph graph1, graph2, graph3, graph4, graph5, graph6, graph7; // Constructor // Mkae the graphs needsed for testing @@ -25,6 +25,7 @@ public TestGraphs() MakeGraph4(); MakeGraph5(); MakeGraph6(); + MakeGraph7(); } // initialize 9 quantifiers @@ -168,24 +169,59 @@ private void MakeGraph6() { graph6 = new Graph(); graph6.AddNode(MakeNode("A", 0)); - graph6.AddNode(MakeNode("B", 0)); - graph6.AddNode(MakeNode("C", 1)); - graph6.AddNode(MakeNode("D", 0)); - graph6.AddNode(MakeNode("E", 1)); - graph6.AddNode(MakeNode("F", 0)); - graph6.AddNode(MakeNode("G", 1)); - graph6.AddNode(MakeNode("H", 0)); + graph6.AddNode(MakeNode("B", 1)); + graph6.AddNode(MakeNode("C", 0)); + graph6.AddNode(MakeNode("D", 2)); + graph6.AddNode(MakeNode("E", 0)); + graph6.AddNode(MakeNode("F", 1)); + graph6.AddNode(MakeNode("G", 0)); + graph6.AddNode(MakeNode("H", 2)); + graph6.AddNode(MakeNode("I", 0)); + graph6.AddNode(MakeNode("J", 1)); + graph6.AddNode(MakeNode("K", 0)); + graph6.AddNode(MakeNode("L", 0)); + graph6.AddNode(MakeNode("M", 1)); - graph6.AddEdge("A", "B"); - graph6.AddEdge("B", "C"); - graph6.AddEdge("B", "D"); - graph6.AddEdge("C", "D"); - graph6.AddEdge("D", "E"); - graph6.AddEdge("D", "F"); - graph6.AddEdge("E", "F"); - graph6.AddEdge("F", "G"); - graph6.AddEdge("F", "H"); - graph6.AddEdge("G", "H"); + for (char c = 'A'; c < 'H'; c++) + { + graph6.AddEdge(c.ToString(), ((char) (c + 1)).ToString()); + } + + char prev = 'A'; + for (char c = 'I'; c <= 'M'; c++) + { + graph6.AddEdge(prev.ToString(), c.ToString()); + prev = c; + } + } + + private void MakeGraph7() + { + graph7 = new Graph(); + graph7.AddNode(MakeNode("A", 0)); + graph7.AddNode(MakeNode("B", 1)); + graph7.AddNode(MakeNode("C", 0)); + graph7.AddNode(MakeNode("D", 2)); + graph7.AddNode(MakeNode("E", 0)); + graph7.AddNode(MakeNode("F", 1)); + graph7.AddNode(MakeNode("G", 0)); + graph7.AddNode(MakeNode("H", 2)); + graph7.AddNode(MakeNode("I", 0)); + graph7.AddNode(MakeNode("J", 1)); + graph7.AddNode(MakeNode("K", 0)); + graph7.AddNode(MakeNode("L", 0)); + graph7.AddNode(MakeNode("M", 1)); + + for (char c = 'H'; c > 'A'; c--) + { + graph7.AddEdge(c.ToString(), ((char) (c - 1)).ToString()); + } + + graph7.AddEdge("M", "L"); + graph7.AddEdge("L", "K"); + graph7.AddEdge("K", "J"); + graph7.AddEdge("J", "I"); + graph7.AddEdge("I", "A"); } } -} +} \ No newline at end of file diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index b70e29c..f48afb0 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -50,20 +50,31 @@ public void TestAllDownPattern3() public void TestAllDownPattern4() { List> result = DAGView.AllDownPatterns(Graphs.graph3.FindNode("A"), 8); - List expected = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List expected1 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; Assert.AreEqual(1, result.Count); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); } - // To test graph 6 + // Test if AllDownPatterns recogizes pattern that contain + // multiple occurences of the same quantifier in the same cycle + [TestMethod] public void TestAllDownPattern5() { - List> result = DAGView.AllDownPatterns(Graphs.graph6.FindNode("B"), 8); + List> result = DAGView.AllDownPatterns(Graphs.graph6.FindNode("A"), 8); List expected1 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; - List expected2 = new List() { Graphs.Quants[0] }; - Assert.AreEqual(2, result.Count); + List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0], Graphs.Quants[2] }; + List expected3 = new List() { Graphs.Quants[0], Graphs.Quants[1], + Graphs.Quants[0], Graphs.Quants[2], Graphs.Quants[0], Graphs.Quants[1] }; + List expected4 = new List() { Graphs.Quants[0] }; + List expected5 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1] }; + List expected6 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0] }; + Assert.AreEqual(6, result.Count); Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected2)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected3)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected4)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected5)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected6)); } } @@ -77,7 +88,7 @@ public class ExtendDownards public void TestExtenDownwards1() { List pattern = new List() { Graphs.Quants[0], Graphs.Quants[1] }; - List result = + List result = DAGView.ExtendDownwards(Graphs.graph1.FindNode("A"), ref pattern, 10); Assert.AreEqual(1, result.Count); } @@ -87,8 +98,8 @@ public void TestExtenDownwards1() [TestMethod] public void TestExtendDownwards2() { - List pattern = new List() { Graphs.Quants[0]}; - List result = + List pattern = new List() { Graphs.Quants[0] }; + List result = DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, 3); List expected = new List() { "A", "M" }; Assert.AreEqual(expected.Count, result.Count); @@ -128,7 +139,7 @@ public void TestExtendDownWards4() DAGView.ExtendDownwards(Graphs.graph2.FindNode("A"), ref pattern, 6); List expected = new List() { "A", "C", "D", "E", "F", "G" }; Assert.AreEqual(expected.Count, result.Count); - for (int i= 0; i < expected.Count; i++) + for (int i = 0; i < expected.Count; i++) { Assert.AreEqual(expected[i], result[i].Id); } @@ -195,9 +206,31 @@ public void TestAllUpPattern3() public void TestAllUpPattern4() { List> result = DAGView.AllUpPatterns(Graphs.graph5.FindNode("A"), 8); - List expected = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List expected1 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; Assert.AreEqual(1, result.Count); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); + } + + // Test if AllDownPatterns recogizes pattern that contain + // multiple occurences of the same quantifier in the same cycle + [TestMethod] + public void TestAllUpPatterns5() + { + List> result = DAGView.AllUpPatterns(Graphs.graph7.FindNode("A"), 8); + List expected1 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; + List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0], Graphs.Quants[2] }; + List expected3 = new List() { Graphs.Quants[0], Graphs.Quants[1], + Graphs.Quants[0], Graphs.Quants[2], Graphs.Quants[0], Graphs.Quants[1] }; + List expected4 = new List() { Graphs.Quants[0] }; + List expected5 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1] }; + List expected6 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0] }; + Assert.AreEqual(6, result.Count); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected2)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected3)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected4)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected5)); + Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected6)); } } @@ -307,8 +340,8 @@ public class CustompathComparerTestClass static Tuple t6 = new Tuple(7, 3, 3, 6); static Tuple t7 = new Tuple(7, 3, 3, 7); - public bool HelperFunction(Tuple path1, Tuple path2) - { + public bool HelperFunction(Tuple path1, Tuple path2) + { // check path 2 does not have size lager than path1 // path1 should have longer path if (path2.Item1 > path1.Item1) return false; @@ -345,7 +378,7 @@ public void TestCustomPathComparer1() [TestMethod] public void TestCustomComparer2() { - List> testList = + List> testList = new List>() { t3, t5 }; testList.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); for (int i = 1; i < testList.Count; i++) @@ -396,41 +429,4 @@ public void TestCustomComparer5() } } - // additional test on graph6 - [TestClass] - public class AdditionalGraph6Test - { - static TestGraphs Graphs = new TestGraphs(); - - // when node B is selected - [TestMethod] - public void AdditionalTest1() - { - List pattern1 = new List() { Graphs.Quants[0] }; - List pattern2 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; - List> patterns = new List>() { pattern1, pattern2 }; - - List downPath1 = DAGView.ExtendDownwards(Graphs.graph6.FindNode("B"), ref pattern1, -1); - pattern1.Reverse(1, pattern1.Count - 1); - List path1 = DAGView.ExtendUpwards(Graphs.graph6.FindNode("B"), ref pattern1, -1); - path1.Reverse(); - path1.RemoveAt(path1.Count - 1); - path1.AddRange(downPath1); - - List downPath2 = DAGView.ExtendDownwards(Graphs.graph6.FindNode("B"), ref pattern2, -1); - pattern2.Reverse(1, pattern2.Count - 1); - List path2 = DAGView.ExtendUpwards(Graphs.graph6.FindNode("B"), ref pattern2, -1); - path2.Reverse(); - path2.RemoveAt(path2.Count - 1); - path2.AddRange(downPath2); - - Tuple info1 = DAGView.GetPathInfo(ref path1, 1, 1); - Tuple info2 = DAGView.GetPathInfo(ref path2, 2, 2); - - List> infos = new List>() { info1, info2 }; - infos.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - - Assert.AreEqual(2, infos[0].Item4); - } - } -} +} \ No newline at end of file diff --git a/source/DAGView.cs b/source/DAGView.cs index f5c5815..ba38858 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -693,12 +693,9 @@ public static List> AllDownPatterns(Node node, int bound) Patterns.Add(CurPattern); } } - else - { - List NewPattern = new List(CurPattern); - NewPattern.Add(ChildQuant); - PathStack.Add(new Tuple>(Child, NewPattern)); - } + List NewPattern = new List(CurPattern); + NewPattern.Add(ChildQuant); + PathStack.Add(new Tuple>(Child, NewPattern)); } } return Patterns; @@ -722,7 +719,7 @@ public static List> AllUpPatterns(Node node, int bound) PathStack.RemoveAt(PathStack.Count - 1); CurNode = CurPair.Item1; CurPattern = CurPair.Item2; - if (CurPattern.Count > bound) break; + if (CurPattern.Count > bound) continue; foreach (Edge edge in CurNode.InEdges) { Parent = edge.SourceNode; @@ -734,12 +731,9 @@ public static List> AllUpPatterns(Node node, int bound) Patterns.Add(CurPattern); } } - else - { - List NewPattern = new List(CurPattern); - NewPattern.Add(ChildQuant); - PathStack.Add(new Tuple>(Parent, NewPattern)); - } + List NewPattern = new List(CurPattern); + NewPattern.Add(ChildQuant); + PathStack.Add(new Tuple>(Parent, NewPattern)); } } return Patterns; @@ -821,11 +815,26 @@ public static List ExtendUpwards(Node node, ref List Pattern, return path; } + // contain pattern check if patterns contain the pattern + // also check that pattern is a a repetition of a smaller pattern that already exists in patterns public static bool ContainPattern(ref List> patterns, ref List pattern) { + bool Contain; for (int i = 0; i < patterns.Count; i++) { - if (patterns[i].SequenceEqual(pattern)) return true; + //if (patterns[i].SequenceEqual(pattern)) return true; + if (pattern.Count() % patterns[i].Count() == 0) { + Contain = true; + for (int j = 0; j < pattern.Count(); j++) + { + if (pattern[j] != patterns[i][j % patterns[i].Count()]) + { + Contain = false; + break; + } + } + if (Contain) return true; + } } return false; } From b271fa27f26eeec95249195e0ec04ac4248d86c7 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 12:01:42 -0700 Subject: [PATCH 40/60] implemented find substrucutre --- source/DAGView.cs | 115 +++++++++++++++++++++++++++++++++++++--------- 1 file changed, 93 insertions(+), 22 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index ba38858..ae58a79 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -867,38 +867,109 @@ public static List> FindSubgraph(List path, int cycleSize, int newPath.Add(path[i]); } subgraph.Add(newPath); - } else if ((repetition < 4) || (pos < cycleSize)) + return subgraph; + } + int start = 0; + if ((repetition < 4) || (pos < (cycleSize + (path.Count % cycleSize)))) start = cycleSize + (path.Count % cycleSize); + int counter = 0; + List cycle = new List(); + for (int i = start; i < path.Count; i++) + { + if (counter >= cycleSize) + { + subgraph.Add(cycle); + cycle = new List() { path[i] }; + } + else + { + cycle.Add(path[i]); + } + counter++; + } + subgraph.Add(cycle); + // Condition 1: + // since we also want the substrucutre to repeat atleast 3 times, + // and we start checking from the second one, there needs to be atleast 4 repetitions. + // Condition 2: + // if the user selected some node in the first full cycle, it is unclear how we can bound it + // so we won't bother find the repeating strucutre + if ((repetition < 4) || (pos < (cycleSize + (path.Count % cycleSize)))) return subgraph; + + List> cloneOfSubgraph = new List>(subgraph); + + int bound = GetDepth(path[path.Count % cycleSize]); + List> generalStruct = new List>(); + FindGeneralStructure(subgraph[0], ref generalStruct, bound); +; + for (int i = 0; i < path.Count; i++) { - // Condition 1: - // since we also want the substrucutre to repeat atleast 3 times, - // and we start checking from the second one, there needs to be atleast 4 repetitions. - // Condition 2: - // if the user selected some node in the first cycle, it is unclear how we can bound it - // so we won't bother find the repeating strucutre - // Consi - int counter = 0; - List cycle = new List(); - for (int i = 0; i < path.Count; i++) + for (int j = 0; j < subgraph[i].Count; j++) { - if (counter >= cycleSize) + List parents = new List(); + foreach (Edge inedge in subgraph[i][j].InEdges) { - subgraph.Add(cycle); - cycle = new List() { path[i] }; + parents.Add(inedge.SourceNode); } - else + parents.Sort(DAGView.ParentComparer); + for (int k = 0; k < parents.Count; k++) { - cycle.Add(path[i]); + if (!subgraph[i].Contains(parents[k]) && + (GetDepth(parents[k]) >= bound) && + (GetQuant(parents[k]) == generalStruct[j][k])) + { + subgraph[i].Add(parents[k]); + } else + { + return cloneOfSubgraph; + } } - counter++; } - subgraph.Add(cycle); - } else - { - // TODO } - + return subgraph; } + + public static void FindGeneralStructure(List cycle, ref List> result, int bound) + { + for (int i = 0; i < cycle.Count; i++) + { + List parents = new List(); + List orderedParent = new List(); + foreach (Edge inedge in cycle[0].InEdges) + { + orderedParent.Add(inedge.SourceNode); + } + orderedParent.Sort(DAGView.ParentComparer); + foreach (Node node in orderedParent) + { + if ((!cycle.Contains(node)) && (GetDepth(node) >= bound)) + { + cycle.Add(node); + parents.Add(GetQuant(node)); + } + } + result.Add(parents); + } + } + + + public static int GetDepth(Node node) + { + return ((Instantiation) node.UserData).Depth; + } + + public static Quantifier GetQuant(Node node) + { + return ((Instantiation)node.UserData).Quant; + } + + public static int ParentComparer(Node a, Node b) + { + int deptha = GetDepth(a), depthb = GetDepth(b); + if (deptha < depthb) return 1; + if (deptha > depthb) return -1; + return string.Compare(GetQuant(a).Qid, GetQuant(b).Qid); + } } } From 3d4301f9441c467564c208d87cdfa39186cac75d Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 12:08:19 -0700 Subject: [PATCH 41/60] changed highlightPath to highlightSubgraph --- source/DAGView.cs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index ae58a79..aad6b24 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -573,6 +573,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) List path = new List() { previouslySelectedNode }; subgraph = new List>() { path }; FoundPattern: + highlightSubgraph(ref subgraph); InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, cycleSize); _z3AxiomProfiler.UpdateSync(instSubgraph); _viewer.Invalidate(); @@ -839,16 +840,19 @@ public static bool ContainPattern(ref List> patterns, ref List< return false; } - private void highlightPath(InstantiationPath path) + private void highlightSubgraph(ref List> subgraph) { if (previouslySelectedNode != null || highlightedNodes.Count != 0) { unselectNode(); } - foreach (var instantiation in path.getInstantiations()) - { - highlightNode(graph.FindNode(instantiation.uniqueID)); + foreach (List cycle in subgraph) + { + foreach (Node node in cycle) + { + highlightNode(node); + } } _viewer.Invalidate(); } From 07606ac1ab873ca34d81d59a0a78dad970f13913 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 12:22:01 -0700 Subject: [PATCH 42/60] findsubgraph, debugg case when selected node is less than the first cycle --- source/DAGView.cs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index aad6b24..febd536 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -873,14 +873,16 @@ public static List> FindSubgraph(List path, int cycleSize, int subgraph.Add(newPath); return subgraph; } - int start = 0; - if ((repetition < 4) || (pos < (cycleSize + (path.Count % cycleSize)))) start = cycleSize + (path.Count % cycleSize); + int start = cycleSize + (path.Count % cycleSize); + if ((repetition < 4) || (pos < (cycleSize + (path.Count % cycleSize)))) start = 0; int counter = 0; List cycle = new List(); for (int i = start; i < path.Count; i++) { if (counter >= cycleSize) { + counter = 0; + //Console.WriteLine("D " + GetDepth(cycle[0])); subgraph.Add(cycle); cycle = new List() { path[i] }; } @@ -924,6 +926,7 @@ public static List> FindSubgraph(List path, int cycleSize, int subgraph[i].Add(parents[k]); } else { + Console.WriteLine("? " + i + " " + j + " " + k); return cloneOfSubgraph; } } From b504031f01458bb24bc00e1f6c0ecfe0e30dc588 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 13:39:43 -0700 Subject: [PATCH 43/60] bug gix for findsubgraph, still contain more bugs --- source/DAGView.cs | 50 ++++++++++++++++++++++++++++++++++------------- 1 file changed, 36 insertions(+), 14 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index febd536..3ac4cfd 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -574,7 +574,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) subgraph = new List>() { path }; FoundPattern: highlightSubgraph(ref subgraph); - InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, cycleSize); + InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, subgraph[0].Count); _z3AxiomProfiler.UpdateSync(instSubgraph); _viewer.Invalidate(); #if !DEBUG @@ -882,7 +882,6 @@ public static List> FindSubgraph(List path, int cycleSize, int if (counter >= cycleSize) { counter = 0; - //Console.WriteLine("D " + GetDepth(cycle[0])); subgraph.Add(cycle); cycle = new List() { path[i] }; } @@ -905,31 +904,46 @@ public static List> FindSubgraph(List path, int cycleSize, int int bound = GetDepth(path[path.Count % cycleSize]); List> generalStruct = new List>(); - FindGeneralStructure(subgraph[0], ref generalStruct, bound); -; - for (int i = 0; i < path.Count; i++) + List generalCycle = new List(); + for (int i = path.Count % cycleSize; i < cycleSize + (path.Count % cycleSize); i++) { - for (int j = 0; j < subgraph[i].Count; j++) + generalCycle.Add(path[i]); + } + generalCycle.AddRange(subgraph[0]); + FindGeneralStructure(generalCycle, ref generalStruct, bound); + + Node curNode; + int subgraphsize = subgraph.Count; + for (int i = 0; i < subgraphsize; i++) + { + counter = 0; + Queue queue = new Queue(); + foreach (Node node in subgraph[i]) { + queue.Enqueue(node); + } + while(queue.Count > 0) { + curNode = queue.Dequeue(); List parents = new List(); - foreach (Edge inedge in subgraph[i][j].InEdges) + foreach (Edge inedge in curNode.InEdges) { parents.Add(inedge.SourceNode); } parents.Sort(DAGView.ParentComparer); - for (int k = 0; k < parents.Count; k++) + for (int k = 0; k < parents.Count && k < generalStruct.Count; k++) { if (!subgraph[i].Contains(parents[k]) && (GetDepth(parents[k]) >= bound) && - (GetQuant(parents[k]) == generalStruct[j][k])) + (GetQuant(parents[k]) == generalStruct[counter][k])) { subgraph[i].Add(parents[k]); - } else + } + else { - Console.WriteLine("? " + i + " " + j + " " + k); return cloneOfSubgraph; } } + counter++; } } @@ -939,11 +953,19 @@ public static List> FindSubgraph(List path, int cycleSize, int public static void FindGeneralStructure(List cycle, ref List> result, int bound) { - for (int i = 0; i < cycle.Count; i++) + Queue queue = new Queue(); + for (int i = cycle.Count / 2; i < cycle.Count; i++) + { + queue.Enqueue(cycle[i]); + } + Node curNode; + while(queue.Count > 0) { + curNode = queue.Dequeue(); + if (GetDepth(curNode) <= bound) continue; List parents = new List(); List orderedParent = new List(); - foreach (Edge inedge in cycle[0].InEdges) + foreach (Edge inedge in curNode.InEdges) { orderedParent.Add(inedge.SourceNode); } @@ -952,7 +974,7 @@ public static void FindGeneralStructure(List cycle, ref List= bound)) { - cycle.Add(node); + queue.Enqueue(node); parents.Add(GetQuant(node)); } } From a46f6c16274534f33ffc3e494cb394051ddb64a0 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 13:48:35 -0700 Subject: [PATCH 44/60] findsubgrpah bug fix --- source/DAGView.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 3ac4cfd..02e92bc 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -916,6 +916,7 @@ public static List> FindSubgraph(List path, int cycleSize, int int subgraphsize = subgraph.Count; for (int i = 0; i < subgraphsize; i++) { + //Console.WriteLine("D " + i); counter = 0; Queue queue = new Queue(); foreach (Node node in subgraph[i]) @@ -924,14 +925,17 @@ public static List> FindSubgraph(List path, int cycleSize, int } while(queue.Count > 0) { curNode = queue.Dequeue(); + //Console.WriteLine(GetQuant(curNode).Qid); List parents = new List(); foreach (Edge inedge in curNode.InEdges) { parents.Add(inedge.SourceNode); } parents.Sort(DAGView.ParentComparer); - for (int k = 0; k < parents.Count && k < generalStruct.Count; k++) + for (int k = 0; k < parents.Count && k < generalStruct[counter].Count; k++) { + //Console.WriteLine("K " + k); + //Console.WriteLine("sz " + generalStruct[counter].Count); if (!subgraph[i].Contains(parents[k]) && (GetDepth(parents[k]) >= bound) && (GetQuant(parents[k]) == generalStruct[counter][k])) From 3ce9e2b513a24bee6ad68f9357719ebde3e06579 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 14:37:50 -0700 Subject: [PATCH 45/60] findsubgraph bug fix --- source/DAGView.cs | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 02e92bc..918f155 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -916,7 +916,6 @@ public static List> FindSubgraph(List path, int cycleSize, int int subgraphsize = subgraph.Count; for (int i = 0; i < subgraphsize; i++) { - //Console.WriteLine("D " + i); counter = 0; Queue queue = new Queue(); foreach (Node node in subgraph[i]) @@ -925,28 +924,25 @@ public static List> FindSubgraph(List path, int cycleSize, int } while(queue.Count > 0) { curNode = queue.Dequeue(); - //Console.WriteLine(GetQuant(curNode).Qid); List parents = new List(); foreach (Edge inedge in curNode.InEdges) { parents.Add(inedge.SourceNode); } parents.Sort(DAGView.ParentComparer); - for (int k = 0; k < parents.Count && k < generalStruct[counter].Count; k++) + int l = 0; + for (int k = 0; k < parents.Count; k++) { - //Console.WriteLine("K " + k); - //Console.WriteLine("sz " + generalStruct[counter].Count); + if (l >= generalStruct[counter].Count) break; if (!subgraph[i].Contains(parents[k]) && (GetDepth(parents[k]) >= bound) && - (GetQuant(parents[k]) == generalStruct[counter][k])) + (GetQuant(parents[k]) == generalStruct[counter][l])) { subgraph[i].Add(parents[k]); - } - else - { - return cloneOfSubgraph; + l++; } } + if (l < (generalStruct[counter].Count - 1)) return cloneOfSubgraph; counter++; } } From 76585fe454fd88c196046f6d576356da6acff3f1 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 20:25:08 -0700 Subject: [PATCH 46/60] basic finding subgraph working --- source/DAGView.cs | 2 +- source/QuantifierModel/InstantiationSubgraph.cs | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 918f155..bee00f3 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -574,7 +574,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) subgraph = new List>() { path }; FoundPattern: highlightSubgraph(ref subgraph); - InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, subgraph[0].Count); + InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, subgraph[0].Count, cycleSize); _z3AxiomProfiler.UpdateSync(instSubgraph); _viewer.Invalidate(); #if !DEBUG diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs index c8fcb33..051b697 100644 --- a/source/QuantifierModel/InstantiationSubgraph.cs +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -11,10 +11,14 @@ namespace AxiomProfiler.QuantifierModel class InstantiationSubgraph : IPrintable { private readonly List> subgraphInstantiations; + // number of elements in cycle (the repeating strucutre) private int cycleSize; - public InstantiationSubgraph(ref List> subgraph, int size) + // number of elements in cycle (when it was just a path) + private int simpleSize; + public InstantiationSubgraph(ref List> subgraph, int size, int simpleSZ) { cycleSize = size; + simpleSize = simpleSZ; subgraphInstantiations = new List>(); foreach (List cycle in subgraph) { From 8acda60f471859fb706af69c043e52d467e49cb5 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 20:59:01 -0700 Subject: [PATCH 47/60] copied parts of InstantiatnionPath to Instantiationgraph with some changes, no compiling error --- source/DAGView.cs | 4 +- .../QuantifierModel/InstantiationSubgraph.cs | 661 +++++++++++++++++- 2 files changed, 651 insertions(+), 14 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index bee00f3..f54fc76 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -574,7 +574,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) subgraph = new List>() { path }; FoundPattern: highlightSubgraph(ref subgraph); - InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, subgraph[0].Count, cycleSize); + InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, subgraph[0].Count); _z3AxiomProfiler.UpdateSync(instSubgraph); _viewer.Invalidate(); #if !DEBUG @@ -866,7 +866,7 @@ public static List> FindSubgraph(List path, int cycleSize, int // less than means it doesn't count as matching loop, // so we'll only look at the first cycle List newPath = new List(); - for (int i = 0; i < cycleSize; i++) + for (int i = pos; i < (pos + cycleSize) && i < path.Count; i++) { newPath.Add(path[i]); } diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs index 051b697..8cbb519 100644 --- a/source/QuantifierModel/InstantiationSubgraph.cs +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -10,16 +10,14 @@ namespace AxiomProfiler.QuantifierModel { class InstantiationSubgraph : IPrintable { - private readonly List> subgraphInstantiations; + private readonly List subgraphInstantiations; // number of elements in cycle (the repeating strucutre) private int cycleSize; - // number of elements in cycle (when it was just a path) - private int simpleSize; - public InstantiationSubgraph(ref List> subgraph, int size, int simpleSZ) + + public InstantiationSubgraph(ref List> subgraph, int size) { cycleSize = size; - simpleSize = simpleSZ; - subgraphInstantiations = new List>(); + subgraphInstantiations = new List(); foreach (List cycle in subgraph) { if (cycle.Count != cycleSize) break; @@ -28,14 +26,14 @@ public InstantiationSubgraph(ref List> subgraph, int size, int simple { cycleInstantiations.Add((Instantiation)(node.UserData)); } - subgraphInstantiations.Add(cycleInstantiations); + subgraphInstantiations.AddRange(cycleInstantiations); } } // To generate the info panel content public void InfoPanelText(InfoPanelContent content, PrettyPrintFormat format) { - if (subgraphInstantiations.Count < 3) + if ((subgraphInstantiations.Count / cycleSize) < 3) { PrintPathInfo(content, format);; } else @@ -56,17 +54,17 @@ public void PrintPathInfo(InfoPanelContent content, PrettyPrintFormat format) content.Append("\n\nLength: " + cycleSize).Append('\n'); printPreamble(content, false); - int termNumbering = printPathHead(content, format, subgraphInstantiations[0][0]); + int termNumbering = printPathHead(content, format, subgraphInstantiations[0]); for (int i = 1; i < cycleSize; i++) { termNumbering = printInstantiationWithPredecessor(content, format, - subgraphInstantiations[0][i], subgraphInstantiations[0][i-1], termNumbering); + subgraphInstantiations[i], subgraphInstantiations[i-1], termNumbering); } content.switchToDefaultFormat(); content.Append("\n\nThis instantiation yields:\n\n"); - subgraphInstantiations[0][cycleSize-1].concreteBody.PrettyPrint(content, format); + subgraphInstantiations[cycleSize-1].concreteBody.PrettyPrint(content, format); } @@ -324,7 +322,646 @@ private int printInstantiationWithPredecessor(InfoPanelContent content, PrettyPr // When a cycle repeats atleat 3 times public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) { - // TODO + List cycle = new List(); + for (int i = 0; i < cycleSize; i++) + { + cycle.Add(subgraphInstantiations[i].Quant); + } + GeneralizationState generalizationState = new GeneralizationState(cycleSize, subgraphInstantiations); + + if (generalizationState.TrueLoop) + { + content.switchFormat(PrintConstants.TitleFont, PrintConstants.warningTextColor); + content.Append("Possible matching loop found!\n"); + } + else + { + content.switchFormat(PrintConstants.BoldFont, PrintConstants.defaultTextColor); + content.Append("Repeating pattern but "); + content.switchFormat(PrintConstants.TitleFont, PrintConstants.defaultTextColor); + content.Append("no"); + content.switchFormat(PrintConstants.BoldFont, PrintConstants.defaultTextColor); + content.Append(" matching loop found!\n"); + } + content.switchToDefaultFormat(); + content.Append($"Number of{(generalizationState.TrueLoop ? " loop" : "")} iterations: ").Append((subgraphInstantiations.Count / cycleSize) + "\n"); + content.Append($"Number of quantifiers in {(generalizationState.TrueLoop ? "loop" : "pattern")}: ").Append(cycle.Count + "\n"); + if (generalizationState.TrueLoop) + { + content.Append("Loop: "); + } + else + { + content.Append("Pattern: "); + } + content.Append(string.Join(" -> ", cycle.Select(quant => quant.PrintName))); + content.Append("\n"); + + printPreamble(content, true); + + content.switchFormat(PrintConstants.TitleFont, PrintConstants.defaultTextColor); + content.Append($"\n\nGeneralized{(generalizationState.TrueLoop ? " Loop" : "")} Iteration:\n\n"); + + var generalizedTerms = generalizationState.generalizedTerms; + + var additionalTerms = generalizedTerms.Take(generalizedTerms.Count - 1).SelectMany(t => t.Item3 + .Where(req => !t.Item2.equalities.SelectMany(eq => eq.Value).Any(eq => Term.semanticTermComparer.Equals(eq.Item2, req))) + .Where(req => t.Item2.equalities.Keys.All(k => t.Item2.bindings[k].Item2 != req)) + .Select(term => Tuple.Create(t.Item2, term))).ToLookup(t => t.Item2.ContainsGeneralization()); + var additionalSetTerms = additionalTerms[true].ToList(); + var additionalSingleTerms = additionalTerms[false].ToList(); + + var numbering = 1; + foreach (var term in additionalSetTerms.Concat(additionalSingleTerms)) + { + format.termNumbers[term.Item2] = numbering; + ++numbering; + } + + foreach (var step in generalizedTerms) + { + format.termNumbers[step.Item1] = numbering; + ++numbering; + + foreach (var ee in step.Item2.EqualityExplanations) + { + format.equalityNumbers[ee] = numbering; + ++numbering; + } + } + + var alreadyIntroducedGeneralizations = new HashSet(); + if (additionalSetTerms.Any()) + { + + // print last yield term before printing the complete loop + // to give the user a term to match the highlighted pattern to + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nStarting anywhere with the following set(s) of term(s):\n\n"); + content.switchToDefaultFormat(); + + var setGroups = additionalSetTerms.GroupBy(t => Tuple.Create(t.Item2.Responsible, generalizationState.IsProducedByLoop(t.Item2))); + foreach (var group in setGroups) + { + var responsible = group.Key.Item1; + var loopProduced = group.Key.Item2; + if (responsible != null) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append($"Generated by {responsible.Quant.PrintName} ({(loopProduced ? "" : "not ")}part of the current loop):\n"); + content.switchToDefaultFormat(); + } + else + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append($"Asserted:\n"); + content.switchToDefaultFormat(); + } + + foreach (var bindingInfoAndTerm in group) + { + generalizationState.tmpHighlightGeneralizedTerm(format, bindingInfoAndTerm.Item2, bindingInfoAndTerm.Item1, false); + + var newlyIntroducedGeneralizations = bindingInfoAndTerm.Item2.GetAllGeneralizationSubtermsAndDependencies() + .GroupBy(gen => gen.generalizationCounter).Select(g => g.First()) + .Where(gen => !alreadyIntroducedGeneralizations.Contains(gen.generalizationCounter)); + PrintNewlyIntroducedGeneralizations(content, format, newlyIntroducedGeneralizations); + alreadyIntroducedGeneralizations.UnionWith(newlyIntroducedGeneralizations.Select(gen => gen.generalizationCounter)); + + var termNumber = format.termNumbers[bindingInfoAndTerm.Item2]; + var numberingString = $"({termNumber}) "; + content.Append($"{numberingString}"); + + bindingInfoAndTerm.Item2.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + content.Append("\n\n"); + } + } + } + else + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nStarting anywhere with the following term(s):\n\n"); + content.switchToDefaultFormat(); + } + + foreach (var bindingInfoAndTerm in additionalSingleTerms) + { + generalizationState.tmpHighlightGeneralizedTerm(format, bindingInfoAndTerm.Item2, bindingInfoAndTerm.Item1, false); + + var termNumber = format.termNumbers[bindingInfoAndTerm.Item2]; + var numberingString = $"({termNumber}) "; + content.Append($"{numberingString}"); + + bindingInfoAndTerm.Item2.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + content.Append("\n\n"); + } + + var insts = subgraphInstantiations.GetEnumerator(); + insts.MoveNext(); + var recursiveEqualityExplanations = new List>(); + var firstStep = generalizationState.generalizedTerms.First(); + printGeneralizedTermWithPrerequisites(content, format, generalizationState, alreadyIntroducedGeneralizations, firstStep.Item1, firstStep.Item2, firstStep.Item3, false, recursiveEqualityExplanations); + + var count = 1; + var loopSteps = generalizedTerms.Skip(1); + var numberOfSteps = loopSteps.Count(); + foreach (var step in loopSteps) + { + format.restoreAllOriginalRules(); + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nApplication of "); + content.Append(insts.Current?.Quant.PrintName); + content.switchToDefaultFormat(); + if (insts.Current?.Quant.BodyTerm != null) + { + content.Append("\n\n"); + + // print quantifier body with pattern + insts.Current.tempHighlightBlameBindTerms(format); + insts.Current.Quant.BodyTerm.PrettyPrint(content, format); + } + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\n\nThis yields:\n\n"); + content.switchToDefaultFormat(); + + insts.MoveNext(); + format.restoreAllOriginalRules(); + printGeneralizedTermWithPrerequisites(content, format, generalizationState, alreadyIntroducedGeneralizations, step.Item1, step.Item2, step.Item3, count == numberOfSteps, recursiveEqualityExplanations); + count++; + } + + if (recursiveEqualityExplanations.Any()) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\n\nEqualities for Next Iteration(s):\n\n"); + + var offsetGroups = recursiveEqualityExplanations.GroupBy(ee => EqualityExplanationShiftCollector.singleton.visit(ee.Item2, null)).OrderBy(group => group.Key).AsEnumerable(); + var nonGeneralizedEqualities = Enumerable.Empty(); + if (offsetGroups.First().Key == -1) + { + nonGeneralizedEqualities = offsetGroups.First().Select(tuple => tuple.Item1); + offsetGroups = offsetGroups.Skip(1); + } + + foreach (var group in offsetGroups) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append($"In {group.Key} Iteration(s) the Following Equalities Will Be Used:\n\n"); + + foreach (var equalityExplanation in group) + { + var equalityNumber = equalityExplanation.Item1; + var shiftedEqualityExplanation = EqualityExplanationShifter.singleton.visit(equalityExplanation.Item2, group.Key); + + var newlyIntroducedGeneralizationTerms = new List(); + EqualityExplanationTermVisitor.singleton.visit(shiftedEqualityExplanation, t => newlyIntroducedGeneralizationTerms.AddRange(t.GetAllGeneralizationSubterms())); + + var newlyIntroducedGeneralizations = newlyIntroducedGeneralizationTerms + .GroupBy(gen => gen.generalizationCounter).Select(g => g.First()) + .Where(gen => !alreadyIntroducedGeneralizations.Contains(gen.generalizationCounter)); + PrintNewlyIntroducedGeneralizations(content, format, newlyIntroducedGeneralizations); + alreadyIntroducedGeneralizations.UnionWith(newlyIntroducedGeneralizations.Select(gen => gen.generalizationCounter)); + + content.switchToDefaultFormat(); + var numberingString = $"({equalityNumber}') "; + content.Append(numberingString); + shiftedEqualityExplanation.source.PrettyPrint(content, format, numberingString.Length); + EqualityExplanationPrinter.singleton.visit(shiftedEqualityExplanation, Tuple.Create(content, format, false, numberingString.Length)); + content.switchToDefaultFormat(); + content.Append("\n\n"); + } + } + + if (nonGeneralizedEqualities.Any()) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("The Following Equalities Reference Several Iterations and Could Not Be Generalized:\n\n"); + content.switchToDefaultFormat(); + content.Append(String.Join(", ", nonGeneralizedEqualities.Select(e => $"({e})"))); + } + } + + format.restoreAllOriginalRules(); + content.Append("\n\n"); + } + + private static void PrintNewlyIntroducedGeneralizations(InfoPanelContent content, PrettyPrintFormat format, IEnumerable newlyIntroducedGeneralizations) + { + if (newlyIntroducedGeneralizations.Any()) + { + var dependentGeneralizationLookup = newlyIntroducedGeneralizations.ToLookup(gen => gen.Args.Count() > 0); + var hasIndependent = dependentGeneralizationLookup[false].Any(); + if (hasIndependent) + { + content.Append("For any term(s) "); + + var ordered = dependentGeneralizationLookup[false].OrderBy(gen => -gen.id); + ordered.First().PrettyPrint(content, format); + content.switchToDefaultFormat(); + foreach (var gen in ordered.Skip(1)) + { + content.Append(", "); + gen.PrettyPrint(content, format); + content.switchToDefaultFormat(); + } + } + if (dependentGeneralizationLookup[true].Any()) + { + if (hasIndependent) + { + content.Append(" and corresponding term(s) "); + } + else + { + content.Append("For corresponding term(s) "); + } + + var ordered = dependentGeneralizationLookup[true].OrderBy(gen => -gen.id); + ordered.First().PrettyPrint(content, format); + content.switchToDefaultFormat(); + foreach (var gen in ordered.Skip(1)) + { + content.Append(", "); + gen.PrettyPrint(content, format); + content.switchToDefaultFormat(); + } + } + content.Append(":\n"); + } + } + + private static void printGeneralizedTermWithPrerequisites(InfoPanelContent content, PrettyPrintFormat format, GeneralizationState generalizationState, ISet alreadyIntroducedGeneralizations, + Term term, BindingInfo bindingInfo, List assocTerms, bool last, List> recursiveEqualityExplanations) + { + generalizationState.tmpHighlightGeneralizedTerm(format, term, bindingInfo, last); + + var newlyIntroducedGeneralizations = term.GetAllGeneralizationSubtermsAndDependencies() + .GroupBy(gen => gen.generalizationCounter).Select(group => group.First()) + .Where(gen => !alreadyIntroducedGeneralizations.Contains(gen.generalizationCounter)); + PrintNewlyIntroducedGeneralizations(content, format, newlyIntroducedGeneralizations); + alreadyIntroducedGeneralizations.UnionWith(newlyIntroducedGeneralizations.Select(gen => gen.generalizationCounter)); + + var distinctBlameTerms = bindingInfo.getDistinctBlameTerms(); + var termNumber = format.termNumbers[term]; + var numberingString = $"({termNumber}) "; + content.switchToDefaultFormat(); + content.Append(numberingString); + term.PrettyPrint(content, format, numberingString.Length); + content.Append('\n'); + + if (last) + { + if (generalizationState.HasGeneralizationsForNextIteration()) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nTerms for the Next Iteration:\n\n"); + content.switchToDefaultFormat(); + generalizationState.PrintGeneralizationsForNextIteration(content, format); + } + + if (bindingInfo.getBindingsToFreeVars().Any()) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nBindings to Start Next Iteration:\n\n"); + content.switchToDefaultFormat(); + + foreach (var binding in bindingInfo.getBindingsToFreeVars()) + { + if (binding.Value == null) + { + content.Append($"A generalized binding for {binding.Key.PrettyName} in the next iteration\ncould not be generated (This pattern cannot repeat indefinetly)."); + } + else + { + content.Append(binding.Key.PrettyName).Append(" will be bound to:\n"); + binding.Value.PrettyPrint(content, format); + content.switchToDefaultFormat(); + content.Append("\n\n"); + } + } + } + + return; + } + + if (bindingInfo.equalities.Count > 0) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nRelevant equalities:\n"); + content.switchToDefaultFormat(); + var equalitySetLookup = bindingInfo.equalities.ToLookup(eq => eq.Key.ContainsGeneralization() || eq.Value.Any(t => t.Item2.ContainsGeneralization())); + + format.printContextSensitive = false; + if (equalitySetLookup[true].Any()) + { + foreach (var equality in equalitySetLookup[true]) + { + var effectiveTerm = bindingInfo.bindings[equality.Key].Item2; + foreach (var t in equality.Value.Select(t => t.Item2).Distinct(Term.semanticTermComparer)) + { + content.Append('\n'); + termNumber = format.GetEqualityNumber(t, effectiveTerm); + + EqualityExplanation explanation; +#if !DEBUG + try + { +#endif + explanation = bindingInfo.EqualityExplanations.First(ee => ee.source.id == t.id && ee.target.id == effectiveTerm.id); +#if !DEBUG + } + catch (Exception) + { + explanation = new TransitiveEqualityExplanation(term, effectiveTerm, new EqualityExplanation[0]); + } +#endif + var isRecursive = EqualityExplanationIsRecursiveVisitor.singleton.visit(explanation, null); + if (isRecursive) + { + recursiveEqualityExplanations.Add(Tuple.Create(termNumber, explanation)); + } + + if (format.ShowEqualityExplanations && !isRecursive) + { + var newlyIntroducedGeneralizationTerms = new List(); + EqualityExplanationTermVisitor.singleton.visit(explanation, u => newlyIntroducedGeneralizationTerms.AddRange(u.GetAllGeneralizationSubterms())); + + newlyIntroducedGeneralizations = newlyIntroducedGeneralizationTerms + .GroupBy(gen => gen.generalizationCounter).Select(group => group.First()) + .Where(gen => !alreadyIntroducedGeneralizations.Contains(gen.generalizationCounter)); + PrintNewlyIntroducedGeneralizations(content, format, newlyIntroducedGeneralizations); + alreadyIntroducedGeneralizations.UnionWith(newlyIntroducedGeneralizations.Select(gen => gen.generalizationCounter)); + + explanation.PrettyPrint(content, format, termNumber); + } + else + { + newlyIntroducedGeneralizations = t.GetAllGeneralizationSubtermsAndDependencies() + .Concat(effectiveTerm.GetAllGeneralizationSubtermsAndDependencies()) + .GroupBy(gen => gen.generalizationCounter).Select(group => group.First()) + .Where(gen => !alreadyIntroducedGeneralizations.Contains(gen.generalizationCounter)); + PrintNewlyIntroducedGeneralizations(content, format, newlyIntroducedGeneralizations); + alreadyIntroducedGeneralizations.UnionWith(newlyIntroducedGeneralizations.Select(gen => gen.generalizationCounter)); + + numberingString = $"({termNumber}) "; + content.switchToDefaultFormat(); + content.Append(numberingString); + var indentString = $"¦{String.Join("", Enumerable.Repeat(" ", numberingString.Length - 1))}"; + t.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + content.Append($"\n{indentString}= (explanation omitted)\n{indentString}"); + effectiveTerm.PrettyPrint(content, format, numberingString.Length); + } + content.switchToDefaultFormat(); + content.Append('\n'); + } + } + } + + if (equalitySetLookup[false].Any()) + { + foreach (var equality in equalitySetLookup[false]) + { + var effectiveTerm = bindingInfo.bindings[equality.Key].Item2; + foreach (var t in equality.Value.Select(t => t.Item2).Distinct(Term.semanticTermComparer)) + { + content.Append('\n'); + termNumber = format.GetEqualityNumber(t, effectiveTerm); + + EqualityExplanation explanation; +#if !DEBUG + try + { +#endif + explanation = bindingInfo.EqualityExplanations.First(ee => ee.source.id == t.id && ee.target.id == effectiveTerm.id); +#if !DEBUG + } + catch (Exception) + { + explanation = new TransitiveEqualityExplanation(term, effectiveTerm, new EqualityExplanation[0]); + } +#endif + var isRecursive = EqualityExplanationIsRecursiveVisitor.singleton.visit(explanation, null); + if (isRecursive) + { + recursiveEqualityExplanations.Add(Tuple.Create(termNumber, explanation)); + } + + + if (format.ShowEqualityExplanations && !isRecursive) + { + var newlyIntroducedGeneralizationTerms = new List(); + EqualityExplanationTermVisitor.singleton.visit(explanation, u => newlyIntroducedGeneralizationTerms.AddRange(u.GetAllGeneralizationSubterms())); + + newlyIntroducedGeneralizations = newlyIntroducedGeneralizationTerms + .GroupBy(gen => gen.generalizationCounter).Select(group => group.First()) + .Where(gen => !alreadyIntroducedGeneralizations.Contains(gen.generalizationCounter)); + PrintNewlyIntroducedGeneralizations(content, format, newlyIntroducedGeneralizations); + alreadyIntroducedGeneralizations.UnionWith(newlyIntroducedGeneralizations.Select(gen => gen.generalizationCounter)); + + explanation.PrettyPrint(content, format, termNumber); + } + else + { + newlyIntroducedGeneralizations = t.GetAllGeneralizationSubtermsAndDependencies() + .Concat(effectiveTerm.GetAllGeneralizationSubtermsAndDependencies()) + .GroupBy(gen => gen.generalizationCounter).Select(group => group.First()) + .Where(gen => !alreadyIntroducedGeneralizations.Contains(gen.generalizationCounter)); + PrintNewlyIntroducedGeneralizations(content, format, newlyIntroducedGeneralizations); + alreadyIntroducedGeneralizations.UnionWith(newlyIntroducedGeneralizations.Select(gen => gen.generalizationCounter)); + + numberingString = $"({termNumber}) "; + content.switchToDefaultFormat(); + content.Append(numberingString); + var indentString = $"¦{String.Join("", Enumerable.Repeat(" ", numberingString.Length - 1))}"; + t.PrettyPrint(content, format, numberingString.Length); + content.switchToDefaultFormat(); + content.Append($"\n{indentString}= (explanation omitted)\n{indentString}"); + effectiveTerm.PrettyPrint(content, format, numberingString.Length); + } + content.switchToDefaultFormat(); + content.Append('\n'); + } + } + } + format.printContextSensitive = true; + + bindingInfo.PrintEqualitySubstitution(content, format); + } + + var bindingsToFreeVars = bindingInfo.getBindingsToFreeVars(); + if (bindingsToFreeVars.Any()) + { + content.switchFormat(PrintConstants.SubtitleFont, PrintConstants.sectionTitleColor); + content.Append("\nBinding information:"); + content.switchToDefaultFormat(); + + foreach (var bindings in bindingsToFreeVars) + { + content.Append("\n\n"); + content.Append(bindings.Key.PrettyName).Append(" was bound to:\n"); + bindings.Value.PrettyPrint(content, format); + content.switchToDefaultFormat(); + } + + content.Append("\n"); + } + } + + private class EqualityExplanationShifter : EqualityExplanationVisitor + { + public static readonly EqualityExplanationShifter singleton = new EqualityExplanationShifter(); + + private static Term MakePrime(Term t) + { + if (t.id >= 0) return t; + var newArgs = t.Args.Select(a => a.iterationOffset == 0 ? MakePrime(a) : RemoveIterationOffset(a)).ToArray(); + return new Term(t, newArgs) { isPrime = true }; + } + + private static Term RemoveIterationOffset(Term t) + { + if (t.iterationOffset == 0) return t; + var newArgs = t.Args.Select(a => a.iterationOffset == 0 ? MakePrime(a) : RemoveIterationOffset(a)).ToArray(); + return new Term(t, newArgs) { iterationOffset = 0 }; + } + + public override EqualityExplanation Direct(DirectEqualityExplanation target, int arg) + { + var newSource = target.source.iterationOffset == 0 ? MakePrime(target.source) : RemoveIterationOffset(target.source); + var newTarget = target.target.iterationOffset == 0 ? MakePrime(target.target) : RemoveIterationOffset(target.target); + var newEquality = target.equality.iterationOffset == 0 ? MakePrime(target.equality) : RemoveIterationOffset(target.equality); + return new DirectEqualityExplanation(newSource, newTarget, newEquality); + } + + public override EqualityExplanation Transitive(TransitiveEqualityExplanation target, int arg) + { + var newSource = target.source.iterationOffset == 0 ? MakePrime(target.source) : RemoveIterationOffset(target.source); + var newTarget = target.target.iterationOffset == 0 ? MakePrime(target.target) : RemoveIterationOffset(target.target); + var newEqualities = target.equalities.Select(ee => visit(ee, arg)).ToArray(); + return new TransitiveEqualityExplanation(newSource, newTarget, newEqualities); + } + + public override EqualityExplanation Congruence(CongruenceExplanation target, int arg) + { + var newSource = target.source.iterationOffset == 0 ? MakePrime(target.source) : RemoveIterationOffset(target.source); + var newTarget = target.target.iterationOffset == 0 ? MakePrime(target.target) : RemoveIterationOffset(target.target); + var newEqualities = target.sourceArgumentEqualities.Select(ee => visit(ee, arg)).ToArray(); + return new CongruenceExplanation(newSource, newTarget, newEqualities); + } + + public override EqualityExplanation Theory(TheoryEqualityExplanation target, int arg) + { + var newSource = target.source.iterationOffset == 0 ? MakePrime(target.source) : RemoveIterationOffset(target.source); + var newTarget = target.target.iterationOffset == 0 ? MakePrime(target.target) : RemoveIterationOffset(target.target); + return new TheoryEqualityExplanation(newSource, newTarget, target.TheoryName); + } + + public override EqualityExplanation RecursiveReference(RecursiveReferenceEqualityExplanation target, int arg) + { + var newSource = target.source.iterationOffset == 0 ? MakePrime(target.source) : RemoveIterationOffset(target.source); + var newTarget = target.target.iterationOffset == 0 ? MakePrime(target.target) : RemoveIterationOffset(target.target); + return new RecursiveReferenceEqualityExplanation(newSource, newTarget, target.ReferencedExplanation, 0, target.GenerationOffset == 0); + } + } + + private class EqualityExplanationIsRecursiveVisitor : EqualityExplanationVisitor + { + public static readonly EqualityExplanationIsRecursiveVisitor singleton = new EqualityExplanationIsRecursiveVisitor(); + + private static bool HasRecursiveTerm(EqualityExplanation target) + { + return target.source.ReferencesOtherIteration() || target.target.ReferencesOtherIteration(); + } + + public override bool Direct(DirectEqualityExplanation target, object arg) + { + return HasRecursiveTerm(target); + } + + public override bool Transitive(TransitiveEqualityExplanation target, object arg) + { + return HasRecursiveTerm(target) || target.equalities.Any(e => visit(e, arg)); + } + + public override bool Congruence(CongruenceExplanation target, object arg) + { + return HasRecursiveTerm(target) || target.sourceArgumentEqualities.Any(e => visit(e, arg)); + } + + public override bool Theory(TheoryEqualityExplanation target, object arg) + { + return HasRecursiveTerm(target); + } + + public override bool RecursiveReference(RecursiveReferenceEqualityExplanation target, object arg) + { + return true; + } + } + + private class EqualityExplanationShiftCollector : EqualityExplanationVisitor + { + public static readonly EqualityExplanationShiftCollector singleton = new EqualityExplanationShiftCollector(); + + private static int CombineShifts(int s1, int s2) + { + if (s1 == 0) return s2; + if (s2 == 0) return s1; + if (s1 == s2) return s1; + return -1; + } + + public override int Direct(DirectEqualityExplanation target, object arg) + { + var shift = target.source.iterationOffset; + shift = CombineShifts(shift, target.target.iterationOffset); + shift = CombineShifts(shift, target.equality.iterationOffset); + + return shift; + } + + public override int Transitive(TransitiveEqualityExplanation target, object arg) + { + var shift = target.source.iterationOffset; + shift = CombineShifts(shift, target.target.iterationOffset); + foreach (var equalityExplanation in target.equalities) + { + shift = CombineShifts(shift, visit(equalityExplanation, arg)); + if (shift == -1) break; + } + + return shift; + } + + public override int Congruence(CongruenceExplanation target, object arg) + { + var shift = target.source.iterationOffset; + shift = CombineShifts(shift, target.target.iterationOffset); + foreach (var equalityExplanation in target.sourceArgumentEqualities) + { + shift = CombineShifts(shift, visit(equalityExplanation, arg)); + if (shift == -1) break; + } + + return shift; + } + + public override int Theory(TheoryEqualityExplanation target, object arg) + { + return CombineShifts(target.source.iterationOffset, target.target.iterationOffset); + } + + public override int RecursiveReference(RecursiveReferenceEqualityExplanation target, object arg) + { + var shift = target.source.iterationOffset; + shift = CombineShifts(shift, target.target.iterationOffset); + shift = CombineShifts(shift, target.GenerationOffset); + + return shift; + } } } } From c16b7df147a10b5819dab46654de451061cb9082 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 8 Aug 2021 21:12:45 -0700 Subject: [PATCH 48/60] bug fix, still had runtime error --- source/QuantifierModel/InstantiationSubgraph.cs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs index 8cbb519..19b8cb3 100644 --- a/source/QuantifierModel/InstantiationSubgraph.cs +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -328,6 +328,7 @@ public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) cycle.Add(subgraphInstantiations[i].Quant); } GeneralizationState generalizationState = new GeneralizationState(cycleSize, subgraphInstantiations); + generalizationState.generalize(); if (generalizationState.TrueLoop) { @@ -462,6 +463,7 @@ public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) insts.MoveNext(); var recursiveEqualityExplanations = new List>(); var firstStep = generalizationState.generalizedTerms.First(); + printGeneralizedTermWithPrerequisites(content, format, generalizationState, alreadyIntroducedGeneralizations, firstStep.Item1, firstStep.Item2, firstStep.Item3, false, recursiveEqualityExplanations); var count = 1; From 2df1beafc11396868098a6e80d8e21bb80707897 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Mon, 9 Aug 2021 10:05:26 -0700 Subject: [PATCH 49/60] updated infopanel for subgraph --- source/CycleDetection/CycleDetection.cs | 10 ++++--- source/DAGView.cs | 2 +- .../QuantifierModel/InstantiationSubgraph.cs | 29 +++++++++++++++---- 3 files changed, 31 insertions(+), 10 deletions(-) diff --git a/source/CycleDetection/CycleDetection.cs b/source/CycleDetection/CycleDetection.cs index 8c00743..cee3f96 100644 --- a/source/CycleDetection/CycleDetection.cs +++ b/source/CycleDetection/CycleDetection.cs @@ -251,6 +251,8 @@ public class GeneralizationState private static readonly EqualityExplanation[] emptyEqualityExplanations = new EqualityExplanation[0]; + public bool isPath = false; + public GeneralizationState(int cycleLength, IEnumerable instantiations) { loopInstantiations = new List[cycleLength]; @@ -319,7 +321,7 @@ public void generalize() var interestingBoundTos = new List(); var interestingExplicitBoundTermIdxs = new List(); var theoryConstraintExplanationGeneralizer = new TheoryConstraintExplanationGeneralizer(this); - + for (var it = 0; it < loopInstantiationsWorkSpace.Length+1; it++) { var i = (loopInstantiationsWorkSpace.Length + it - 1) % loopInstantiationsWorkSpace.Length; @@ -356,7 +358,7 @@ public void generalize() } } - if (it == 0) + if (it == 0 && isPath) { /* The first term in the matching loop explanation is not produced by a loop instantiation (and may not necessarily * have been produced by a quantifier that occurs in the loop). We therefore need to extract the terms to run the generalization @@ -375,9 +377,9 @@ public void generalize() c.bindingInfo.bindings.Where(kv => p.dependentTerms.Contains(kv.Value.Item2, Term.semanticTermComparer)).Select(kv => kv.Key)); var boundTo = boundToCandidates.Skip(1).Aggregate(new HashSet(boundToCandidates.First()), (set, iterationResult) => { - set.IntersectWith(iterationResult); return set; }).FirstOrDefault(); + if (boundTo == null) throw new Exception("Couldn't generalize!"); interestingBoundTos.Add(boundTo); @@ -418,7 +420,7 @@ public void generalize() parentConcreteTerm = parent.concreteBody; generalizedYield = generalizeYieldTermPointWise(loopInstantiationsWorkSpace[i], loopInstantiationsWorkSpace[j], nextBindingInfo, j <= i, isWrapInstantiation); } - + //This will later be used to find out which quantifier was used to generate this term. generalizedYield.Responsible = loopInstantiationsWorkSpace[i].First(); generalizedYield.dependentInstantiationsBlame.Add(loopInstantiationsWorkSpace[j].First()); diff --git a/source/DAGView.cs b/source/DAGView.cs index f54fc76..0daddf8 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -574,7 +574,7 @@ private void pathExplanationButton_Click(object sender, EventArgs e) subgraph = new List>() { path }; FoundPattern: highlightSubgraph(ref subgraph); - InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, subgraph[0].Count); + InstantiationSubgraph instSubgraph = new InstantiationSubgraph(ref subgraph, subgraph[0].Count, cycleSize); _z3AxiomProfiler.UpdateSync(instSubgraph); _viewer.Invalidate(); #if !DEBUG diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs index 19b8cb3..1a7db85 100644 --- a/source/QuantifierModel/InstantiationSubgraph.cs +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -13,10 +13,13 @@ class InstantiationSubgraph : IPrintable private readonly List subgraphInstantiations; // number of elements in cycle (the repeating strucutre) private int cycleSize; + // number of elements in cycle (when it was just a path) + private int simpleSize; - public InstantiationSubgraph(ref List> subgraph, int size) + public InstantiationSubgraph(ref List> subgraph, int size, int simpleSZ) { cycleSize = size; + simpleSize = simpleSZ; subgraphInstantiations = new List(); foreach (List cycle in subgraph) { @@ -33,20 +36,28 @@ public InstantiationSubgraph(ref List> subgraph, int size) // To generate the info panel content public void InfoPanelText(InfoPanelContent content, PrettyPrintFormat format) { - if ((subgraphInstantiations.Count / cycleSize) < 3) + if (simpleSize == cycleSize) { - PrintPathInfo(content, format);; + if ((subgraphInstantiations.Count / cycleSize) < 3) + { + PrintPathWithNoLoopInfo(content, format); ; + } + else + { + PrintCycleInfo(content, format); + } } else { PrintCycleInfo(content, format); } + } // When there is no repeating cycle // only take the first cycle even when there are two // Requires the subgraph to be a path - public void PrintPathInfo(InfoPanelContent content, PrettyPrintFormat format) + public void PrintPathWithNoLoopInfo(InfoPanelContent content, PrettyPrintFormat format) { content.switchFormat(PrintConstants.TitleFont, PrintConstants.defaultTextColor); content.Append("Path explanation:"); @@ -328,6 +339,7 @@ public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) cycle.Add(subgraphInstantiations[i].Quant); } GeneralizationState generalizationState = new GeneralizationState(cycleSize, subgraphInstantiations); + if (simpleSize != cycleSize) generalizationState.isPath = false; generalizationState.generalize(); if (generalizationState.TrueLoop) @@ -355,7 +367,14 @@ public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) { content.Append("Pattern: "); } - content.Append(string.Join(" -> ", cycle.Select(quant => quant.PrintName))); + if (simpleSize == cycleSize) + { + content.Append(string.Join(" -> ", cycle.Select(quant => quant.PrintName))); + } else + { + content.Append(string.Join(" , ", cycle.Select(quant => quant.PrintName))); + } + content.Append("\n"); printPreamble(content, true); From ef2d8d511becb654e3dc59d475a8eb8cd64f5463 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Mon, 9 Aug 2021 10:32:58 -0700 Subject: [PATCH 50/60] changes to DAGView --- source/DAGView.cs | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 0daddf8..1a373c5 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -564,6 +564,9 @@ private void pathExplanationButton_Click(object sender, EventArgs e) extendedPathStat.Add(GetPathInfo(ref upPath, pathPatternSize[i], i)); } extendedPathStat.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); + + Console.WriteLine("pathlength " + extendedPaths[extendedPathStat[0].Item4].Count); + // send to FindSubgrpah() to construct subgraph from the path subgraph = FindSubgraph(extendedPaths[extendedPathStat[0].Item4], extendedPathStat[0].Item3, positionOfSelectedNode); cycleSize = extendedPathStat[0].Item3; @@ -693,10 +696,13 @@ public static List> AllDownPatterns(Node node, int bound) { Patterns.Add(CurPattern); } + } else + { + List NewPattern = new List(CurPattern); + NewPattern.Add(ChildQuant); + PathStack.Add(new Tuple>(Child, NewPattern)); } - List NewPattern = new List(CurPattern); - NewPattern.Add(ChildQuant); - PathStack.Add(new Tuple>(Child, NewPattern)); + } } return Patterns; @@ -731,10 +737,12 @@ public static List> AllUpPatterns(Node node, int bound) { Patterns.Add(CurPattern); } + } else + { + List NewPattern = new List(CurPattern); + NewPattern.Add(ChildQuant); + PathStack.Add(new Tuple>(Parent, NewPattern)); } - List NewPattern = new List(CurPattern); - NewPattern.Add(ChildQuant); - PathStack.Add(new Tuple>(Parent, NewPattern)); } } return Patterns; @@ -898,6 +906,7 @@ public static List> FindSubgraph(List path, int cycleSize, int // Condition 2: // if the user selected some node in the first full cycle, it is unclear how we can bound it // so we won't bother find the repeating strucutre + Console.WriteLine("pos " + pos + " dd " + (cycleSize + (path.Count % cycleSize))); if ((repetition < 4) || (pos < (cycleSize + (path.Count % cycleSize)))) return subgraph; List> cloneOfSubgraph = new List>(subgraph); From 204d3de1299b827d15a78cf89e37438c4835e74d Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 10 Aug 2021 16:33:29 -0700 Subject: [PATCH 51/60] fix match same term bug --- source/CycleDetection/CycleDetection.cs | 3 ++- source/DAGView.cs | 16 +++++----------- 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/source/CycleDetection/CycleDetection.cs b/source/CycleDetection/CycleDetection.cs index cee3f96..3356105 100644 --- a/source/CycleDetection/CycleDetection.cs +++ b/source/CycleDetection/CycleDetection.cs @@ -251,10 +251,11 @@ public class GeneralizationState private static readonly EqualityExplanation[] emptyEqualityExplanations = new EqualityExplanation[0]; - public bool isPath = false; + public bool isPath; public GeneralizationState(int cycleLength, IEnumerable instantiations) { + isPath = true; loopInstantiations = new List[cycleLength]; for (var i = 0; i < loopInstantiations.Length; i++) { diff --git a/source/DAGView.cs b/source/DAGView.cs index 1a373c5..67729c9 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -565,8 +565,6 @@ private void pathExplanationButton_Click(object sender, EventArgs e) } extendedPathStat.Sort((elem1, elem2) => DAGView.CustomPathComparer(ref elem1, ref elem2)); - Console.WriteLine("pathlength " + extendedPaths[extendedPathStat[0].Item4].Count); - // send to FindSubgrpah() to construct subgraph from the path subgraph = FindSubgraph(extendedPaths[extendedPathStat[0].Item4], extendedPathStat[0].Item3, positionOfSelectedNode); cycleSize = extendedPathStat[0].Item3; @@ -881,7 +879,7 @@ public static List> FindSubgraph(List path, int cycleSize, int subgraph.Add(newPath); return subgraph; } - int start = cycleSize + (path.Count % cycleSize); + int start = path.Count % cycleSize; if ((repetition < 4) || (pos < (cycleSize + (path.Count % cycleSize)))) start = 0; int counter = 0; List cycle = new List(); @@ -906,24 +904,20 @@ public static List> FindSubgraph(List path, int cycleSize, int // Condition 2: // if the user selected some node in the first full cycle, it is unclear how we can bound it // so we won't bother find the repeating strucutre - Console.WriteLine("pos " + pos + " dd " + (cycleSize + (path.Count % cycleSize))); if ((repetition < 4) || (pos < (cycleSize + (path.Count % cycleSize)))) return subgraph; List> cloneOfSubgraph = new List>(subgraph); int bound = GetDepth(path[path.Count % cycleSize]); List> generalStruct = new List>(); - List generalCycle = new List(); - for (int i = path.Count % cycleSize; i < cycleSize + (path.Count % cycleSize); i++) - { - generalCycle.Add(path[i]); - } - generalCycle.AddRange(subgraph[0]); + List generalCycle = new List(subgraph[0]); + generalCycle.AddRange(subgraph[1]); FindGeneralStructure(generalCycle, ref generalStruct, bound); + if (generalStruct.Count == subgraph[0].Count) return subgraph; Node curNode; int subgraphsize = subgraph.Count; - for (int i = 0; i < subgraphsize; i++) + for (int i = 1; i < subgraphsize; i++) { counter = 0; Queue queue = new Queue(); From 1ccb5c91040b0da94186a8c3218024223b5ae436 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 10 Aug 2021 16:39:30 -0700 Subject: [PATCH 52/60] finding subgrpah bug fix --- source/DAGView.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 67729c9..bf1d6b1 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -916,8 +916,9 @@ public static List> FindSubgraph(List path, int cycleSize, int if (generalStruct.Count == subgraph[0].Count) return subgraph; Node curNode; + subgraph.RemoveAt(0); int subgraphsize = subgraph.Count; - for (int i = 1; i < subgraphsize; i++) + for (int i = 0; i < subgraphsize; i++) { counter = 0; Queue queue = new Queue(); From 4190cfa43da850ac9e4605e925e0e30daf663b52 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 10 Aug 2021 17:23:31 -0700 Subject: [PATCH 53/60] find subgraph bug fix --- source/DAGView.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index bf1d6b1..98d7582 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -913,7 +913,7 @@ public static List> FindSubgraph(List path, int cycleSize, int List generalCycle = new List(subgraph[0]); generalCycle.AddRange(subgraph[1]); FindGeneralStructure(generalCycle, ref generalStruct, bound); - if (generalStruct.Count == subgraph[0].Count) return subgraph; + //if (generalStruct.Count == subgraph[0].Count) return subgraph; Node curNode; subgraph.RemoveAt(0); @@ -949,6 +949,7 @@ public static List> FindSubgraph(List path, int cycleSize, int if (l < (generalStruct[counter].Count - 1)) return cloneOfSubgraph; counter++; } + if ((i == 0) && (subgraph[0].Count == cloneOfSubgraph[0].Count)) return cloneOfSubgraph; } From e46dd87fc7da230f567ac6e14bc8ea512ffc95f3 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Tue, 10 Aug 2021 17:24:45 -0700 Subject: [PATCH 54/60] delted useless comment --- source/DAGView.cs | 1 - 1 file changed, 1 deletion(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 98d7582..5e2beb7 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -913,7 +913,6 @@ public static List> FindSubgraph(List path, int cycleSize, int List generalCycle = new List(subgraph[0]); generalCycle.AddRange(subgraph[1]); FindGeneralStructure(generalCycle, ref generalStruct, bound); - //if (generalStruct.Count == subgraph[0].Count) return subgraph; Node curNode; subgraph.RemoveAt(0); From e2b2d798398b17b4c9bb75d23cadf9a34e7e2179 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Wed, 11 Aug 2021 08:46:32 -0700 Subject: [PATCH 55/60] deleted test cases that no longer applies --- UnitTestProject1/UnitTest1.cs | 44 ----------------------------------- 1 file changed, 44 deletions(-) diff --git a/UnitTestProject1/UnitTest1.cs b/UnitTestProject1/UnitTest1.cs index f48afb0..35c8843 100644 --- a/UnitTestProject1/UnitTest1.cs +++ b/UnitTestProject1/UnitTest1.cs @@ -54,28 +54,6 @@ public void TestAllDownPattern4() Assert.AreEqual(1, result.Count); Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); } - - // Test if AllDownPatterns recogizes pattern that contain - // multiple occurences of the same quantifier in the same cycle - [TestMethod] - public void TestAllDownPattern5() - { - List> result = DAGView.AllDownPatterns(Graphs.graph6.FindNode("A"), 8); - List expected1 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; - List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0], Graphs.Quants[2] }; - List expected3 = new List() { Graphs.Quants[0], Graphs.Quants[1], - Graphs.Quants[0], Graphs.Quants[2], Graphs.Quants[0], Graphs.Quants[1] }; - List expected4 = new List() { Graphs.Quants[0] }; - List expected5 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1] }; - List expected6 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0] }; - Assert.AreEqual(6, result.Count); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected2)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected3)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected4)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected5)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected6)); - } } [TestClass] @@ -210,28 +188,6 @@ public void TestAllUpPattern4() Assert.AreEqual(1, result.Count); Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); } - - // Test if AllDownPatterns recogizes pattern that contain - // multiple occurences of the same quantifier in the same cycle - [TestMethod] - public void TestAllUpPatterns5() - { - List> result = DAGView.AllUpPatterns(Graphs.graph7.FindNode("A"), 8); - List expected1 = new List() { Graphs.Quants[0], Graphs.Quants[1] }; - List expected2 = new List() { Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0], Graphs.Quants[2] }; - List expected3 = new List() { Graphs.Quants[0], Graphs.Quants[1], - Graphs.Quants[0], Graphs.Quants[2], Graphs.Quants[0], Graphs.Quants[1] }; - List expected4 = new List() { Graphs.Quants[0] }; - List expected5 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1] }; - List expected6 = new List() { Graphs.Quants[0], Graphs.Quants[0], Graphs.Quants[1], Graphs.Quants[0] }; - Assert.AreEqual(6, result.Count); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected1)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected2)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected3)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected4)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected5)); - Assert.IsTrue(DAGView.ContainPattern(ref result, ref expected6)); - } } // Similar to ExtendDownwards, but up From 7d1433ec6e29a7aff84ae0d74cc1a35ffc45f90b Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Wed, 11 Aug 2021 09:33:57 -0700 Subject: [PATCH 56/60] order of cycleInstantiations changed --- source/DAGView.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/source/DAGView.cs b/source/DAGView.cs index 5e2beb7..333cd05 100644 --- a/source/DAGView.cs +++ b/source/DAGView.cs @@ -1000,8 +1000,8 @@ public static Quantifier GetQuant(Node node) public static int ParentComparer(Node a, Node b) { int deptha = GetDepth(a), depthb = GetDepth(b); - if (deptha < depthb) return 1; - if (deptha > depthb) return -1; + if (deptha < depthb) return -1; + if (deptha > depthb) return 1; return string.Compare(GetQuant(a).Qid, GetQuant(b).Qid); } } From 4e1f204940bfe9c23d8c3eca3b0d1dea0de53e0a Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Thu, 19 Aug 2021 17:40:15 -0700 Subject: [PATCH 57/60] CycleDetection, deleted a 'if debug' this is debugg seems unnecesary --- source/CycleDetection/CycleDetection.cs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/source/CycleDetection/CycleDetection.cs b/source/CycleDetection/CycleDetection.cs index 3356105..1a4b962 100644 --- a/source/CycleDetection/CycleDetection.cs +++ b/source/CycleDetection/CycleDetection.cs @@ -717,11 +717,7 @@ private void GeneralizeEqualityExplanations(int instIndex) return eeCollector; }).ToList(); -#if DEBUG - if (equalityExplanations.Any(l => l.Count == 0)) throw new Exception("Found no concrete explanations."); -#else equalityExplanations = equalityExplanations.Where(l => l.Count != 0).ToList(); -#endif var recursionPointFinder = new RecursionPointFinder(); generalizedBindingInfo.EqualityExplanations = equalityExplanations.Select(list => { From a4633654e5d8fcff1cf5b628b06338fff33ad197 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Fri, 20 Aug 2021 10:17:48 -0700 Subject: [PATCH 58/60] Console output fix the newly added line after [assin] in z3 log will no longer cause 'wrongline' in console --- source/LogProcessor.cs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/source/LogProcessor.cs b/source/LogProcessor.cs index b19c1b7..6d6103a 100644 --- a/source/LogProcessor.cs +++ b/source/LogProcessor.cs @@ -44,6 +44,7 @@ public class LogProcessor private static readonly char[] splitAtSpace = new char[] { ' ' }; private static readonly Regex varNamesParser = new Regex(@"\(\s*((?:\|[^\|\\]*\|)|[\w\d~!@$%^&*_\-+=<>.?/]*)\s*;\s*((?:\|[^\|\\]*\|)|[\w\d~!@$%^&*_\-+=<>.?/]*)\)"); private static readonly Regex idParser = new Regex(@"((?:\|[^\|\\]*\|)|[\w\d~!@$%^&*_\-+=<>.?/]*)#(\d*)"); + public bool lastLineStartedWithAssign = false; public LogProcessor(List bplFileInfos, bool skipDecisions, int cons) { @@ -298,6 +299,12 @@ public void ParseSingleLine(string line) { return; } + // The following condition is added to the newly added line in z3 log does not + // output wongline in console + if (lastLineStartedWithAssign && (words[0][0] != '[')) + { + return; + } ParseTraceLine(line, words); } @@ -897,6 +904,7 @@ private int ParseIdentifierRootNamespace(string idString) private void ParseTraceLine(string line, string[] words) { + lastLineStartedWithAssign = false; switch (words[0]) { case "[tool-version]": @@ -1248,6 +1256,7 @@ private void ParseTraceLine(string line, string[] words) case "[assign]": { + lastLineStartedWithAssign = true; if (!interestedInCurrentCheck) break; if (skipDecisions || words.Length < 2) break; ScopeDesc d = model.scopes[model.scopes.Count - 1]; From c649cc8a849275fd99b573f4a54df2a85d0600e9 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 22 Aug 2021 09:19:05 -0700 Subject: [PATCH 59/60] bug fix fixed the index out of bound error when clicking explain subgraph --- source/QuantifierModel/InstantiationSubgraph.cs | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs index 1a7db85..97cb604 100644 --- a/source/QuantifierModel/InstantiationSubgraph.cs +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -36,17 +36,11 @@ public InstantiationSubgraph(ref List> subgraph, int size, int simple // To generate the info panel content public void InfoPanelText(InfoPanelContent content, PrettyPrintFormat format) { - if (simpleSize == cycleSize) + if ((subgraphInstantiations.Count / cycleSize) < 3) { - if ((subgraphInstantiations.Count / cycleSize) < 3) - { - PrintPathWithNoLoopInfo(content, format); ; - } - else - { - PrintCycleInfo(content, format); - } - } else + PrintPathWithNoLoopInfo(content, format); ; + } + else { PrintCycleInfo(content, format); } @@ -338,6 +332,8 @@ public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) { cycle.Add(subgraphInstantiations[i].Quant); } + Console.WriteLine("cycle length " + cycleSize); + Console.WriteLine("cycle instantiatons size " + subgraphInstantiations.Count); GeneralizationState generalizationState = new GeneralizationState(cycleSize, subgraphInstantiations); if (simpleSize != cycleSize) generalizationState.isPath = false; generalizationState.generalize(); From a445a89d9915b1d1037eff61cde13b654603ef46 Mon Sep 17 00:00:00 2001 From: Tiger Wu Date: Sun, 22 Aug 2021 09:21:10 -0700 Subject: [PATCH 60/60] deleted useless line --- source/QuantifierModel/InstantiationSubgraph.cs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/source/QuantifierModel/InstantiationSubgraph.cs b/source/QuantifierModel/InstantiationSubgraph.cs index 97cb604..34385f8 100644 --- a/source/QuantifierModel/InstantiationSubgraph.cs +++ b/source/QuantifierModel/InstantiationSubgraph.cs @@ -332,8 +332,7 @@ public void PrintCycleInfo(InfoPanelContent content, PrettyPrintFormat format) { cycle.Add(subgraphInstantiations[i].Quant); } - Console.WriteLine("cycle length " + cycleSize); - Console.WriteLine("cycle instantiatons size " + subgraphInstantiations.Count); + GeneralizationState generalizationState = new GeneralizationState(cycleSize, subgraphInstantiations); if (simpleSize != cycleSize) generalizationState.isPath = false; generalizationState.generalize();