diff options
Diffstat (limited to 'Source/Provers/Z3api/TypeAdapter.cs')
-rw-r--r-- | Source/Provers/Z3api/TypeAdapter.cs | 92 |
1 files changed, 81 insertions, 11 deletions
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index 280e93e9..0d79bd5a 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -15,6 +15,26 @@ 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)
@@ -46,20 +66,38 @@ namespace Microsoft.Boogie.Z3 }
}
- private Z3TypeBuilder builder;
+ 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;
+ }
- public Z3TypeCachedBuilder(Z3TypeBuilder builder)
+ private Z3Type GetMapType(MapType mapType)
{
- this.builder = builder;
+ 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 = builder.BuildBvType(bvType);
+ Z3Type typeAst = BuildBvType(bvType);
bvTypes.Add(bvType, typeAst);
}
Z3Type result;
@@ -72,7 +110,7 @@ namespace Microsoft.Boogie.Z3 {
if (!basicTypes.ContainsKey(basicType))
{
- Z3Type typeAst = builder.BuildBasicType(basicType);
+ Z3Type typeAst = BuildBasicType(basicType);
basicTypes.Add(basicType, typeAst);
}
Z3Type result;
@@ -87,16 +125,48 @@ namespace Microsoft.Boogie.Z3 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");
}
- }
- public class Z3Type { }
+ private Z3Type WrapType(Sort typeAst)
+ {
+ return new Z3SafeType(typeAst);
+ }
- interface Z3TypeBuilder
- {
- Z3Type BuildBvType(BvType bvType);
- Z3Type BuildBasicType(BasicType basicType);
+ 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 { }
}
\ No newline at end of file |