summaryrefslogtreecommitdiff
path: root/Source/AIFramework/Mutable.ssc
blob: 894359ef768a6b8d367da07a2e4e08c71b78dfb3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework.Collections
{
    using System.Collections;   
    using Microsoft.Contracts;

    /// <summary>
    ///  Extend sets for using as a IWorkList.
    /// </summary>
    public class WorkSet : Microsoft.Boogie.Set, Microsoft.Boogie.IWorkList
    {
      
        // See Bug #148 for an explanation of why this is here.
        // Without it, the contract inheritance rules will complain since it
        // has nowhere to attach the out-of-band contract it gets from
        // ICollection.Count that it gets from IWorkList.
        [Pure][Reads(ReadsAttribute.Reads.Owned)]
        public override int Count { get { return base.Count; } }

        [Pure][Reads(ReadsAttribute.Reads.Owned)] public bool IsEmpty()
        {
            return Count == 0;
        }

        /// <summary>
        ///  Pull an element out of the workset.
        /// </summary>
        public object Pull()
        {
            IEnumerator iter = GetEnumerator();
            iter.MoveNext();

            object result = (!)iter.Current;
            Remove(result);

            return result;
        }
        
        bool Microsoft.Boogie.IWorkList.Add(object o){
          if (o == null) throw new System.ArgumentNullException();
          this.Add(o);
          return true;
        }
        bool Microsoft.Boogie.IWorkList.AddAll(IEnumerable objs){
          if (objs == null) throw new System.ArgumentNullException();
          return this.AddAll(objs);
        }
        
        // ICollection members
        public void CopyTo (System.Array! a, int i) { 
          if (this.Count > a.Length - i) throw new System.ArgumentException();
          int j = i; 
          foreach(object o in this){
            a.SetValue(o, j++);
          }
          return;
        }
        object! ICollection.SyncRoot { [Pure] get { return this; } }
        public bool IsSynchronized { get { return false; } }
          
    }
}

namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
{
    using System.Collections.Generic;

    public class HashMultiset<T>
    {
        private readonly IDictionary<T,int>! dict;
        
        //invariant forall{KeyValuePair<T,int> entry in dict; entry.Value >= 1};
        
        public HashMultiset()
        {
            this.dict = new Dictionary<T,int>();
            // base();
        }
        
        public HashMultiset(int size)
        {
            this.dict = new Dictionary<T,int>(size);
            // base();
        }
        
        public void Add(T t)
        { expose (this) {
            if (dict.ContainsKey(t))
            {
                dict[t] = dict[t] + 1;
            }
            else
            {
                dict.Add(t,1);
            }
        }}
        
        public void Remove(T t)
        {
            if (dict.ContainsKey(t))
            { expose (this) {
                int count = dict[t];
                if (count == 1) { dict.Remove(t); }
                else { dict[t] = count - 1; }
            }}
        }
        
        public bool Contains(T t)
        {
            return dict.ContainsKey(t);
        }
    }
}