Added CheckAssumptions api interface

4 files changed, 138 insertions, 5 deletions

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index a5f2d6be..750e4a00 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -100,6 +100,13 @@ namespace Microsoft.Boogie.Z3
             outcome = cm.Check(out z3LabelModels);

         }

 

+        public override void CheckAssumptions(List<VCExpr> assumptions)

+        {

+            Z3SafeContext cm = context.cm;

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

+            outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels);

+        }

+

         public override void Push()

         {

             Z3SafeContext cm = context.cm;

diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 0e3d35ea..d52a7f99 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -396,6 +396,66 @@ namespace Microsoft.Boogie.Z3
             }

         }

 

+        public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions, out List<Z3ErrorModelAndLabels> boogieErrors)

+        {

+            Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");

+            boogieErrors = new List<Z3ErrorModelAndLabels>();

+            LBool outcome = LBool.Undef;

+

+            Model z3Model;

+            Term proof;

+            Term[] core;

+            Term[] assumption_terms = new Term[assumptions.Count];

+

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

+            {

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

+                Z3TermAst z3ast = (Z3TermAst)assumptions[i].Accept(visitor, linOptions);

+                assumption_terms[i] = Unwrap(z3ast);

+            }

+

+            log("check-assumptions ...");

+            outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);

+

+            if (outcome != LBool.False)

+            {

+                Debug.Assert(z3Model != null);

+                LabeledLiterals labels = z3.GetRelevantLabels();

+                Debug.Assert(labels != null);

+

+                List<string> labelStrings = new List<string>();

+                uint numLabels = labels.GetNumLabels();

+                for (uint i = 0; i < numLabels; ++i)

+                {

+                    Symbol sym = labels.GetLabel(i);

+                    string labelName = z3.GetSymbolString(sym);

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

+                    {

+                        labels.Disable(i);

+                    }

+                    labelStrings.Add(labelName);

+                }

+                boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));

+

+                labels.Dispose();

+                z3Model.Dispose();

+            }

+

+            if (boogieErrors.Count > 0)

+            {

+                return ProverInterface.Outcome.Invalid;

+            }

+            else if (outcome == LBool.False)

+            {

+                return ProverInterface.Outcome.Valid;

+            }

+            else

+            {

+                Debug.Assert(outcome == LBool.Undef);

+                return ProverInterface.Outcome.Undetermined;

+            }

+        }

+

         public void TypeCheckBool(Z3TermAst term)

         {

             Term unwrapTerm = Unwrap(term);

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e602e293..54a8823f 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -671,6 +671,7 @@ namespace Microsoft.Boogie {
       public abstract void Assert(VCExpr vc, bool polarity);

       public abstract void AssertAxioms();

       public abstract void Check();

+      public abstract void CheckAssumptions(List<VCExpr> assumptions);

       public abstract void Push();

   }

 

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 0e962307..ef8a4c80 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -495,6 +495,23 @@ namespace VC
             abstract public void Pop();

             abstract public void AddAxiom(VCExpr vc);

             abstract public void LogComment(string str);

+            virtual public Outcome CheckAssumptions(List<VCExpr> assumptions)

+            {

+                if (assumptions.Count == 0)

+                {

+                    return CheckVC();

+                }

+

+                Push();

+                foreach (var a in assumptions)

+                {

+                    AddAxiom(a);

+                }

+                var ret = CheckVC();

+                Pop();

+

+                return ret;

+            }

         }

 

         public class NormalChecker : StratifiedCheckerInterface

@@ -665,7 +682,32 @@ namespace VC
             {

                 checker.TheoremProver.LogComment(str);

             }

+            /*

+            public override Outcome CheckAssumptions(List<VCExpr> assumptions)

+            {

+                TheoremProver.AssertAxioms();

+                TheoremProver.CheckAssumptions(assumptions);

+                ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter);

+                numQueries++;

 

+                switch (outcome)

+                {

+                    case ProverInterface.Outcome.Valid:

+                        return Outcome.Correct;

+                    case ProverInterface.Outcome.Invalid:

+                        return Outcome.Errors;

+                    case ProverInterface.Outcome.OutOfMemory:

+                        return Outcome.OutOfMemory;

+                    case ProverInterface.Outcome.TimeOut:

+                        return Outcome.TimedOut;

+                    case ProverInterface.Outcome.Undetermined:

+                        return Outcome.Inconclusive;

+                    default:

+                        Contract.Assert(false);

+                        throw new cce.UnreachableException();

+                }

+            }

+             */

         }

 

         // Store important information related to a single VerifyImplementation query

@@ -961,6 +1003,13 @@ namespace VC
             reporter.underapproximationMode = true;

             checker.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");

 

+            var assumptions = new List<VCExpr>();

+            foreach (int id in calls.currCandidates)

+            {

+                assumptions.Add(calls.getFalseExpr(id));

+            }

+

+            /*

             checker.Push();

 

             foreach (int id in calls.currCandidates)

@@ -973,6 +1022,9 @@ namespace VC
 

             // Pop

             checker.Pop();

+            */

+

+            ret = checker.CheckAssumptions(assumptions);

 

             checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");

 

@@ -1009,8 +1061,7 @@ namespace VC
             bool allTrue = true;

             bool allFalse = true;

 

-            checker.Push();

-

+            assumptions = new List<VCExpr>();

             foreach (int id in calls.currCandidates)

             {

                 if (calls.getRecursionBound(id) <= bound)

@@ -1020,11 +1071,23 @@ namespace VC
                 }

                 else

                 {

-                    checker.AddAxiom(calls.getFalseExpr(id));

+                    //checker.AddAxiom(calls.getFalseExpr(id));

+                    assumptions.Add(calls.getFalseExpr(id));

                     allTrue = false;

                 }

             }

 

+            if (allFalse)

+            {

+                ret = Outcome.Correct;

+            }

+            else

+            {

+                ret = checker.CheckAssumptions(assumptions);

+            }

+            /*

+            checker.Push();

+

             // Check

             if (allFalse)

             {

@@ -1039,6 +1102,7 @@ namespace VC
 

             // Pop

             checker.Pop();

+            */

 

             if (ret != Outcome.Correct && ret != Outcome.Errors)

             {

@@ -1105,7 +1169,7 @@ namespace VC
                 {

                     GenerateVCForStratifiedInlining(program, info, checker);

                 }

-

+                //Console.WriteLine("Inlining {0}", procName);

                 VCExpr expansion = cce.NonNull(info.vcexpr);

 

                 // Instantiate the "forall" variables

@@ -1534,7 +1598,8 @@ namespace VC
             // Return the formula (candidate IFF false)

             public VCExpr getFalseExpr(int candidateId)

             {

-                return Gen.Eq(VCExpressionGenerator.False, id2ControlVar[candidateId]);

+                //return Gen.Eq(VCExpressionGenerator.False, id2ControlVar[candidateId]);

+                return Gen.Not(id2ControlVar[candidateId]);

             }

 

             // Return the formula (candidate IFF true)