Minor fixes

1 files changed, 140 insertions, 67 deletions

diff --git a/Source/VCGeneration/DoomedStrategy.cs b/Source/VCGeneration/DoomedStrategy.cs
index 74ac0657..18de31c7 100644
--- a/Source/VCGeneration/DoomedStrategy.cs
+++ b/Source/VCGeneration/DoomedStrategy.cs
@@ -37,35 +37,35 @@ namespace VC
         protected BlockHierachy m_BlockH = null;

 

         protected int m_MaxBranchingDepth = 0;

-        protected int m_MaxMinElemPerPath = 0;

+        protected int m_MaxK = 0;

+

+        protected Stopwatch sw = new Stopwatch();

 

 

         // This is the List with all detected doomed program points. This List is used by VCDoomed.cs to 

         // create an error message

         public List<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();

 

+        private List<Block> __DEBUG_minelements = new List<Block>();

+

         // There is no default constructor, because these parameters are needed for most subclasses

         public DoomDetectionStrategy(Implementation imp, Block unifiedexit, List<Block> unreach) 

         {

             m_BlockH = new BlockHierachy(imp, unifiedexit);

             __DEBUG_EQCLeaf = m_BlockH.Leaves.Count;

+            

+            //foreach (BlockHierachyNode bhn in m_BlockH.Leaves)

+            //{

+            //    if (bhn.Content.Count > 0) __DEBUG_minelements.Add(bhn.Content[0]);

+            //}

+            //if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0);

+

 

-            if (imp.Blocks.Count>0) m_GatherInfo(imp.Blocks[0], 0, 0,0);

             if (__DEBUGOUT)

             {

-                Console.WriteLine("MaBranchingDepth {0}  MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxMinElemPerPath);

-                double avgplen = 0, avglpp=0;

-                foreach (int i in __pathLength)

-                { 

-                    avgplen+=i;

-                }

-                foreach (int i in __leavespp)

-                {

-                    avglpp += i;

-                }

-                avglpp = (__leavespp.Count > 0) ? avglpp / (double)__leavespp.Count : 1;

-                avgplen = (__pathLength.Count > 0) ? avgplen / (double)__pathLength.Count : 1;

-                Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", avglpp, avgplen);

+                Console.WriteLine("MaBranchingDepth {0}  MaxMinPP {1} ", m_MaxBranchingDepth, m_MaxK);

+

+                Console.WriteLine("AvgLeaverPerPath {0} AvgPLen {1}", 0, 0);

             }

 

             MaxBlocks = imp.Blocks.Count;

@@ -74,7 +74,6 @@ namespace VC
             __DEBUG_BlocksTotal = imp.Blocks.Count;

         }

 

-

         public int MaxBlocks, MinBlocks;

         public bool HACK_NewCheck;

 

@@ -116,14 +115,9 @@ namespace VC
             if (b.Predecessors.Length > 1) branchingdepth--;

 

             GotoCmd gc = b.TransferCmd as GotoCmd;

-            BlockHierachyNode bhn = null;

-            if (m_BlockH.BlockToHierachyMap.TryGetValue(b, out bhn))

-            {

-                if (m_BlockH.Leaves.Contains(bhn)) leavespp++;

-            }

-            m_MaxMinElemPerPath = (leavespp > m_MaxMinElemPerPath) ? leavespp : m_MaxMinElemPerPath;

+            if (__DEBUG_minelements.Contains(b)) leavespp++;

             plen++;

-            if (gc != null)

+            if (gc != null && gc.labelTargets.Length>0)

             {

                 if (gc.labelTargets.Length > 1) branchingdepth++;

                 m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth;

@@ -136,11 +130,12 @@ namespace VC
             {

                 __pathLength.Add(plen);

                 __leavespp.Add(leavespp);

+                m_MaxK = (m_MaxK > leavespp) ? m_MaxK : leavespp;

             }

-

         }

 

 

+

     }

     #endregion

 

