BeginCheck now adds context.Axioms as well as the conjecture to the context.

Also started using the new quantifier api.

6 files changed, 16 insertions, 45 deletions

diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 631597b2..759c6920 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -88,8 +88,7 @@ namespace Microsoft.Boogie.Z3
         void AddSmtlibString(string smtlibString);

         string GetDeclName(Z3ConstDeclAst constDeclAst);

         Z3PatternAst MakePattern(List<Z3TermAst> exprs);

-        Z3TermAst MakeForall(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);

-        Z3TermAst MakeExists(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);

+        Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);

         List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels);

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

         void TypeCheckBool(Z3TermAst t);

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 9348e413..940f4ce6 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -27,7 +27,6 @@ namespace Microsoft.Boogie.Z3
         {

             this.options = opts;

             this.context = (Z3apiProverContext) ctxt;

-            this.z3ContextIsUsed = false;

             this.numAxiomsPushed = 0;

         }

 

@@ -54,7 +53,6 @@ namespace Microsoft.Boogie.Z3
             cm.config.Config.Dispose();

             cm.CloseLog();

         }

-        private bool z3ContextIsUsed;

 

         public void PushAxiom(VCExpr axiom)

         {

@@ -90,6 +88,7 @@ namespace Microsoft.Boogie.Z3
             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

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

             Push();

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

             cm.AddConjecture(vc, linOptions);

             outcome = cm.Check(out z3LabelModels);

             Pop();

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 7305f29a..bb09be58 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -288,12 +288,10 @@ namespace Microsoft.Boogie.Z3
             return z3Types;

         }

 

-        public Z3TermAst MakeForall(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body)

+        public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body)

         {

             List<Pattern> unwrapPatterns = Unwrap(patterns);

-            // List<Term> unwrapNoPatterns = Unwrap(no_patterns);

-            // List<Sort> z3Types = GetTypes(boogieTypes);

-            // List<Symbol> symbols = GetSymbols(varNames);

+            List<Term> unwrapNoPatterns = Unwrap(no_patterns);

             Term unwrapBody = Unwrap(body);

 

             List<Term> bound = new List<Term>();

@@ -302,28 +300,11 @@ namespace Microsoft.Boogie.Z3
                 Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]);

                 bound.Add(Unwrap(t));

             }

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

-            return Wrap(termAst);

-        }

 

-        public Z3TermAst MakeExists(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body)

-        {

-            List<Pattern> unwrapPatterns = Unwrap(patterns);

-            // List<Term> unwrapNoPatterns = Unwrap(no_patterns);

-            // List<Sort> z3Types = GetTypes(boogieTypes);

-            // List<Symbol> symbols = GetSymbols(varNames);

-            Term unwrapBody = Unwrap(body);

-

-            List<Term> bound = new List<Term>();

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

-            {

-                Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]);

-                bound.Add(Unwrap(t));

-            }

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

+            Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid), unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), bound.ToArray(), unwrapBody);

             return Wrap(termAst);

         }

-

+   

         private static bool Equals(List<string> l, List<string> r)

         {

             Debug.Assert(l != null);

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index ade8cad0..17435e14 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -28,11 +28,8 @@ namespace Microsoft.Boogie.Z3 {
     public Z3PatternAst MakePattern(List<Z3TermAst> exprs) {

       return new Z3StubPatternAst();

     }

-    public Z3TermAst MakeForall(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

-      return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeExists(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

-      return new Z3StubTermAst();

+    public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

+        return new Z3StubTermAst();

     }

     public List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels) {

       return new List<string>();

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index 6397ccba..c2eeb45f 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -129,27 +129,22 @@ namespace Microsoft.Boogie.Z3
                 Z3TermAst body = Linearise(node.Body, options);

                 Z3TermAst result;

                 uint weight = 1;

+                string qid = "";

+                int skolemid = 0;

 

-                /*

                 if (options.QuantifierIds)

                 {

-                    // only needed for Z3

                     VCQuantifierInfos infos = node.Infos;

                     Contract.Assert(infos != null);

                     if (infos.qid != null)

                     {

-                        wr.Write("(QID ");

-                        wr.Write(infos.qid);

-                        wr.Write(") ");

+                        qid = infos.qid;

                     }

                     if (0 <= infos.uniqueId)

                     {

-                        wr.Write("(SKOLEMID ");

-                        wr.Write(infos.uniqueId);

-                        wr.Write(") ");

+                        skolemid = infos.uniqueId;

                     }

                 }

-                */

 

                 if (options.UseWeights)

                 {

@@ -159,9 +154,9 @@ namespace Microsoft.Boogie.Z3
                 switch (node.Quan)

                 {

                     case Quantifier.ALL:

-                        result = cm.MakeForall(weight, varNames, varTypes, patterns, no_patterns, body); break;

+                        result = cm.MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;

                     case Quantifier.EX:

-                        result = cm.MakeExists(weight, varNames, varTypes, patterns, no_patterns, body); break;

+                        result = cm.MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;

                     default:

                         throw new Exception("unknown quantifier kind " + node.Quan);

                 }

diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 1aa4534f..dc96a6ad 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.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>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid>

     <OutputType>Library</OutputType>

@@ -45,7 +45,7 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>

     </Reference>

-    <Reference Include="Microsoft.Z3, Version=2.0.3662.37897, Culture=neutral, PublicKeyToken=9c8d792caae602a2, processorArchitecture=x86">

+    <Reference Include="Microsoft.Z3, Version=2.0.40827.2, Culture=neutral, PublicKeyToken=9c8d792caae602a2, processorArchitecture=x86">

       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\..\Binaries\Microsoft.Z3.dll</HintPath>

     </Reference>