various fixes to port to latest version of Microsoft.Z3.dll

4 files changed, 52 insertions, 22 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 3a9c74ae..e6ba7b66 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -20,11 +20,6 @@ namespace Microsoft.Boogie.Z3
         private string logFilename;

         private List<string> debugTraces = new List<string>();

 

-        public void SetModelCompletion(bool enabled)

-        {

-            config.SetParamValue("MODEL_VALUE_COMPLETION", (enabled ? "true" : "false"));

-        }

-

         public void SetModel(bool enabled)

         {

             config.SetParamValue("MODEL", (enabled ? "true" : "false"));

@@ -109,15 +104,17 @@ namespace Microsoft.Boogie.Z3
     internal class PartitionMap

     {

         private Context ctx;

+        private Model model;

         private Dictionary<Term, int> termToPartition = new Dictionary<Term, int>();

         private Dictionary<object, int> valueToPartition = new Dictionary<object, int>();

         private List<Object> partitionToValue = new List<Object>();

         private int partitionCounter = 0;

         public int PartitionCounter { get { return partitionCounter; } }

 

-        public PartitionMap(Context ctx)

+        public PartitionMap(Context ctx, Model z3Model)

         { 

-            this.ctx = ctx; 

+            this.ctx = ctx;

+            this.model = z3Model;

         }

 

         public int GetPartition(Term value)

@@ -158,7 +155,7 @@ namespace Microsoft.Boogie.Z3
                     return BigNum.FromString(ctx.GetNumeralString(v));

                 }

             }

-            else if (ctx.TryGetArrayValue(v, out av))

+            else if (model.TryGetArrayValue(v, out av))

             {

                 List<List<int>> arrayValue = new List<List<int>>();

                 List<int> tuple;

@@ -249,10 +246,10 @@ namespace Microsoft.Boogie.Z3
         private Z3Context container;

         private PartitionMap partitionMap;

 

-        public BoogieErrorModelBuilder(Z3Context container)

+        public BoogieErrorModelBuilder(Z3Context container, Model z3Model)

         {

             this.container = container;

-            this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3);

+            this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3, z3Model);

         }

         

         private Dictionary<string, int> CreateConstantToPartition(Model z3Model)

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 5f776bff..7bdc07a0 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -202,7 +202,6 @@ namespace Microsoft.Boogie.Z3
         private static Z3Config BuildConfig(int timeout, bool nativeBv)

         {

             Z3Config config = new Z3Config();

-            config.SetModelCompletion(false);

             config.SetModel(true);

 

             if (0 <= CommandLineOptions.Clo.ProverCCLimit)

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index a7ed29eb..30207e75 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -315,7 +315,7 @@ namespace Microsoft.Boogie.Z3
 

         private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels)

         {

-            BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this);

+            BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model);

             Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model);

             return new Z3ErrorModelAndLabels(boogieModel, new List<string>(relevantLabels));

         }

diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index 009a6a59..dec25e97 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -65,9 +65,21 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

+        private class CtorTypeComparator : IEqualityComparer<CtorType> {

+          public bool Equals(CtorType x, CtorType y) {

+            return (x.Decl.Name == y.Decl.Name);

+          }

+

+          public int GetHashCode(CtorType ctorType) {

+            return ctorType.Decl.Name.GetHashCode();

+          }

+        }

+

         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 Dictionary<CtorType, Z3Type> ctorTypes = new Dictionary<CtorType, Z3Type>(new CtorTypeComparator());

+

         private Z3Context container;

 

         public Z3TypeCachedBuilder(Z3Context context)

@@ -118,16 +130,29 @@ namespace Microsoft.Boogie.Z3
             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 GetCtorType(CtorType ctorType) {

+          if (!ctorTypes.ContainsKey(ctorType)) {

+            Z3Type typeAst = BuildCtorType(ctorType);

+            ctorTypes.Add(ctorType, typeAst);

+          }

+          Z3Type result;

+          bool containsKey = ctorTypes.TryGetValue(ctorType, out result);

+          Debug.Assert(containsKey);

+          return result;

+        }

+

+        public virtual Z3Type GetType(Type boogieType) {

+          System.Type type = boogieType.GetType();

+          if (type.Equals(typeof(BvType)))

+            return GetBvType((BvType)boogieType);

+          else if (type.Equals(typeof(BasicType)))

+            return GetBasicType((BasicType)boogieType);

+          else if (type.Equals(typeof(MapType)))

+            return GetMapType((MapType)boogieType);

+          else if (type.Equals(typeof(CtorType)))

+            return GetCtorType((CtorType)boogieType);

+          else

+            throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");

         }

 

         private Z3Type WrapType(Sort typeAst)

@@ -165,6 +190,15 @@ namespace Microsoft.Boogie.Z3
                 throw new Exception("Unknown Basic Type " + basicType.ToString());

             return WrapType(typeAst);

         }

+

+        public Z3Type BuildCtorType(CtorType ctorType) {

+          Context z3 = ((Z3SafeContext)container).z3;

+          Sort typeAst;

+          if (ctorType.Arguments.Length > 0)

+            throw new Exception("Type constructor of non-zero arity are not handled");

+          typeAst = z3.MkSort(ctorType.Decl.Name);

+          return WrapType(typeAst);

+        }

     }

 

     public class Z3Type { }