@@ -206,6 +201,7 @@ namespace VC
 

         override public bool GetNextBlock(out  List<Block> lb)

         {

+            sw.Start();

             if (m_Current < m_Blocks.Count)

             {

                 lb = new List<Block>();

@@ -230,6 +226,10 @@ namespace VC
             {

                 m_doomedBlocks.Add(m_Blocks[m_Current - 1]);

             }

+            if (__DEBUGOUT) Console.WriteLine("K := {0,3} , out {1,8}, time {2,12}", MaxBlocks, outcome, sw.ElapsedTicks);

+            sw.Stop();

+            sw.Reset();

+

             return true;

         }

     }

@@ -299,7 +299,7 @@ namespace VC
     }

     #endregion

 

-    #region Path Cover Optimization

+    #region Path Cover Optimization with L

     internal class PathCoverStrategy : DoomDetectionStrategy

     {

         List<Block> m_Uncheckedlocks = new List<Block>();

@@ -312,26 +312,113 @@ namespace VC
 

         public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> unreach)

             : base(imp, unifiedexit, unreach)

-        {

+        {            

             m_Ignore = unreach;

             HACK_NewCheck = true;

             impl = imp;

             foreach (BlockHierachyNode bhn in m_BlockH.Leaves)

             {

-                //foreach (Block b in h.Content)

-                //{

-                //    m_Uncheckedlocks.Add(b);

-                //}

                 if (bhn.Content.Count > 0)

                 {

                     m_Uncheckedlocks.Add(bhn.Content[0]);

                 }

 

             }

-            MaxBlocks = m_Uncheckedlocks.Count;

+            m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);

+            MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0);

+            MaxBlocks = -1;

+        }

+

+        override public bool GetNextBlock(out  List<Block> lb)

+        {

+            sw.Start();

+

+            lb = new List<Block>();

+

+            if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves)

+            {

+                if (m_Uncheckedlocks.Count > 0)

+                {

+                    DetectedBlock.Add(m_BlockH.GetOtherDoomedBlocks(m_Uncheckedlocks));

+                }

+

+                return false;

+            }

+

+            lb.AddRange(m_Uncheckedlocks);

+

+            return true;

+        }

+

+        override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)

+        {

+            this.__DEBUG_BlocksChecked++;            

+            // Valid means infeasible...            

+            int oldl = MinBlocks;

+            int oldsize = m_Uncheckedlocks.Count;

+

+

+            if (outcome == ProverInterface.Outcome.Valid)

+            {

+                this.__DEBUG_InfeasibleTraces++;

+                if (MinBlocks == 1)

+                {

+                    m_NoMoreMoves = true;

+                }

+                else

+                {

+                    MinBlocks = 1;

+                }

+            }

+            else if (outcome == ProverInterface.Outcome.Invalid)

+            {

+                this.__DEBUG_TracesChecked++;

+                

+                List<Block> errortrace = m_GetErrorTraceFromCE(cb);

+                foreach (Block b in errortrace)

+                {

+                    if (m_Uncheckedlocks.Contains(b))

+                    {

+                        m_Uncheckedlocks.Remove(b);

+                    }

+                }

+                cb.TraceNodes.Clear();

+                m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);

+                if (m_MaxK < 1)

+                {

+                    m_NoMoreMoves = true; m_Uncheckedlocks.Clear();

+                }

+                MinBlocks = m_MaxK / 2 + (m_MaxK % 2 > 0 ? 1 : 0);

+                //if (MinBlocks > m_MaxK) MinBlocks = m_MaxK;

+                

+            }

+            else

+            {

+                m_NoMoreMoves = true; m_Uncheckedlocks.Clear();

+            }

+            if (__DEBUGOUT) 

+                Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", MaxBlocks, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks);

+            sw.Stop();

+            sw.Reset();

+            return true;

         }

 

-        public PathCoverStrategy(Implementation imp, Block unifiedexit, List<Block> unreach, bool test_alternativeK)

+

+    }

+    #endregion

+

+    #region Path Cover Optimization with K

+    internal class PathCoverStrategyK : DoomDetectionStrategy

