bug fixes in z3api

5 files changed, 88 insertions, 56 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 64533c02..631597b2 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -83,7 +83,7 @@ namespace Microsoft.Boogie.Z3
     {

         void CreateBacktrackPoint();

         void Backtrack();

-        void AddAxiom(VCExpr vc, LineariserOptions linOptions);

+        void AddAxiom(VCExpr axiom, LineariserOptions linOptions);

         void AddConjecture(VCExpr vc, LineariserOptions linOptions);

         void AddSmtlibString(string smtlibString);

         string GetDeclName(Z3ConstDeclAst constDeclAst);

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 7c41f25c..8d0c8aeb 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -10,6 +10,7 @@ using Microsoft.Boogie;
 using Microsoft.Boogie.Z3;

 using Microsoft.Z3;

 using Microsoft.Boogie.VCExprAST;

+using Microsoft.Boogie.Simplify;

 

 using TypeAst = System.IntPtr;

 using TermAst = System.IntPtr;

@@ -20,49 +21,62 @@ using PatternAst = System.IntPtr;
 

 namespace Microsoft.Boogie.Z3

 {

-    public class Z3apiProcessTheoremProver : Z3ProcessTheoremProver

+    public class Z3apiProcessTheoremProver : ProverInterface

     {

-        public Z3apiProcessTheoremProver(VCExpressionGenerator gen,

-                                         DeclFreeProverContext ctx,

-                                         Z3InstanceOptions opts)

-            : base(gen, ctx, opts)

+        public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)

         {

+            this.options = opts;

+            this.context = (Z3apiProverContext) ctxt;

             this.z3ContextIsUsed = false;

         }

 

+        private Z3InstanceOptions options;

+

+        private Z3apiProverContext context;

+        public override ProverContext Context

+        {

+            get { return context; }

+        }

+

+        public override VCExpressionGenerator VCExprGen

+        {

+            get { return context.ExprGen; }

+        }

+

         public override void Close()

         {

             base.Close();

-            ((Z3apiProverContext)Context).cm.z3.Dispose();

-            ((Z3apiProverContext)Context).cm.config.Config.Dispose();

+            ((Z3apiProverContext)context).cm.z3.Dispose();

+            ((Z3apiProverContext)context).cm.config.Config.Dispose();

         }

         private bool z3ContextIsUsed;

 

         public void PushAxiom(VCExpr axiom)

         {

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

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

             cm.CreateBacktrackPoint();

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

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

+            cm.AddAxiom(axiom, linOptions);

+            

         }

 

         private void PushConjecture(VCExpr conjecture)

         {

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

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

             cm.CreateBacktrackPoint();

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

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

+            cm.AddConjecture(conjecture, linOptions);

         }

 

         public void PrepareCheck(string descriptiveName, VCExpr vc)

         {

-            PushAxiom(ctx.Axioms);

+            PushAxiom(context.Axioms);

             PushConjecture(vc);

         }

 

         public void BeginPreparedCheck()

         {

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

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

             outcome = Outcome.Undetermined;

             outcome = cm.Check(out z3LabelModels);

         }

@@ -75,19 +89,19 @@ namespace Microsoft.Boogie.Z3
         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;

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

             if (z3ContextIsUsed)

             {

                 cm.Backtrack();

             }

             else

             {

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

+                cm.AddAxiom(context.Axioms, linOptions);

                 z3ContextIsUsed = true;

             }

 

             cm.CreateBacktrackPoint();

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

+            cm.AddConjecture(vc, linOptions);

 

             BeginPreparedCheck();

         }

@@ -111,12 +125,13 @@ namespace Microsoft.Boogie.Z3
 

         public void CreateBacktrackPoint()

         {

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

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

             cm.CreateBacktrackPoint();

         }

+

         override public void Pop()

         {

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

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

             cm.Backtrack();

         }

 

@@ -148,13 +163,11 @@ namespace Microsoft.Boogie.Z3
     {

         public Z3SafeContext cm;

         

-        public Z3apiProverContext(VCExpressionGenerator gen, 

-                                  VCGenerationOptions genOptions, 

-                                  Z3InstanceOptions opts)

-            : base(gen, genOptions)

+        public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)

+            : base(gen, new VCGenerationOptions(new List<string>()))

         {

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

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

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

         }

         private static Z3Config BuildConfig(int timeout, bool nativeBv)

         {

@@ -208,25 +221,37 @@ namespace Microsoft.Boogie.Z3
             base.DeclareGlobalVariable(v, attributes);

             cm.DeclareConstant(v.Name, v.TypedIdent.Type);

         }

+

+        public override string Lookup(VCExprVar var)

+        {

+            return cm.Namer.Lookup(var);

+        }

     }

 }

 

 namespace Microsoft.Boogie.Z3api

 {

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

+    public class Factory : ProverFactory

     {

-        protected override Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,

-                                                              DeclFreeProverContext ctx,

-                                                              Z3InstanceOptions opts)

+        public override object SpawnProver(ProverOptions options, object ctxt)

+        {

+            return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt);

+        }

