Automata.dll functions are used to create Automata from Graph

1 files changed, 417 insertions, 158 deletions

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 989e9472..87fe44e2 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -1,6 +1,5 @@
 #if QED

 

-

 using System;

 using System.Collections;

 using System.Collections.Generic;

@@ -8,11 +7,12 @@ using System.Collections.Generic;
 using System.Linq;

 using System.Text;

 using Microsoft.Boogie;

-//! using Microsoft.Automata;

+using Microsoft.Automata;

 

 using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie.GraphUtil;

+

 namespace Microsoft.Boogie

 {

     /*

@@ -20,17 +20,18 @@ namespace Microsoft.Boogie
      * 

      */

     class YieldTypeChecker

-    {/*

+    {

+        

           CharSetSolver yieldTypeCheckerAutomatonSolver;

           string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";

           Char[][] yieldTypeCheckerVocabulary;

           BvSet yielTypeCheckerBvSet;

           Automaton<BvSet> yieldTypeCheckerAutomaton;

-          */

+          

 

         private YieldTypeChecker()

         {

-            /*

+            

             yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);

             yieldTypeCheckerVocabulary = new char[][] {

                 new char[]{'1','2'},

@@ -44,7 +45,13 @@ namespace Microsoft.Boogie
             yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary);

             yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r

 

-            */

+            

+        }

+        public bool IsYieldTypeSafe(Automaton<BvSet> implTypeCheckAutomaton){

+

+            Automaton<BvSet> complYieldTypeSafeProp = this.yieldTypeCheckerAutomaton.Complement(this.yieldTypeCheckerAutomatonSolver);

+            

+            return true;

         }

 

         public static void AddChecker(LinearTypeChecker linearTypeChecker)

@@ -64,7 +71,7 @@ namespace Microsoft.Boogie
                             phaseNumSpecImpl = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);

 

                         }

-                        YieldTypeCheckerCore.TypeCheck(impl, phaseNumSpecImpl, 5);

+                        YieldTypeCheckerCore.TypeCheck(impl, phaseNumSpecImpl);

 

 

                     }

@@ -86,8 +93,7 @@ namespace Microsoft.Boogie
         int specPhaseNumImpl; // impl.proc's spec num

         int yTypeCheckCurrentPhaseNum;// current phase of yield type checking

         int programCounter; // initial state of the impl

-

-        //! Take of that : Dictionary<Tuple<int, int>, HashSet<int>> backwardEdgesPerYield; //backward edges per yield 

+        int concreteInitialState; // First seen initial state in an implementation

 

         HashSet<CallCmd> callCmdsInImpl; //  callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... }

         int numCallCmdInEnclosingProc; // Number of CallCmds in       

@@ -98,17 +104,17 @@ namespace Microsoft.Boogie
 

         List<Tuple<int, int>> phaseIntervals; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] intervals

 

-

-        private YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum, int currentPhsCheckNum)

+        

+        private YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum)

         {

             ytypeChecked = toTypeCheck;

             this.errorCount = 0;

             this.checkingContext = new CheckingContext(null);

             // numCallInEncImpl = 0;

             specPhaseNumImpl = specPhaseNum;

-            yTypeCheckCurrentPhaseNum = currentPhsCheckNum;

+            yTypeCheckCurrentPhaseNum = 0;

             programCounter = Math.Abs(Guid.NewGuid().GetHashCode());

-

+            concreteInitialState = programCounter;

 

             /*Utility Maps*/

             phaseIntervals = new List<Tuple<int, int>>();

@@ -117,22 +123,15 @@ namespace Microsoft.Boogie
 

             // Graph and Automaton

             yieldTypeCheckGraph = new HashSet<Tuple<int, int>>();

-            // yieldTypeCheckAutomaton = new Dictionary<Implementation, Automaton<YieldTypeSet>>();

             verticesToEdges = new Dictionary<Tuple<int, int>, string>();

-            /*Console.Write("\n Proc being checked is " + ytypeChecked.Proc.Name+ "\n"); 

-            Console.Write("\n Specnum is " + specPhaseNumImpl.ToString() + "\n");

-            Console.Write("\n PhaseCheckNum is " + yTypeCheckCurrentPhaseNum.ToString() + "\n");

-            */

         }

 

 

