simplified the push-pop business

2 files changed, 21 insertions, 65 deletions

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 6d26edd2..0803098d 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -49,8 +49,9 @@ namespace Microsoft.Boogie.Z3
         public override void Close()

         {

             base.Close();

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

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

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

+            cm.z3.Dispose();

+            cm.config.Config.Dispose();

         }

         private bool z3ContextIsUsed;

 

@@ -71,19 +72,6 @@ namespace Microsoft.Boogie.Z3
             cm.AddConjecture(conjecture, linOptions);

         }

 

-        public void PrepareCheck(string descriptiveName, VCExpr vc)

-        {

-            PushAxiom(context.Axioms);

-            PushConjecture(vc);

-        }

-

-        public void BeginPreparedCheck()

-        {

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

-            outcome = Outcome.Undetermined;

-            outcome = cm.Check(out z3LabelModels);

-        }

-

         public override void PushVCExpression(VCExpr vc)

         {

             PushAxiom(vc);

@@ -94,37 +82,8 @@ namespace Microsoft.Boogie.Z3
         {

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

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

-            if (z3ContextIsUsed)

-            {

-                cm.Backtrack();

-            }

-            else

-            {

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

-                z3ContextIsUsed = true;

-            }

-

-            cm.CreateBacktrackPoint();

             cm.AddConjecture(vc, linOptions);

-

-            BeginPreparedCheck();

-        }

-

-        private Outcome outcome;

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

-

-        [NoDefaultContract]

-        public override Outcome CheckOutcome(ErrorHandler handler)

-        {

-            if (outcome == Outcome.Invalid)

-            {

-                foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)

-                {

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

-                    handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);

-                }

-            }

-            return outcome;

+            outcome = cm.Check(out z3LabelModels);

         }

 

         public void CreateBacktrackPoint()

@@ -152,6 +111,23 @@ namespace Microsoft.Boogie.Z3
             return ret;

         }

 

+        private Outcome outcome;

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

+

+        [NoDefaultContract]

+        public override Outcome CheckOutcome(ErrorHandler handler)

+        {

+            if (outcome == Outcome.Invalid)

+            {

+                foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)

+                {

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

+                    handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);

+                }

+            }

+            return outcome;

+        }

+

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

         {

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

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index c6907639..67cff382 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -266,15 +266,6 @@ namespace Microsoft.Boogie.Z3
                 bound.Add(Unwrap(t));

             }

             Term termAst = z3.MkForall(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody);

-            /*

-            Term termAst = z3.MkQuantifier(true,

-                             weight,

-                             unwrapPatterns.ToArray(),

-                             unwrapNoPatterns.ToArray(),

-                             z3Types.ToArray(),

-                             symbols.ToArray(),

-                             unwrapBody);

-            */

             return Wrap(termAst);

         }

 

@@ -293,15 +284,6 @@ namespace Microsoft.Boogie.Z3
                 bound.Add(Unwrap(t));

             }

             Term termAst = z3.MkExists(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody);

-            /*

-            Term termAst = z3.MkQuantifier(false,

-                                                  weight,

-                                                  unwrapPatterns.ToArray(),

-                                                  unwrapNoPatterns.ToArray(),

-                                                  z3Types.ToArray(),

-                                                  symbols.ToArray(),

-                                                  unwrapBody);

-            */ 

             return Wrap(termAst);

         }

 

@@ -360,7 +342,6 @@ namespace Microsoft.Boogie.Z3
         {

             boogieErrors = new List<Z3ErrorModelAndLabels>();

             LBool outcome = LBool.Undef;

-            z3.Push();

             while (boogieErrors.Count < this.config.Counterexamples)

             {

                 Model z3Model;

@@ -382,7 +363,6 @@ namespace Microsoft.Boogie.Z3
                 else

                     break;

             }

-            z3.Pop();

 

             if (boogieErrors.Count > 0)

                 return ProverInterface.Outcome.Invalid;