fixed z3api so that it works on small examples now.

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