-

+        // return phase intervals

         private void CalculateCallCmds(Implementation impl)

         {

-            // HashSet<CallCmd> callCmdInBodyEncImpl = new HashSet<CallCmd>();

             List<CallCmd> callCmdInBodyEncImplList = new List<CallCmd>();

-

-

+            

             foreach (Block b in impl.Blocks)

             {

                 List<Cmd> cmds = new List<Cmd>();

@@ -183,23 +182,33 @@ namespace Microsoft.Boogie
                     phaseIntervals.Add(intervalToInsert);

                 }

             }

-

+            

         }

 

-        public static bool TypeCheck(Implementation impl, int specPhsNum, int checkPhsNum)

-        {

-

+        public Automaton<YieldTypeSet> YieldTypeCheckAutomata(YieldTypeCheckerCore yieldTypeCheckerPerImpl)

+        {              

+            

+            for (int i = 0; i<this.phaseIntervals.Count ; i++) {

+                yTypeCheckCurrentPhaseNum =  this.phaseIntervals[i].Item2 - 1;

+            }

 

-            YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(impl, specPhsNum, checkPhsNum);

-            yieldTypeCheckerPerImpl.CalculateCallCmds(impl);

             yieldTypeCheckerPerImpl.BuildAutomatonGraph();

-            Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));

-            //  yieldTypeCheckerPerImpl.BackwardEdgesOfYields(yieldTypeCheckerPerImpl.GetTuplesForGraph());

-            return true;

+            //Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));

+            yieldTypeCheckerPerImpl.PostProcessGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph());

+            return yieldTypeCheckerPerImpl.BuildAutomaton(yieldTypeCheckerPerImpl.GetTuplesForGraph());

+            

+        }

+

+        public static Automaton<YieldTypeSet> TypeCheck(Implementation impl, int specPhsNum)

+        {

+            YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(impl, specPhsNum);

+            return yieldTypeCheckerPerImpl.YieldTypeCheckAutomata(yieldTypeCheckerPerImpl);

         }

 

+      

 

-        public void BuildAutomatonGraph()

+

