further fixes to Z3api project trying to make it work; still a long way off.

9 files changed, 142 insertions, 276 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 51cb7f2f..b572dd6f 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -3,7 +3,7 @@
   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

     <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProductVersion>9.0.30729</ProductVersion>

+    <ProductVersion>9.0.21022</ProductVersion>

     <SchemaVersion>2.0</SchemaVersion>

     <ProjectGuid>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</ProjectGuid>

     <OutputType>Exe</OutputType>

@@ -121,6 +121,10 @@
       <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>

       <Name>SMTLib</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Provers\Z3api\Z3api.csproj">

+      <Project>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</Project>

+      <Name>Z3api</Name>

+    </ProjectReference>

     <ProjectReference Include="..\Provers\Z3\Z3.csproj">

       <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>

       <Name>Z3</Name>

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index bcf55c4c..3813c63b 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -155,7 +155,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     }

   }

 

-  internal class Z3LineariserOptions : LineariserOptions {

+  public class Z3LineariserOptions : LineariserOptions {

     private readonly Z3InstanceOptions opts;

 

     [ContractInvariantMethod]

@@ -169,7 +169,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       return opts.BitVectors;

     } }

  

-    internal Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {

+    public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {

     Contract.Requires(opts != null);

       Contract.Requires(cce.NonNullElements(letVariables));

     

@@ -415,8 +415,7 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
         proverCommands.Add("bvInt");

       VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);

       

-

-      return new DeclFreeProverContext(gen, genOptions);

+      return NewProverContext(gen, genOptions, opts);

     }

 

     public override ProverOptions BlankProverOptions()

@@ -426,8 +425,8 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
     }

 

     protected virtual Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,

-                                                          DeclFreeProverContext ctx,

-                                                          Z3InstanceOptions opts) {

+                                                         DeclFreeProverContext ctx,

+                                                         Z3InstanceOptions opts) {

       Contract.Requires(gen != null);

       Contract.Requires(ctx != null);

       Contract.Requires(opts != null);

@@ -435,5 +434,12 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
 

       return new Z3ProcessTheoremProver(gen, ctx, opts);

     }

+

+      protected virtual DeclFreeProverContext NewProverContext(VCExpressionGenerator gen, 

+                                                               VCGenerationOptions genOptions,

+                                                               Z3InstanceOptions opts)

