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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
using System;
using System.Collections;
using System.Collections.Generic;
using System.Threading;
using System.IO;
using System.Diagnostics;
using Microsoft.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie;
using Microsoft.Boogie.Z3;
using Microsoft.Z3;
using Microsoft.Boogie.VCExprAST;
namespace Microsoft.Boogie.Z3
{
internal class Z3TypeCachedBuilder
{
private class MapTypeComparator : IEqualityComparer<MapType>
{
public bool Equals(MapType x, MapType y)
{
if (x.MapArity != y.MapArity)
return false;
for (int i = 0; i < x.MapArity; i++)
{
if (!Equals(x.Arguments[i], y.Arguments[i]))
return false;
}
return Equals(x.Result, y.Result);
}
public int GetHashCode(MapType mapType)
{
return mapType.GetHashCode();
}
}
private class BvTypeComparator : IEqualityComparer<BvType>
{
public bool Equals(BvType x, BvType y)
{
return x.Bits == y.Bits;
}
public int GetHashCode(BvType bvType)
{
return bvType.Bits;
}
}
private class BasicTypeComparator : IEqualityComparer<BasicType>
{
public bool Equals(BasicType x, BasicType y)
{
return (x.IsBool == y.IsBool) &&
(x.IsInt == y.IsInt);
}
public int GetHashCode(BasicType basicType)
{
if (basicType.IsBool)
return 1;
else if (basicType.IsInt)
return 2;
else
throw new Exception("Basic Type " + basicType.ToString() + " is unkwown");
}
}
private Dictionary<MapType, Z3Type> mapTypes = new Dictionary<MapType, Z3Type>(new MapTypeComparator());
private Dictionary<BvType, Z3Type> bvTypes = new Dictionary<BvType, Z3Type>(new BvTypeComparator());
private Dictionary<BasicType, Z3Type> basicTypes = new Dictionary<BasicType, Z3Type>(new BasicTypeComparator());
private Z3Context container;
public Z3TypeCachedBuilder(Z3Context context)
{
this.container = context;
}
private Z3Type GetMapType(MapType mapType)
{
Context z3 = ((Z3SafeContext)container).z3;
if (!mapTypes.ContainsKey(mapType))
{
Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1");
Z3Type domain = GetType(mapType.Arguments[0]);
Z3Type range = GetType(mapType.Result);
Z3Type typeAst = BuildMapType(domain, range);
mapTypes.Add(mapType, typeAst);
}
Z3Type result;
bool containsKey = mapTypes.TryGetValue(mapType, out result);
Debug.Assert(containsKey);
return result;
}
private Z3Type GetBvType(BvType bvType)
{
if (!bvTypes.ContainsKey(bvType))
{
Z3Type typeAst = BuildBvType(bvType);
bvTypes.Add(bvType, typeAst);
}
Z3Type result;
bool containsKey = bvTypes.TryGetValue(bvType, out result);
Debug.Assert(containsKey);
return result;
}
private Z3Type GetBasicType(BasicType basicType)
{
if (!basicTypes.ContainsKey(basicType))
{
Z3Type typeAst = BuildBasicType(basicType);
basicTypes.Add(basicType, typeAst);
}
Z3Type result;
bool containsKey = basicTypes.TryGetValue(basicType, out result);
Debug.Assert(containsKey);
return result;
}
public virtual Z3Type GetType(Type boogieType)
{
if (boogieType.GetType().Equals(typeof(BvType)))
return GetBvType((BvType)boogieType);
else if (boogieType.GetType().Equals(typeof(BasicType)))
return GetBasicType((BasicType)boogieType);
else if (boogieType.GetType().Equals(typeof(MapType)))
return GetMapType((MapType)boogieType);
else
throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
}
private Z3Type WrapType(Sort typeAst)
{
return new Z3SafeType(typeAst);
}
public Z3Type BuildMapType(Z3Type domain, Z3Type range)
{
Context z3 = ((Z3SafeContext)container).z3;
Sort typeAst = z3.MkArraySort(((Z3SafeType)domain).TypeAst, ((Z3SafeType)range).TypeAst);
return WrapType(typeAst);
}
public Z3Type BuildBvType(BvType bvType)
{
Context z3 = ((Z3SafeContext)container).z3;
Sort typeAst = z3.MkBvSort((uint)bvType.Bits);
return WrapType(typeAst);
}
public Z3Type BuildBasicType(BasicType basicType)
{
Context z3 = ((Z3SafeContext)container).z3;
Sort typeAst;
if (basicType.IsBool)
{
typeAst = z3.MkBoolSort();
}
else if (basicType.IsInt)
{
typeAst = z3.MkIntSort();
}
else
throw new Exception("Unknown Basic Type " + basicType.ToString());
return WrapType(typeAst);
}
}
public class Z3Type { }
}
|
