Use the new ProverInterface's Evaluate method in stratified inlinig

(guarded by the flag /useProverEvaluate)

5 files changed, 45 insertions, 27 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 82768cf6..37c7eeae 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -399,6 +399,7 @@ namespace Microsoft.Boogie {
     public bool UseUnsatCoreForContractInfer = false;

     public bool PrintAssignment = false;

     public int InlineDepth = -1;

+    public bool UseProverEvaluate = false; // Use ProverInterface's Evaluate method, instead of model to get variable values

     public bool UseUncheckedContracts = false;

     public bool SimplifyLogFileAppend = false;

     public bool SoundnessSmokeTest = false;

@@ -1215,6 +1216,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("crossDependencies", ref HoudiniUseCrossDependencies) ||

               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||

               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||

+              ps.CheckBooleanFlag("useProverEvaluate", ref UseProverEvaluate) ||

               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||

               ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)

               ) {

@@ -1275,6 +1277,8 @@ namespace Microsoft.Boogie {
         if (ProverName == "Z3API" || ProverName == "SMTLIB") {

           ProverCCLimit = 1;

         }

+        if (UseProverEvaluate)

+            StratifiedInliningWithoutModels = true;

       }

 

       if (Trace) {

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index b1cef239..d336252e 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -45,7 +45,7 @@ namespace Microsoft.Boogie.SMTLib
     public bool OptimizeForBv = false;

 

     public bool ProduceModel() {

-      return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini ||

+      return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate ||

              ExpectingModel();

     }

 

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 795fc9ca..8e28362b 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -20,14 +20,15 @@ namespace Microsoft.Boogie {
 

   public class CalleeCounterexampleInfo {

     public Counterexample counterexample;

-    public List<Model.Element>/*!>!*/ args;

+    public List<object>/*!>!*/ args;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(args));

     }

 

-    public CalleeCounterexampleInfo(Counterexample cex, List<Model.Element/*!>!*/> x) {

+    public CalleeCounterexampleInfo(Counterexample cex, List<object/*!>!*/> x)

+    {

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

       counterexample = cex;

       args = x;

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 6ad97141..e32b3255 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -477,7 +477,7 @@ namespace VC {
       }

 

       return extractLoopTraceRec(

-          new CalleeCounterexampleInfo(cex, new List<Model.Element>()),

+          new CalleeCounterexampleInfo(cex, new List<object>()),

           mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

     }

 

@@ -2614,31 +2614,44 @@ namespace VC {
               }

             }

 

-            if (calleeName.StartsWith(recordProcName) && errModel != null) {

+            if (calleeName.StartsWith(recordProcName) && (errModel != null || CommandLineOptions.Clo.UseProverEvaluate)) {

               var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)];

 

               // Record concrete value of the argument to this procedure

-              var args = new List<Model.Element>();

-              if (expr is VCExprIntLit) {

-                args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));

+              var args = new List<object>();

+              if (errModel == null && CommandLineOptions.Clo.UseProverEvaluate)

+              {

+                  args.Add(theoremProver.Evaluate(expr));

               }

-              else if (expr == VCExpressionGenerator.True) {

-                args.Add(errModel.MkElement("true"));

-              }

-              else if (expr == VCExpressionGenerator.False) {

-                args.Add(errModel.MkElement("false"));

-              }

-              else if (expr is VCExprVar) {

-                var idExpr = expr as VCExprVar;

-                string name = theoremProver.Context.Lookup(idExpr);

-                Contract.Assert(name != null);

-                Model.Func f = errModel.TryGetFunc(name);

-                if (f != null) {

-                  args.Add(f.GetConstant());

-                }

-              }

-              else {

-                Contract.Assert(false);

+              else

+              {

+                  if (expr is VCExprIntLit)

+                  {

+                      args.Add(errModel.MkElement((expr as VCExprIntLit).Val.ToString()));

+                  }

+                  else if (expr == VCExpressionGenerator.True)

+                  {

+                      args.Add(errModel.MkElement("true"));

+                  }

+                  else if (expr == VCExpressionGenerator.False)

+                  {

+                      args.Add(errModel.MkElement("false"));

+                  }

+                  else if (expr is VCExprVar)

+                  {

+                      var idExpr = expr as VCExprVar;

+                      string name = theoremProver.Context.Lookup(idExpr);

+                      Contract.Assert(name != null);

+                      Model.Func f = errModel.TryGetFunc(name);

+                      if (f != null)

+                      {

+                          args.Add(f.GetConstant());

+                      }

+                  }

+                  else

+                  {

+                      Contract.Assert(false);

+                  }

               }

               calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                    new CalleeCounterexampleInfo(null, args);

@@ -2659,7 +2672,7 @@ namespace VC {
               orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));

               var calleeInfo = implName2StratifiedInliningInfo[calleeName];

               calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

-                  new CalleeCounterexampleInfo(GenerateTrace(labels, errModel, calleeId, calleeInfo.impl, calleeInfo.mvInfo), new List<Model.Element>());

+                  new CalleeCounterexampleInfo(GenerateTrace(labels, errModel, calleeId, calleeInfo.impl, calleeInfo.mvInfo), new List<object>());

               orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));

             }

           }

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index b13b7e35..bcf0b0e5 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2199,7 +2199,7 @@ namespace VC {
         }

 

         return extractLoopTraceRec(

-            new CalleeCounterexampleInfo(cex, new List<Model.Element>()),

+            new CalleeCounterexampleInfo(cex, new List<object>()),

             mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

     }