+      {

+          return new DeclFreeProverContext(gen, genOptions);

+      }

   }

 }

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 532b1932..e3ba1fa7 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -15,30 +15,20 @@ namespace Microsoft.Boogie.Z3
 {

     public class Z3Config

     {

+        ~Z3Config()

+        {

+            config.Dispose();

+        }

         private Config config = new Config();

         private int counterexamples;

         private string logFilename;

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

 

-        public void SetPartialModels(bool enabled)

-        {

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

-        }

         public void SetModelCompletion(bool enabled)

         {

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

         }

 

-        public void SetHideUnusedPartitions(bool enabled)

-        {

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

-        }

-

-        public void SetMAM(string mamNumber)

-        {

-            config.SetParamValue("MAM", mamNumber);

-        }

-

         public void SetModel(bool enabled)

         {

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

@@ -54,11 +44,6 @@ namespace Microsoft.Boogie.Z3
             config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false"));

         }

 

-        public void SetReflectBvOps(bool enabled)

-        {

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

-        }

-

         public void SetCounterExample(int counterexample)

         {

             this.counterexamples = counterexample;

@@ -93,16 +78,6 @@ namespace Microsoft.Boogie.Z3
         }

     }

 

-    public abstract class Z3ContextFactory

-    {

-

-        public static Z3Context BuildZ3Context(Z3Config config, VCExpressionGenerator gen)

-        {

-            return new Z3SafeContext(config, gen);

-        }

-    }

-

-

     public abstract class Z3TermAst { }

     public abstract class Z3PatternAst { }

     public abstract class Z3ConstDeclAst { }

@@ -112,8 +87,8 @@ namespace Microsoft.Boogie.Z3
     {

         void CreateBacktrackPoint();

         void Backtrack();

-        void AddAxiom(VCExpr vc);

-        void AddConjecture(VCExpr vc);

+        void AddAxiom(VCExpr vc, LineariserOptions linOptions);

+        void AddConjecture(VCExpr vc, LineariserOptions linOptions);

         void AddSmtlibString(string smtlibString);

         string GetDeclName(Z3ConstDeclAst constDeclAst);

         Z3PatternAst MakePattern(List<Z3TermAst> exprs);

@@ -142,7 +117,7 @@ namespace Microsoft.Boogie.Z3
         private int partitionCounter = FAKE_PARTITION;

         public int GetPartition(int valueHash)

         {

-            if (partitionToValueHash.ContainsKey(valueHash))

+            if (!partitionToValueHash.ContainsKey(valueHash))

             {

                 partitionCounter++;

                 partitionToValueHash.Add(valueHash, partitionCounter);

@@ -234,7 +209,7 @@ namespace Microsoft.Boogie.Z3
                 string c_name = container.GetDeclName(new Z3TypeSafeConstDecl(c));

                 Term v = z3Model.Eval(c, new Term[0]);

                 Sort s = v.GetSort();

-                Context ctx = new Context(null); // placeholder.

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

                 Sort boolSort = ctx.MkBoolSort();

                 Sort intSort = ctx.MkIntSort();

 

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 02362edf..f3dfab69 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -20,84 +20,31 @@ using PatternAst = System.IntPtr;
 

 namespace Microsoft.Boogie.Z3

 {

-    public class Z3ThreadTheoremProver : ProverInterface

+    public class Z3apiProcessTheoremProver : Z3ProcessTheoremProver

     {

-        protected DeclFreeProverContext ctx;

-        protected VCExpressionGenerator gen;

-        public override ProverContext Context

+        public Z3apiProcessTheoremProver(VCExpressionGenerator gen,

+                                         DeclFreeProverContext ctx,

+                                         Z3InstanceOptions opts)

+            : base(gen, ctx, opts)

         {

-            get { return this.ctx; }

-        }

-        public override VCExpressionGenerator VCExprGen

-        {

-            get { return this.gen; }

-        }

-

-        private int timeout;

-        private Z3Context cm;

-

-        public Z3ThreadTheoremProver(Z3InstanceOptions proverOptions)

-            : base()

-        {

-            gen = new VCExpressionGenerator();

-

-            string codebaseString = Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);

-            string backgroundPredicates;

-

-            // Initialize '_backgroundPredicates'

-            string univBackPredPath = Path.Combine(codebaseString,

-                // yes, using .NeedsTypes here is an ugly hack...

-                "Z3API_UnivBackPred.smt");

-            using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))

-            {

-                backgroundPredicates = reader.ReadToEnd();

-            }

-

-            Z3Config config = BuildConfig(timeout, true);

-            Z3Context cm = Z3ContextFactory.BuildZ3Context(config, gen);

-            Z3ThreadProverContext ctx = new Z3ThreadProverContext(gen, cm);

-

-            this.cm = cm;

-            cm.AddSmtlibString(backgroundPredicates);

             this.z3ContextIsUsed = false;

         }

 

-        private static Z3Config BuildConfig(int timeout, bool nativeBv)

-        {

-            Z3Config config = new Z3Config();

-            config.SetPartialModels(true);

-            config.SetModelCompletion(false);

-            config.SetHideUnusedPartitions(false);

-            config.SetModel(true);

-

-            if (0 <= CommandLineOptions.Clo.ProverCCLimit)

-            {

-                config.SetCounterExample(CommandLineOptions.Clo.ProverCCLimit);

-            }

-

-            if (0 <= timeout)

-            {

-                config.SetSoftTimeout(timeout.ToString());

-            }

-

-            config.SetTypeCheck(true);

-            if (nativeBv)

-                config.SetReflectBvOps(true);

-

-            return config;

-        }

-

         private bool z3ContextIsUsed;

 

         public void PushAxiom(VCExpr axiom)

         {

+            Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

             cm.CreateBacktrackPoint();

-            cm.AddAxiom((VCExpr)axiom);

+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

+            cm.AddAxiom((VCExpr)axiom, linOptions);

         }

         private void PushConjecture(VCExpr conjecture)

         {

+            Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

             cm.CreateBacktrackPoint();

-            cm.AddConjecture((VCExpr)conjecture);

+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

+            cm.AddConjecture((VCExpr)conjecture, linOptions);

         }

 

         public void PrepareCheck(string descriptiveName, VCExpr vc)

@@ -108,31 +55,33 @@ namespace Microsoft.Boogie.Z3
 

         public void BeginPreparedCheck()

         {

+            Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

             outcome = Outcome.Undetermined;

             outcome = cm.Check(out z3LabelModels);

         }

 

         public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)

         {

+            LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

+            Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

             if (z3ContextIsUsed)

             {

                 cm.Backtrack();

             }

             else

             {

-                cm.AddAxiom((VCExpr)ctx.Axioms);

+                cm.AddAxiom((VCExpr)ctx.Axioms, linOptions);

                 z3ContextIsUsed = true;

             }

 

             cm.CreateBacktrackPoint();

-            cm.AddConjecture((VCExpr)vc);

+            cm.AddConjecture((VCExpr)vc, linOptions);

 

             BeginPreparedCheck();

         }

 

         private Outcome outcome;

         private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>();

-        private UnexpectedProverOutputException proverException = null;

 

         [NoDefaultContract]

         public override Outcome CheckOutcome(ErrorHandler handler)

@@ -141,7 +90,7 @@ namespace Microsoft.Boogie.Z3
             {

                 foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)

                 {

-                    List<string> unprefixedLabels = RemovePreffixes(z3LabelModel.RelevantLabels);

+                    List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);

                     handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);

                 }

             }