+    {

+        List<Block> m_Uncheckedlocks = new List<Block>();

+        List<Block> m_Ignore = new List<Block>();

+

+        Random m_Random = new Random();

+        bool m_NoMoreMoves = false;

+

+        private List<Block> m_foundBlock = new List<Block>();

+

+        public PathCoverStrategyK(Implementation imp, Block unifiedexit, List<Block> unreach)

             : base(imp, unifiedexit, unreach)

         {

             m_Ignore = unreach;

@@ -339,20 +426,16 @@ namespace VC
             impl = imp;

             foreach (BlockHierachyNode bhn in m_BlockH.Leaves)

             {

-                //foreach (Block b in h.Content)

-                //{

-                //    m_Uncheckedlocks.Add(b);

-                //}

                 if (bhn.Content.Count > 0)

                 {

                     m_Uncheckedlocks.Add(bhn.Content[0]);

                 }

 

-            }            

+            }

+

+            m_MaxK = m_BlockH.GetMaxK(m_Uncheckedlocks);

+

             MaxBlocks = m_Uncheckedlocks.Count;

-            if (test_alternativeK) 

-            {

-                m_CountUncheckedPP(impl.Blocks[0], 0);

                 if (m_MaxK < m_Uncheckedlocks.Count && m_MaxK > 0)

                 {

                     MaxBlocks = m_MaxK;

@@ -365,33 +448,13 @@ namespace VC
                 {

                     MaxBlocks = 1;

                 }

-                Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks);

-            }                                

-        }

-

-        int m_MaxK = 0;

-

-        private void m_CountUncheckedPP(Block b, int localmax)

-        {

-            if (m_Uncheckedlocks.Contains(b)) localmax++;

-

-            GotoCmd gc = b.TransferCmd as GotoCmd;

-            if (gc != null && gc.labelTargets.Length>0)

-            {

-                foreach (Block s in gc.labelTargets)

-                {

-                    m_CountUncheckedPP(s, localmax);

-                }

-            }

-            else

-            {

-                m_MaxK = (localmax > m_MaxK) ? localmax : m_MaxK;

-            }

-

+                //Console.WriteLine("InitK {0}, Max {1}", m_MaxK, MaxBlocks);

         }

 

         override public bool GetNextBlock(out  List<Block> lb)

         {

+            sw.Start();

+

             lb = new List<Block>();

 

             if (m_Uncheckedlocks.Count == 0 || m_NoMoreMoves)

@@ -405,17 +468,20 @@ namespace VC
             }

 

             lb.AddRange(m_Uncheckedlocks);

-            MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks;

-            MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0);                       

 

+            MaxBlocks = MaxBlocks > m_Uncheckedlocks.Count ? m_Uncheckedlocks.Count : MaxBlocks;

+            MinBlocks = MaxBlocks / 2 + (MaxBlocks % 2 > 0 ? 1 : 0);

             return true;

         }

 

         override public bool SetCurrentResult(List<Variable> reachvar, ProverInterface.Outcome outcome, DoomErrorHandler cb)

         {

             this.__DEBUG_BlocksChecked++;

-            //Console.WriteLine(outcome);

             // Valid means infeasible...

+            int oldk = MaxBlocks;

+            int oldl = MinBlocks;

+            int oldsize = m_Uncheckedlocks.Count;

+

             if (outcome == ProverInterface.Outcome.Valid)

             {

                 this.__DEBUG_InfeasibleTraces++;

@@ -431,7 +497,7 @@ namespace VC
             else if (outcome == ProverInterface.Outcome.Invalid)

             {

                 this.__DEBUG_TracesChecked++;

-                //int oldsize = m_Uncheckedlocks.Count;

+

                 List<Block> errortrace = m_GetErrorTraceFromCE(cb);

                 foreach (Block b in errortrace)

                 {

@@ -441,11 +507,18 @@ namespace VC
                     }

                 }

                 cb.TraceNodes.Clear();

+

+                int k = m_BlockH.GetMaxK(m_Uncheckedlocks);

+                MaxBlocks = (k > MaxBlocks) ? MaxBlocks : k;

             }

             else

             {

                 m_NoMoreMoves = true; m_Uncheckedlocks.Clear();

             }

+            if (__DEBUGOUT) 

+                Console.WriteLine("K := {0,3}, L := {1,3}, deltaSp {2,3}, out {3,8}, time {4,8}", oldk, oldl, (oldsize - m_Uncheckedlocks.Count), outcome, sw.ElapsedTicks);

+            sw.Stop();

+            sw.Reset();

             return true;

         }