Cleanup

boogie-org · Oct 3, 2024 · c603cc8 · c603cc8
1 parent ff1442a
commit c603cc8
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 8 deletions.
diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs
@@ -24,7 +24,7 @@ public class VerificationTask : IVerificationTask {
   public IToken ScopeToken => Split.Implementation.tok;
   public string ScopeId => Split.Implementation.VerboseName;
 
-  public IToken Token => Split.Origin;
+  public IToken Token => Split.Token;
   public ManualSplit Split { get; }
 
   public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgram, ManualSplit split,
@@ -45,7 +45,7 @@ public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgra
   public IVerificationTask FromSeed(int newSeed)
   {
     var split = new ManualSplit(Split.Options, () => Split.Blocks, 
-      Split.parent, Split.Run, Split.Origin, newSeed);
+      Split.parent, Split.Run, Split.Token, newSeed);
     split.SplitIndex = Split.SplitIndex;
     return new VerificationTask(engine, ProcessedProgram, split, modelViewInfo);
   }

diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs
@@ -8,7 +8,7 @@ namespace VC;
 public class ManualSplit : Split
 {
 
-  public ImplementationPartOrigin Origin { get; }
+  public ImplementationPartOrigin Token { get; }
 
   public ManualSplit(VCGenOptions options, 
     Func<List<Block>> blocks, 
@@ -17,6 +17,6 @@ public ManualSplit(VCGenOptions options,
     ImplementationPartOrigin origin, int? randomSeed = null) 
     : base(options, blocks, parent, run, randomSeed)
   {
-    Origin = origin;
+    Token = origin;
   }
 }
diff --git a/Source/VCGeneration/Splits/Split.cs b/Source/VCGeneration/Splits/Split.cs
@@ -14,7 +14,6 @@
 
 namespace VC
 {
-  // TODO rename since it's not only used to split a proof into two. For example focus doesn't really split
   public class Split : ProofRun
   {
       public VCGenOptions Options { get; }
@@ -99,7 +98,7 @@ private void PrintSplit() {
           Thread.Sleep(100);
         }
 
-        var prefix = (this is ManualSplit manualSplit) ? manualSplit.Origin.ShortName : "";
+        var prefix = (this is ManualSplit manualSplit) ? manualSplit.Token.ShortName : "";
         var name = Implementation.Name + prefix; 
         using var writer = printToConsole
           ? new TokenTextWriter("<console>", Options.OutputWriter, false, Options.PrettyPrint, Options) 

diff --git a/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs b/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs
@@ -144,7 +144,7 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance
         await run.OutputWriter.WriteLineAsync(string.Format(CultureInfo.InvariantCulture, 
             "    checking split {1}/{2}{3}, {4:0.00}%, {0} ...",
             split.Stats, splitIdxStr, total,
-            split is ManualSplit manualSplit ? $" (line {manualSplit.Origin.line})" : "", 
+            split is ManualSplit manualSplit ? $" (line {manualSplit.Token.line})" : "", 
             100 * provenCost / (provenCost + remainingCost)));
       }
 

diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs
@@ -131,7 +131,7 @@ private static bool ShouldSplitHere(Cmd c) {
       return null;
     }
 
-    return createVc(new SplitOrigin(split?.tok ?? partToSplit.Origin), newBlocks);
+    return createVc(new SplitOrigin(split?.tok ?? partToSplit.Token), newBlocks);
 
     List<Cmd> GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock)
     {