@@ -150,14 +99,16 @@ namespace Microsoft.Boogie.Z3
 

         public void CreateBacktrackPoint()

         {

+            Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

             cm.CreateBacktrackPoint();

         }

         override public void Pop()

         {

+            Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;

             cm.Backtrack();

         }

 

-        private List<string> RemovePreffixes(List<string> labels)

+        private List<string> RemovePrefixes(List<string> labels)

         {

             List<string> result = new List<string>();

             foreach (string label in labels)

@@ -175,22 +126,42 @@ namespace Microsoft.Boogie.Z3
                     result.Add(label.Substring(1));

                 }

                 else

-                    throw new Exception("Unknown preffix in label " + label);

+                    throw new Exception("Unknown prefix in label " + label);

             }

             return result;

         }

-

     }

 

-    public class Z3ThreadProverContext : DeclFreeProverContext

+    public class Z3apiProverContext : DeclFreeProverContext

     {

+        public Z3SafeContext cm;

+        

+        public Z3apiProverContext(VCExpressionGenerator gen, 

+                                  VCGenerationOptions genOptions, 

+                                  Z3InstanceOptions opts)

+            : base(gen, genOptions)

+        {

+            Z3Config config = BuildConfig(opts.Timeout, true);

+            this.cm = new Z3SafeContext(config, gen);

+        }

+        private static Z3Config BuildConfig(int timeout, bool nativeBv)

+        {

+            Z3Config config = new Z3Config();

+            config.SetModelCompletion(false);

+            config.SetModel(true);

 

-        private Z3Context cm;

+            if (0 <= CommandLineOptions.Clo.ProverCCLimit)

+            {

+                config.SetCounterExample(CommandLineOptions.Clo.ProverCCLimit);

+            }

 

-        public Z3ThreadProverContext(VCExpressionGenerator gen, Z3Context cm)

-            : base(gen, null)

-        {

-            this.cm = cm;

+            if (0 <= timeout)

+            {

+                config.SetSoftTimeout(timeout.ToString());

+            }

+

+            config.SetTypeCheck(true);

+            return config;

         }

 

         public override void DeclareType(TypeCtorDecl t, string attributes)

@@ -205,7 +176,6 @@ namespace Microsoft.Boogie.Z3
             cm.DeclareConstant(c.Name, c.TypedIdent.Type);

         }

 

-

         public override void DeclareFunction(Function f, string attributes)

         {

             base.DeclareFunction(f, attributes);

@@ -231,23 +201,20 @@ namespace Microsoft.Boogie.Z3
 

 namespace Microsoft.Boogie.Z3api

 {

-

-    public class Factory : ProverFactory

+    public class Factory : Microsoft.Boogie.Z3.Factory

     {

-        public override object SpawnProver(ProverOptions popts, object ctxt)

+        protected override Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,

+                                                              DeclFreeProverContext ctx,

+                                                              Z3InstanceOptions opts)

         {

-            Z3InstanceOptions options = (Z3InstanceOptions) popts;

-            if (CommandLineOptions.Clo.BracketIdsInVC < 0)

-            {

-                CommandLineOptions.Clo.BracketIdsInVC = 0;

-            }

-

-            return new Z3ThreadTheoremProver(options);

+            return new Z3apiProcessTheoremProver(gen, ctx, opts);

         }

 

-        public override object NewProverContext(ProverOptions options)

+        protected override DeclFreeProverContext NewProverContext(VCExpressionGenerator gen,

+                                                                  VCGenerationOptions genOptions,

+                                                                  Z3InstanceOptions opts)

         {

-            throw new NotImplementedException();

+            return new Z3apiProverContext(gen, genOptions, opts);

         }

     }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 26e7385d..70b7f35c 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -81,13 +81,16 @@ namespace Microsoft.Boogie.Z3
 

     public class Z3SafeContext : Z3Context

     {

-

         private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();

         internal BacktrackDictionary<string, Z3TypeSafeTerm> constants = new BacktrackDictionary<string, Z3TypeSafeTerm>();

         internal BacktrackDictionary<string, Z3TypeSafeConstDecl> functions = new BacktrackDictionary<string, Z3TypeSafeConstDecl>();

         internal BacktrackDictionary<string, Z3TypeSafeTerm> labels = new BacktrackDictionary<string, Z3TypeSafeTerm>();

 

-        private Context z3;

+        ~Z3SafeContext()

+        {

+            z3.Dispose();

+        }

+        public Context z3;

         private Z3Config config;

 

         public void CreateBacktrackPoint()

@@ -108,19 +111,19 @@ namespace Microsoft.Boogie.Z3
             symbols.Backtrack();

         }

 

-        public void AddAxiom(VCExpr vc)

+        public void AddAxiom(VCExpr vc, LineariserOptions linOptions)

         {

             Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);

-            Z3TermAst z3ast = (Z3TermAst)vc.Accept(visitor, null);

+            Z3TermAst z3ast = (Z3TermAst)vc.Accept(visitor, linOptions);

             Term term = Unwrap(z3ast);

             z3.AssertCnstr(term);

         }

 

-        public void AddConjecture(VCExpr vc)

+        public void AddConjecture(VCExpr vc, LineariserOptions linOptions)

         {

             VCExpr not_vc = (VCExpr)this.gen.Not(vc);

             Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);

-            Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, null);