+

+        public override object NewProverContext(ProverOptions opts)

         {

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

+            if (CommandLineOptions.Clo.BracketIdsInVC < 0)

+            {

+                CommandLineOptions.Clo.BracketIdsInVC = 0;

+            }

+

+            VCExpressionGenerator gen = new VCExpressionGenerator();

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

         }

 

-        protected override DeclFreeProverContext NewProverContext(VCExpressionGenerator gen,

-                                                                  VCGenerationOptions genOptions,

-                                                                  Z3InstanceOptions opts)

+        public override ProverOptions BlankProverOptions()

         {

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

+            return new Z3InstanceOptions();

         }

     }

 }
\ No newline at end of file
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 9ce303f4..c6907639 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -87,8 +87,29 @@ namespace Microsoft.Boogie.Z3
 

         public Context z3;

         public Z3Config config;

+        public Z3apiProverContext ctxt;

         private VCExpressionGenerator gen;

         private Z3TypeCachedBuilder tm;

+        private UniqueNamer namer;

+        public UniqueNamer Namer

+        {

+            get { return namer; }

+        }

+

+        public Z3SafeContext(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen)

+        {

+            Context z3 = new Context(config.Config);

+            if (config.LogFilename != null)

+                z3.OpenLog(config.LogFilename);

+            foreach (string tag in config.DebugTraces)

+                z3.EnableDebugTrace(tag);

+            this.ctxt = ctxt;

+            this.z3 = z3;

+            this.config = config;

+            this.tm = new Z3TypeCachedBuilder(this);

+            this.gen = gen;

+            this.namer = new UniqueNamer();

+        }

 

         public void CreateBacktrackPoint()

         {

@@ -108,10 +129,10 @@ namespace Microsoft.Boogie.Z3
             symbols.Backtrack();

         }

 

-        public void AddAxiom(VCExpr vc, LineariserOptions linOptions)

+        public void AddAxiom(VCExpr axiom, LineariserOptions linOptions)

         {

-            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);

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

+            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

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

             Term term = Unwrap(z3ast);

             z3.AssertCnstr(term);

         }

@@ -119,7 +140,7 @@ namespace Microsoft.Boogie.Z3
         public void AddConjecture(VCExpr vc, LineariserOptions linOptions)

         {

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

-            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);

+            Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);

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

             Term term = Unwrap(z3ast);

             z3.AssertCnstr(term);

@@ -346,7 +367,7 @@ namespace Microsoft.Boogie.Z3
                 //System.Console.WriteLine("Check Begin");

                 outcome = z3.CheckAndGetModel(out z3Model);

                 //System.Console.WriteLine("Check End");

-                if (outcome == LBool.True)

+                if (outcome != LBool.False)

                 {

                     Debug.Assert(z3Model != null);

 

@@ -390,20 +411,6 @@ namespace Microsoft.Boogie.Z3
                 throw new Exception("Failed Int Typecheck");

         }

 

-        public Z3SafeContext(Z3Config config, VCExpressionGenerator gen)

-        {

-            Context z3 = new Context(config.Config);

-            // TBD: z3.EnableArithmetic();

-            if (config.LogFilename != null)

-                z3.OpenLog(config.LogFilename);

-            foreach (string tag in config.DebugTraces)

-                z3.EnableDebugTrace(tag);

-            this.z3 = z3;

-            this.config = config;

-            this.tm = new Z3TypeCachedBuilder(this);

-            this.gen = gen;

-        }

-

         public void DeclareType(string typeName)

         {

         }

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index 0284d219..ade8cad0 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -12,14 +12,14 @@ using Microsoft.Z3;
 using Microsoft.Boogie.VCExprAST;

 

 namespace Microsoft.Boogie.Z3 {

-  public class Z3StubContext:Z3Context {

+  public class Z3StubContext : Z3Context {

     class Z3StubPatternAst: Z3PatternAst {}

     class Z3StubTermAst: Z3TermAst {}

     class Z3StubLabeledLiterals: Z3LabeledLiterals {}

   

     public void CreateBacktrackPoint(){}

     public void Backtrack(){}

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

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

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

     public void AddSmtlibString(string smtlibString) {}

     public string GetDeclName(Z3ConstDeclAst constDeclAst) {

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index b2a84c8f..35bdb61a 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -32,10 +32,10 @@ namespace Microsoft.Boogie.Z3
         internal readonly Dictionary<VCExprVar, Z3TermAst> letBindings;

         protected Z3Context cm;

 

-        public Z3apiExprLineariser(Z3Context cm)

+        public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer)

         {

             this.cm = cm;

-            this.namer = new UniqueNamer();

+            this.namer = namer;

             this.letBindings = new Dictionary<VCExprVar, Z3TermAst>();

         }