blob: 280e93e9c71fe387664e61b09f659ac5da8d9655 (
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
|
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 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 Z3TypeBuilder builder;
private Dictionary<BvType, Z3Type> bvTypes = new Dictionary<BvType, Z3Type>(new BvTypeComparator());
private Dictionary<BasicType, Z3Type> basicTypes = new Dictionary<BasicType, Z3Type>(new BasicTypeComparator());
public Z3TypeCachedBuilder(Z3TypeBuilder builder)
{
this.builder = builder;
}
private Z3Type GetBvType(BvType bvType)
{
if (!bvTypes.ContainsKey(bvType))
{
Z3Type typeAst = builder.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 = builder.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
throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
}
}
public class Z3Type { }
interface Z3TypeBuilder
{
Z3Type BuildBvType(BvType bvType);
Z3Type BuildBasicType(BasicType basicType);
}
}
|