+            Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions);

             Term term = Unwrap(z3ast);

             z3.AssertCnstr(term);

         }

@@ -281,7 +284,7 @@ namespace Microsoft.Boogie.Z3
                 return false;

 

             for (int i = 0; i < l.Count; i++)

-                if (l[i].Equals(r[i]))

+                if (!l[i].Equals(r[i]))

                     return false;

             return true;

         }

@@ -295,7 +298,7 @@ namespace Microsoft.Boogie.Z3
             {

                 Symbol sym = relevantLabels.GetLabel(i);

                 string labelName = z3.GetSymbolString(sym);

-                if (labelName.StartsWith("@"))

+                if (!labelName.StartsWith("@"))

                 {

                     relevantLabels.Disable(i);

                 }

@@ -322,7 +325,6 @@ namespace Microsoft.Boogie.Z3
             System.Console.WriteLine("---");

         }

 

-

         public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors)

         {

             boogieErrors = new List<Z3ErrorModelAndLabels>();

@@ -380,7 +382,7 @@ namespace Microsoft.Boogie.Z3
 

         private VCExpressionGenerator gen;

 

-        internal Z3SafeContext(Z3Config config, VCExpressionGenerator gen)

+        public Z3SafeContext(Z3Config config, VCExpressionGenerator gen)

         {

             Context z3 = new Context(config.Config);

             // TBD: z3.EnableArithmetic();

@@ -390,7 +392,7 @@ namespace Microsoft.Boogie.Z3
                 z3.EnableDebugTrace(tag);

             this.z3 = z3;

             this.config = config;

-            this.tm = new Z3TransformerTypeCache(new Z3SafeTypeBuilder(z3), new IntTransformer());

+            this.tm = new Z3TypeCachedBuilder(new Z3SafeTypeBuilder(z3));

             this.gen = gen;

         }

 

@@ -448,13 +450,13 @@ namespace Microsoft.Boogie.Z3
 

         private Symbol GetSymbol(string symbolName)

         {

-            if (symbols.ContainsKey(symbolName))

+            if (!symbols.ContainsKey(symbolName))

             {

                 Symbol symbolAst = z3.MkSymbol(symbolName);

                 symbols.Add(symbolName, symbolAst);

             }

             Symbol result;

-            if (symbols.TryGetValue(symbolName, out result))

+            if (!symbols.TryGetValue(symbolName, out result))

                 throw new Exception("symbol " + symbolName + " is undefined");

             return result;

         }

@@ -462,10 +464,10 @@ namespace Microsoft.Boogie.Z3
         public Z3TermAst GetConstant(string constantName, Type constantType)

         {

             Z3TypeSafeTerm typeSafeTerm;

-            if (constants.ContainsKey(constantName))

+            if (!constants.ContainsKey(constantName))

                 this.DeclareConstant(constantName, constantType);

 

-            if (constants.TryGetValue(constantName, out typeSafeTerm))

+            if (!constants.TryGetValue(constantName, out typeSafeTerm))

                 throw new Exception("constant " + constantName + " is not defined");

             return typeSafeTerm;

         }

@@ -548,7 +550,7 @@ namespace Microsoft.Boogie.Z3
         private FuncDecl GetFunction(string functionName)

         {

             Z3TypeSafeConstDecl function;

-            if (functions.TryGetValue(functionName, out function))

+            if (!functions.TryGetValue(functionName, out function))

                 throw new Exception("function " + functionName + " is undefined");

             FuncDecl unwrapFunction = Unwrap(function);

             return unwrapFunction;

@@ -557,7 +559,6 @@ namespace Microsoft.Boogie.Z3
 

     public class Z3SafeTypeBuilder : Z3TypeBuilder

     {

-

         protected Context z3;

 

         public Z3SafeTypeBuilder(Context z3)

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index 80f1776e..e4dd9318 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -19,8 +19,8 @@ namespace Microsoft.Boogie.Z3 {
   

     public void CreateBacktrackPoint(){}

     public void Backtrack(){}

-    public void AddAxiom(VCExpr vc) {}

-    public void AddConjecture(VCExpr vc){}

+    public void AddAxiom(VCExpr vc, LineariserOptions linOptions) {}

+    public void AddConjecture(VCExpr vc, LineariserOptions linOptions){}

     public void AddSmtlibString(string smtlibString) {}

     public string GetDeclName(Z3ConstDeclAst constDeclAst) {

       return "";

diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index 553205b1..280e93e9 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -57,7 +57,7 @@ namespace Microsoft.Boogie.Z3
 

         private Z3Type GetBvType(BvType bvType)

         {

-            if (bvTypes.ContainsKey(bvType))

+            if (!bvTypes.ContainsKey(bvType))

             {

                 Z3Type typeAst = builder.BuildBvType(bvType);

                 bvTypes.Add(bvType, typeAst);

@@ -70,7 +70,7 @@ namespace Microsoft.Boogie.Z3
 

         private Z3Type GetBasicType(BasicType basicType)

         {

-            if (basicTypes.ContainsKey(basicType))

+            if (!basicTypes.ContainsKey(basicType))

             {

                 Z3Type typeAst = builder.BuildBasicType(basicType);

                 basicTypes.Add(basicType, typeAst);

@@ -99,65 +99,4 @@ namespace Microsoft.Boogie.Z3
         Z3Type BuildBvType(BvType bvType);

         Z3Type BuildBasicType(BasicType basicType);

     }

-

-

-    internal class Z3TransformerTypeCache : Z3TypeCachedBuilder

-    {

-

-        private BoogieTypeTransformer transformer;

-

-        public Z3TransformerTypeCache(Z3TypeBuilder builder, BoogieTypeTransformer transformer)

-            : base(builder)

-        {

-            this.transformer = transformer;

-        }

-

-        public override Z3Type GetType(Type boogieType)

-        {

-            Type resolvedBoogieType = transformer.TransformType(boogieType);

-            return base.GetType(resolvedBoogieType);

-        }

-    }

-

-    internal abstract class BoogieTypeTransformer

-    {

-

-        protected abstract Type TransformBvType(BvType boogieType);

-        protected abstract Type TransformBasicType(BasicType boogieType);

-

-        public Type TransformType(Type boogieType)

-        {

-            return Dispatch(boogieType);

-        }

-

-        private Type Dispatch(Type boogieType)

-        {

-            if (boogieType.GetType().Equals(typeof(BvType)))

-                return TransformBvType((BvType)boogieType);

-            else if (boogieType.GetType().Equals(typeof(BasicType)))

-                return TransformBasicType((BasicType)boogieType);

-            else

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

-        }

-

-    }

-

-    internal class IntTransformer : BoogieTypeTransformer

-    {

-

-        protected override Type TransformBvType(BvType bvType)

-        {

-            // registerBvType(bvType.Bits)

-            return BasicType.Int;

-        }

-

-        protected override Type TransformBasicType(BasicType boogieType)

-        {

-            if (boogieType.IsBool)

-            {

-                // registerBool()

-            }

-            return BasicType.Int;

-        }

-    }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index ca32a824..25b674a7 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -14,7 +14,6 @@ using Microsoft.Boogie.VCExprAST;
 

 namespace Microsoft.Boogie.Z3

 {

-    // Lineariser for expressions. The result (bool) is currently not used for anything

     public class Z3apiExprLineariser : IVCExprVisitor<Z3TermAst, LineariserOptions>

     {

         private Z3apiOpLineariser OpLinObject = null;

@@ -30,18 +29,12 @@ namespace Microsoft.Boogie.Z3
         }

 

         internal readonly UniqueNamer Namer;

-        private readonly TextWriter wr;

-

         protected Z3Context cm;

 

-        protected Stack<Dictionary<string, VCExpr>> lets;

-        protected Stack<List<string>> binders;

-

         public Z3apiExprLineariser(Z3Context cm)

         {

             this.cm = cm;

-            Stack<Dictionary<string, VCExpr>> lets = new Stack<Dictionary<string, VCExpr>>();

-            Stack<List<string>> binders = new Stack<List<string>>();

+            this.Namer = new UniqueNamer();

         }

 

         public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)

@@ -53,39 +46,6 @@ namespace Microsoft.Boogie.Z3
 

         /////////////////////////////////////////////////////////////////////////////////////

 

-        private bool DeBruijnIndex(string variableName, out int deBruijnIndex)

-        {

-            deBruijnIndex = -1;

-            foreach (List<string> binder in binders)

-            {

-                for (int i = binder.Count - 1; i >= 0; i--)

-                {

-                    deBruijnIndex++;

-                    if (binder[i].Equals(variableName))

-                        return true;

-                }

-            }

-            deBruijnIndex = -1;

-            return false;

-        }

-

-        protected Z3TermAst FindDefinition(string variableName, Type variableType)

-        {

-            Z3TermAst termAst;

-            int deBruijnIndex;

-            if (DeBruijnIndex(variableName, out deBruijnIndex))

-            {

-                return cm.MakeBoundVariable((uint)deBruijnIndex, variableType);

-            }

-            else

-            {

-                termAst = cm.GetConstant(variableName, variableType);

-                return termAst;

-            }

-        }

-

-        /////////////////////////////////////////////////////////////////////////////////////

-

         public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options)

         {

             Contract.Requires(options != null);

@@ -142,8 +102,8 @@ namespace Microsoft.Boogie.Z3
         {

             Contract.Requires(options != null);

             Contract.Requires(node != null);

-

-            return FindDefinition(node.Name, node.Type);

+            string varName = Namer.GetName(node, node.Name);

+            return cm.GetConstant(varName, node.Type);

         }

 

         /////////////////////////////////////////////////////////////////////////////////////

@@ -154,7 +114,7 @@ namespace Microsoft.Boogie.Z3
             Contract.Requires(node != null);

             Contract.Assert(node.TypeParameters.Count == 0);

 

-            binders.Push(new List<string>());

+            Namer.PushScope();

             try

             {

                 List<string> varNames;

@@ -211,7 +171,7 @@ namespace Microsoft.Boogie.Z3
             }

             finally

             {

-                binders.Pop();

+                Namer.PopScope();

             }

         }

         

@@ -221,9 +181,9 @@ namespace Microsoft.Boogie.Z3
             varTypes = new List<Type>();

             foreach (VCExprVar var in boundVars)

             {

-                varNames.Add(var.Name);

+                string varName = Namer.GetLocalName(var, var.Name);

+                varNames.Add(varName);

                 varTypes.Add(var.Type);

-                binders.Peek().Add(var.Name);

             }

         }

 

@@ -260,24 +220,32 @@ namespace Microsoft.Boogie.Z3
 

         public Z3TermAst Visit(VCExprLet node, LineariserOptions options)

         {

+            Namer.PushScope();

             try

             {

-                Dictionary<string, VCExpr> let = new Dictionary<string, VCExpr>();

-                lets.Push(let);

+                List<Z3TermAst> equations = new List<Z3TermAst>();

                 foreach (VCExprLetBinding b in node)

                 {

-                    let.Add(b.V.Name, b.E);

+                    string varName = Namer.GetLocalName(b.V, b.V.Name);

+                    Z3TermAst varAst = cm.GetConstant(varName, b.V.Type);

+                    Z3TermAst defAst = Linearise(b.E, options);

+                    List<Z3TermAst> args = new List<Z3TermAst>();

+                    args.Add(varAst);

+                    args.Add(defAst);

+                    equations.Add(cm.Make("EQ", args));

                 }

-                Z3TermAst letAST = Linearise(node.Body, options);

-                return letAST;

+                System.Diagnostics.Debug.Assert(equations.Count > 0);

+                Z3TermAst eqAst = cm.Make("AND", equations);

+                List<Z3TermAst> t = new List<Z3TermAst>();

+                t.Add(eqAst);

+                t.Add(Linearise(node.Body, options));

+                return cm.Make("IMPLIES", t);

             }

             finally

             {

-                lets.Pop();

+                Namer.PopScope();

             }

-        }

-

-  

+        }  

 

         /////////////////////////////////////////////////////////////////////////////////////

 

@@ -546,28 +514,28 @@ namespace Microsoft.Boogie.Z3
             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("intLess", node, options);  // arguments are always terms

+                return WriteApplication("<", node, options);  // arguments are always terms

             }

 

             public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("intAtMost", node, options);  // arguments are always terms

+                return WriteApplication("<=", node, options);  // arguments are always terms

             }

 

             public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("intGreater", node, options);  // arguments are always terms

+                return WriteApplication(">", node, options);  // arguments are always terms

             }

 

             public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)

             {

                 Contract.Requires(options != null);

                 Contract.Requires(node != null);

-                return WriteApplication("intAtLeast", node, options);  // arguments are always terms

+                return WriteApplication(">=", node, options);  // arguments are always terms

             }

 

             public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 15dfa133..fb01ce94 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -3,13 +3,13 @@
   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

     <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

-    <ProductVersion>9.0.30729</ProductVersion>

+    <ProductVersion>9.0.21022</ProductVersion>

     <SchemaVersion>2.0</SchemaVersion>

     <ProjectGuid>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid>

     <OutputType>Library</OutputType>

     <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>Z3api</RootNamespace>

-    <AssemblyName>Z3api</AssemblyName>

+    <RootNamespace>Microsoft.Boogie.Z3api</RootNamespace>

+    <AssemblyName>Provers.Z3api</AssemblyName>

     <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <StartupObject>

@@ -81,6 +81,10 @@
       <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Simplify\Simplify.csproj">

+      <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>

+      <Name>Simplify</Name>

+    </ProjectReference>

     <ProjectReference Include="..\Z3\Z3.csproj">

       <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>

       <Name>Z3</Name>

@@ -91,7 +95,9 @@
     <Compile Include="ProverLayer.cs" />

     <Compile Include="SafeContext.cs" />

     <Compile Include="StubContext.cs" />

-    <Compile Include="TypeAdapter.cs" />

+    <Compile Include="TypeAdapter.cs">

+      <SubType>Code</SubType>

+    </Compile>

     <Compile Include="VCExprVisitor.cs" />

   </ItemGroup>

 </Project>
\ No newline at end of file