Fixed non-incremental option of stratified inlining

1 files changed, 19 insertions, 3 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 6a12c3e9..dad151e5 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -609,6 +609,7 @@ namespace VC
             abstract public void Pop();

             abstract public void AddAxiom(VCExpr vc);

             abstract public void LogComment(string str);

+            abstract public void updateMainVC(VCExpr vcMain);

             virtual public Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

             {

                 Outcome ret;

@@ -657,6 +658,11 @@ namespace VC
                 numQueries = 0;

             }

 

+            public override void updateMainVC(VCExpr vcMain)

+            {

+                this.vcMain = vcMain;

+            }

+

             public override Outcome CheckVC()

             {

                 Contract.Requires(vcMain != null);

@@ -757,6 +763,11 @@ namespace VC
                 TheoremProver.Assert(vcMain, false);

             }

 

+            public override void updateMainVC(VCExpr vcMain)

+            {

+                throw new NotImplementedException("Stratified non-incremental search is not yet supported with z3api");

+            }

+

             public override Outcome CheckVC()

             {

                 Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

@@ -850,7 +861,7 @@ namespace VC
         public class VerificationState

         {

             // The VC of main

-            public VCExpr vcMain;

+            public VCExpr vcMain { get; private set; }

             // The call tree

             public FCallHandler calls;

             // Error reporter (stores models)

@@ -888,6 +899,12 @@ namespace VC
                 vcSize = 0;

                 expansionCount = 0;

             }

+

+            public void updateMainVC(VCExpr vcMain)

+            {

+                this.vcMain = vcMain;

+                checker.updateMainVC(vcMain);

+            }

         }

 

         public Outcome FindLeastToVerify(Implementation impl, Program program, ref HashSet<string> allBoolVars)

@@ -1626,7 +1643,6 @@ namespace VC
         // Does on-demand inlining -- inlines procedures into the VC of main.

         private void DoExpansionAndInline(List<int>/*!*/ candidates, VerificationState vState)

         {

-            Contract.Requires(vState.vcMain != null);

             Contract.Requires(candidates != null);

             Contract.Requires(vState.calls != null);

             Contract.Requires(vState.checker != null);

@@ -1698,7 +1714,7 @@ namespace VC
 

             }

 

-            vState.vcMain = inliner.Mutate(vState.vcMain, true);

+            vState.updateMainVC(inliner.Mutate(vState.vcMain, true));

             vState.vcSize = SizeComputingVisitor.ComputeSize(vState.vcMain);

         }