+        private void BuildAutomatonGraph()

         {

             foreach (Block block in ytypeChecked.Blocks)

             {

@@ -224,14 +233,14 @@ namespace Microsoft.Boogie
 

         }

 

-        public Graph<int> GetTuplesForGraph()

+        private Graph<int> GetTuplesForGraph()

         {

             Graph<int> graphFromTuples = new Graph<int>(yieldTypeCheckGraph);

             return graphFromTuples;

 

         }

 

-        public void AddNodeToGraph(Cmd cmd)

+        private void AddNodeToGraph(Cmd cmd)

         {

             if (cmd is AssignCmd)

             {

@@ -263,19 +272,15 @@ namespace Microsoft.Boogie
             {

 

                 CallCmd callCmd = cmd as CallCmd;

-                //  Console.Write(" Impelemtation is " + ytypeChecked.Proc.Name+ "\n");

-                // Console.Write("CallCmd PhaseCheck Num " + yTypeCheckCurrentPhaseNum.ToString() + "\n");

-                //Console.Write("CallCmd PhaseCheck Num "+specPhaseNumImpl.ToString() + "\n");

                 AddNodeToGraphForCallCmd(callCmd, yTypeCheckCurrentPhaseNum);

 

             }

         }

 

-        public void AddNodeToGraphForGotoCmd(GotoCmd cmd)

+        private void AddNodeToGraphForGotoCmd(GotoCmd cmd)

         {

             int source = programCounter;

             int dest = programCounter;//Math.Abs(Guid.NewGuid().GetHashCode());

-            //Console.Write("\n Program counter before goto " + source.ToString() +" \n");

             programCounter = dest;

 

             // Create a Epsilon transition between them

@@ -284,14 +289,14 @@ namespace Microsoft.Boogie
             verticesToEdges[srcdst] = "N";

         }

 

-        public void AddNodeToGraphForReturnCmd(ReturnCmd cmd)

+        private void AddNodeToGraphForReturnCmd(ReturnCmd cmd)

         {

 

             // Do nothing !

 

         }

 

-        public void AddNodeToGraphForYieldCmd(YieldCmd cmd)

+        private void AddNodeToGraphForYieldCmd(YieldCmd cmd)

         {

 

             int source = programCounter;

@@ -304,7 +309,7 @@ namespace Microsoft.Boogie
 

         }

 

-        public void AddNodeToGraphForAssignCmd(AssignCmd cmd)

+        private void AddNodeToGraphForAssignCmd(AssignCmd cmd)

         {

 

             int source = programCounter;

@@ -316,7 +321,7 @@ namespace Microsoft.Boogie
             verticesToEdges[srcdst] = "Q";

         }

 

-        public void AddNodeToGraphForHavocCmd(HavocCmd cmd)

+        private void AddNodeToGraphForHavocCmd(HavocCmd cmd)

         {

 

             int source = programCounter;

@@ -329,7 +334,7 @@ namespace Microsoft.Boogie
 

         }

 

-        public void AddNodeToGraphForAssumeCmd(AssumeCmd cmd)

+        private void AddNodeToGraphForAssumeCmd(AssumeCmd cmd)

         {

 

             int source = programCounter;

@@ -342,7 +347,7 @@ namespace Microsoft.Boogie
 

         }

 

-        public void AddNodeToGraphForAssertCmd(AssertCmd cmd)

+        private void AddNodeToGraphForAssertCmd(AssertCmd cmd)

         {

             int source = programCounter;

             int dest = Math.Abs(Guid.NewGuid().GetHashCode());

@@ -356,11 +361,10 @@ namespace Microsoft.Boogie
         }

 

 

-        public void AddNodeToGraphForCallCmd(CallCmd cmd, int currentCheckPhsNum)

+        private void AddNodeToGraphForCallCmd(CallCmd cmd, int currentCheckPhsNum)

         {

             int callePhaseNum = 0;

-            //Console.Write("\n Add CallCmd for " + cmd.Proc.Name +" is encountered ");

-

+            

             foreach (Ensures e in cmd.Proc.Ensures)

             {

                 callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);

@@ -370,15 +374,10 @@ namespace Microsoft.Boogie
             {

                 int source = Math.Abs(Guid.NewGuid().GetHashCode());

                 programCounter = source;

-                //  Console.Write(" New component with source state " + programCounter.ToString() + " generated");

             }

             else

             {

-                /*

-                Console.Write("\n Callee " + cmd.Proc.Name + " phase num is " + callePhaseNum.ToString());

-                Console.Write("\n Current phase check num is " + currentCheckPhsNum.ToString());

-                Console.Write("\n Program Counter is " + programCounter.ToString());

-            */

+          

 

                 foreach (Ensures e in cmd.Proc.Ensures)

                 {

@@ -428,7 +427,7 @@ namespace Microsoft.Boogie
         }

 

 

-        public Graph<int> CreateGrapFromHashSet(HashSet<Tuple<int, int>> grph)

+        private Graph<int> CreateGrapFromHashSet(HashSet<Tuple<int, int>> grph)

         {

 

             Graph<int> graphForAutomaton = new Graph<int>(grph);

@@ -449,156 +448,416 @@ namespace Microsoft.Boogie
             return s.ToString();

 

         }

-        /*

-        public void BackwardEdgesOfYields(Graph<int> graph)

-        {            

-            foreach (var e in graph.Edges)

-            {

-                var s = new StringBuilder();

-

-                if (verticesToEdges[e] == "Y")

+        

+        private HashSet<Tuple<int,int>> CollectBackEdges(Graph<int> g, Tuple<int,int> backEdge)

+        {           

+            int n = backEdge.Item1;

+            int d = backEdge.Item2;

+

+            HashSet<int> loop = new HashSet<int>();

+            Stack<int> stack = new Stack<int>();

+            HashSet<Tuple<int,int>> yieldReachingEdges = new HashSet<Tuple<int,int>>();

+            loop.Add(d);

+            if (!n.Equals(d)) // then n is not in loop

+            {

+                loop.Add(n);

+                stack.Push(n); // push n onto stack

+            }

+            while (stack.Count > 0) // not empty

+            {

+                int m = stack.Peek();

+              //  Console.Write("\n Back is : " + m.ToString()+ "\n");

+                stack.Pop(); // pop stack

+                foreach (int p in g.Predecessors(m))

                 {

-                    graph.Successors(e.Item1);

+                   // Contract.Assert(p!= null);

+                    if (!(loop.Contains(p)))

+                    {

+                        Tuple<int , int > yieldReaching = new Tuple<int,int>(p,m);

+                        yieldReachingEdges.Add(yieldReaching);

+                        //Console.Write("\n "+ p.ToString()+ " --> " + m.ToString() + "\n"); 

+                        loop.Add(p);

+                        stack.Push(p); // push p onto stack

+                    }

                 }

             }

-        }*/

+            return yieldReachingEdges;

+        }

+       

+        private HashSet<Tuple<int,int>> BackwardEdgesOfYields(Graph<int> graph)

+        {

+            HashSet<Tuple<int, int>> yieldTrueEdges = new HashSet<Tuple<int, int>>();

+            

+            foreach(var e in graph.Edges){

+               

+               

+                if(verticesToEdges[e] == "Y"){

+                   HashSet<Tuple<int,int>> yieldReachingEdges= CollectBackEdges(graph, e);

+                   foreach(Tuple<int,int> yldrch in yieldReachingEdges){

+                       // Console.Write("\n" + " From :"+yldrch.Item1.ToString() + " To :"+yldrch.Item2.ToString()+"\n");

+                        yieldTrueEdges.Add(yldrch);

+                    }

+                }

+            }

+            return yieldTrueEdges;

+        }

 

+        private void PostProcessGraph(Graph<int> graph)

+        {

+            HashSet<Tuple<int, int>> yieldTrueEdges = BackwardEdgesOfYields(graph);

 

 

+            foreach (Tuple<int, int> yldrch in yieldTrueEdges)

+            {

 

-        private void Error(Absy node, string message)

-        {

-            checkingContext.Error(node, message);

-            errorCount++;

-        }

+                if (verticesToEdges[yldrch] == "Q")

+                {

+                    verticesToEdges[yldrch] = "3";

+                }

+                else if (verticesToEdges[yldrch] == "P")

+                {

+                    verticesToEdges[yldrch] = "1";

+                }

+                else if (verticesToEdges[yldrch] == "B")

+                {

+                    verticesToEdges[yldrch] = "7";

+                }

+                else if (verticesToEdges[yldrch] == "R")

+                {

+                    verticesToEdges[yldrch] = "5";

+                }

+                else if (verticesToEdges[yldrch] == "L")

+                {

+                    verticesToEdges[yldrch] = "9";

+                }

+                else if (verticesToEdges[yldrch] == "A")

+                {

+                    verticesToEdges[yldrch] = "A";

+                }

+                else if (verticesToEdges[yldrch] == "Y")

+                {

+                    verticesToEdges[yldrch] = "D";

+                }

 

 

 

-        /*

-        internal class YieldTypeSet

-        {

-            uint elems;

+            }

+            foreach (Tuple<int, int> nyldrch in yieldTypeCheckGraph)

+            {

 

-            static internal YieldTypeSet Empty = new YieldTypeSet(0);

-            static internal YieldTypeSet Full = new YieldTypeSet(uint.MaxValue);

+                if (!yieldTrueEdges.Contains(nyldrch))

+                {

 

-            internal YieldTypeSet(uint elems)

-            {

-                this.elems = elems;

-            }

+                    if (verticesToEdges[nyldrch] == "Q")

+                    {

+                        verticesToEdges[nyldrch] = "4";

+                    }

+                    else if (verticesToEdges[nyldrch] == "P")

+                    {

+                        verticesToEdges[nyldrch] = "2";

+                    }

+                    else if (verticesToEdges[nyldrch] == "B")

+                    {

+                        verticesToEdges[nyldrch] = "8";

+                    }

+                    else if (verticesToEdges[nyldrch] == "R")

+                    {

+                        verticesToEdges[nyldrch] = "6";

+                    }

+                    else if (verticesToEdges[nyldrch] == "L")

+                    {

+                        verticesToEdges[nyldrch] = "C";

+                    }

+                    else if (verticesToEdges[nyldrch] == "A")

+                    {

+                        verticesToEdges[nyldrch] = "B";

+                    }                   

+                    

+                }

 

-            public override bool Equals(object obj)

-            {

-                YieldTypeSet s = obj as YieldTypeSet;

-                if (s == null)

-                    return false;

-                return elems == s.elems;

             }

+        }

+

+        private int[] ComputeFinalStates(Graph<int> graph)

+        {

 

-            public override int GetHashCode()

+            List<int> finalStatesList = new List<int>();

+            

+            foreach (int fe in graph.Nodes)

             {

-                return (int)elems;

+                foreach (Tuple<int, int> e in graph.Edges)

+                {

+                    if (!fe.Equals(e.Item1))

+                    {

+                        finalStatesList.Add(fe);

+                    }

+                }

             }

+            int[] finalStates = new int[finalStatesList.Count];

 

-            public YieldTypeSet Union(YieldTypeSet s)

-            {

-                return new YieldTypeSet(elems | s.elems);

+            for (int i = 0; i < finalStatesList.Count; i++) {

+                finalStates[i] = finalStatesList[i];            

             }

 

-            public YieldTypeSet Intersect(YieldTypeSet s)

+            return finalStates;

+        }

+

+        private List<int> ComputeInitalStates(Graph<int> graph) {

+

+            List<int> initialStates = new List<int>();

+            foreach (int fe in graph.Nodes)

             {

-                return new YieldTypeSet(elems & s.elems);

+                foreach (Tuple<int, int> e in graph.Edges)

+                {

+                    if (!fe.Equals(e.Item2))

+                    {

+                        initialStates.Add(fe);

+                    }

+                }

             }

+            return initialStates;

 

-            public YieldTypeSet Complement()

-            {

-                return new YieldTypeSet(~elems);

+        }

+        

+        private Automaton<YieldTypeSet> BuildAutomaton(Graph<int> graph) {

+            

+            List<Move<YieldTypeSet>> transitions = new List<Move<YieldTypeSet>>();

+         //   var solver = new YieldTypeSetSolver();

+

+            

+            foreach (Tuple<int, int> e in graph.Edges) {

+                

+                if (verticesToEdges[e] == "3")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.Q)));

+                }

+                else if (verticesToEdges[e] == "1")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.P)));

+                    

+                }

+                else if (verticesToEdges[e] == "7")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.B)));

+                }

+                else if (verticesToEdges[e] == "5")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.R)));

+                }

+                else if (verticesToEdges[e] == "9")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.L)));   

+                }

+                else if (verticesToEdges[e] == "A")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.A)));

+                }

+                else if (verticesToEdges[e] == "D")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.Y)));

+                }

+                else if (verticesToEdges[e] == "4")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.QF)));

+                }

+                else if (verticesToEdges[e] == "2")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.PF)));

+                }

+                else if (verticesToEdges[e] == "8")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.BF)));

+                }

+                else if (verticesToEdges[e] == "6")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.RF)));

+                }

+                else if (verticesToEdges[e] == "C")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.LF)));

+                }

+                else if (verticesToEdges[e] == "B")

+                {

+                    transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.AF)));    

+               

+                }

+                else if (verticesToEdges[e] == "N") { 

+                      transitions.Add(Move<YieldTypeSet>.Epsilon(e.Item1,e.Item2));  

+                

+                }

+            

             }

 

-            public override string ToString()

-            {

-                return string.Format("YieldTypeSet(0x{0})", elems.ToString("X"));

+            // get initial states 

+            List<int> initialStates = ComputeInitalStates(graph);

+            // get final states

+            int[] finalStates = ComputeFinalStates(graph);

+            // put Epslion from first initial state seen to other initial states created

+

+            foreach (int s in initialStates) {

+                // Put every one epsilon to itself no problem

+                /*if (!s.Equals(concreteInitialState)) { }*/

+                transitions.Add(Move<YieldTypeSet>.Epsilon(concreteInitialState,s));

             }

+

+

+            //create Automaton

+            Automaton<YieldTypeSet> yieldTypeCheckAutomaton = Automaton<YieldTypeSet>.Create(concreteInitialState, finalStates, transitions); ;

+            

+            return yieldTypeCheckAutomaton;

+

         }

 

 

-        internal class YieldTypeSetSolver : IBoolAlgMinterm<YieldTypeSet>

+        

+        private void Error(Absy node, string message)

         {

+            checkingContext.Error(node, message);

+            errorCount++;

+        }

+ 

 

-            MintermGenerator<YieldTypeSet> mtg; //use the default built-in minterm generator

-            internal YieldTypeSetSolver()

-            {

-                //create the minterm generator for this solver

-                mtg = new MintermGenerator<YieldTypeSet>(this);

-            }

 

-            public bool AreEquivalent(YieldTypeSet predicate1, YieldTypeSet predicate2)

-            {

-                return predicate1.Equals(predicate2);

-            }

+    }

 

-            public YieldTypeSet False

-            {

-                get { return YieldTypeSet.Empty; }

-            }

+    static class Transitions

+    {

 

-            public YieldTypeSet MkAnd(IEnumerable<YieldTypeSet> predicates)

-            {

-                YieldTypeSet res = YieldTypeSet.Full;

-                foreach (var s in predicates)

-                    res = res.Intersect(s);

-                return res;

-            }

+        public static uint P = 0x1;

+        public static uint Q = 0x4;

+        public static uint Y = 0x1000;

+        public static uint R = 0x10;

+        public static uint B = 0x40;

+        public static uint A = 0x200;

+        public static uint L = 0x100;

+        public static uint PF = 0x2;

+        public static uint QF = 0x8;

+        public static uint BF = 0x80;

+        public static uint RF = 0x20;

+        public static uint LF = 0x800;

+        public static uint AF = 0x400;

 

-            public YieldTypeSet MkNot(YieldTypeSet predicate)

-            {

-                return predicate.Complement();

-            }

 

-            public YieldTypeSet MkOr(IEnumerable<YieldTypeSet> predicates)

-            {

-                YieldTypeSet res = YieldTypeSet.Empty;

-                foreach (var s in predicates)

-                    res = res.Union(s);

-                return res;

-            }

+    }

 

-            public YieldTypeSet True

-            {

-                get { return YieldTypeSet.Full; }

-            }

+    public class YieldTypeSet

+    {

+        uint elems;

 

-            public bool IsSatisfiable(YieldTypeSet predicate)

-            {

-                return !predicate.Equals(YieldTypeSet.Empty);

-            }

+        static internal YieldTypeSet Empty = new YieldTypeSet(0);

+        static internal YieldTypeSet Full = new YieldTypeSet(uint.MaxValue);

 

-            public YieldTypeSet MkAnd(YieldTypeSet predicate1, YieldTypeSet predicate2)

-            {

-                return predicate1.Intersect(predicate2);

-            }

+        public YieldTypeSet(uint elems)

+        {

+            this.elems = elems;

+        }

 

-            public YieldTypeSet MkOr(YieldTypeSet predicate1, YieldTypeSet predicate2)

-            {

-                return predicate1.Union(predicate2);

-            }

+        public override bool Equals(object obj)

+        {

+            YieldTypeSet s = obj as YieldTypeSet;

+            if (s == null)

+                return false;

+            return elems == s.elems;

+        }

 

-            public IEnumerable<Pair<bool[], YieldTypeSet>> GenerateMinterms(params YieldTypeSet[] constraints)

-            {

-                return mtg.GenerateMinterms(constraints);

-            }

-            public YieldTypeSet Simplify(YieldTypeSet s)

-            {

-                return s;

+        public override int GetHashCode()

+        {

+            return (int)elems;

+        }

 

-            }

-        }*/

+        public YieldTypeSet Union(YieldTypeSet s)

+        {

+            return new YieldTypeSet(elems | s.elems);

+        }

+

+        public YieldTypeSet Intersect(YieldTypeSet s)

+        {

+            return new YieldTypeSet(elems & s.elems);

+        }

+

+        public YieldTypeSet Complement()

+        {

+            return new YieldTypeSet(~elems);

+        }

+

+        public override string ToString()

+        {

+            return string.Format("YieldTypeSet(0x{0})", elems.ToString("X"));

+        }

+    }

+

+

+    public class YieldTypeSetSolver : IBoolAlgMinterm<YieldTypeSet>

+    {

+

+        MintermGenerator<YieldTypeSet> mtg; //use the default built-in minterm generator

+        YieldTypeSetSolver()

+        {

+            //create the minterm generator for this solver

+            mtg = new MintermGenerator<YieldTypeSet>(this);

+        }

+

+        public bool AreEquivalent(YieldTypeSet predicate1, YieldTypeSet predicate2)

+        {

+            return predicate1.Equals(predicate2);

+        }

+

+        public YieldTypeSet False

+        {

+            get { return YieldTypeSet.Empty; }

+        }

+

+        public YieldTypeSet MkAnd(IEnumerable<YieldTypeSet> predicates)

+        {

+            YieldTypeSet res = YieldTypeSet.Full;

+            foreach (var s in predicates)

+                res = res.Intersect(s);

+            return res;

+        }

+

+        public YieldTypeSet MkNot(YieldTypeSet predicate)

+        {

+            return predicate.Complement();

+        }

+

+        public YieldTypeSet MkOr(IEnumerable<YieldTypeSet> predicates)

+        {

+            YieldTypeSet res = YieldTypeSet.Empty;

+            foreach (var s in predicates)

+                res = res.Union(s);

+            return res;

+        }

+

+        public YieldTypeSet True

+        {

+            get { return YieldTypeSet.Full; }

+        }

 

+        public bool IsSatisfiable(YieldTypeSet predicate)

+        {

+            return !predicate.Equals(YieldTypeSet.Empty);

+        }

 

+        public YieldTypeSet MkAnd(YieldTypeSet predicate1, YieldTypeSet predicate2)

+        {

+            return predicate1.Intersect(predicate2);

+        }

 

+        public YieldTypeSet MkOr(YieldTypeSet predicate1, YieldTypeSet predicate2)

+        {

+            return predicate1.Union(predicate2);

+        }

 

+        public IEnumerable<Pair<bool[], YieldTypeSet>> GenerateMinterms(params YieldTypeSet[] constraints)

+        {

+            return mtg.GenerateMinterms(constraints);

+        }

+        public YieldTypeSet Simplify(YieldTypeSet s)

+        {

+            return s;

+

+        }

     }

 }

 

-

 #endif
\ No newline at end of file