DafnyExtension: Integrated support for multiple Z3 instances in Boogie (incl. request cancellation).

3 files changed, 13 insertions, 7 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 11bc1ef6..392a6f17 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2383,7 +2383,7 @@ namespace Microsoft.Dafny {
       var prefix = UniqueIdPrefix ?? decl.tok.filename;

       if (impl != null && !string.IsNullOrEmpty(prefix))

       {

-        decl.AddAttribute("id", prefix + ":" + impl.Id);

+        decl.AddAttribute("id", prefix + ":" + impl.Name + ":0");

       }

     }

 

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 4819123c..b5629b96 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -35,6 +35,7 @@ namespace DafnyLanguage
         var options = new Dafny.DafnyOptions();

         options.ProverKillTime = 10;

         options.ErrorTrace = 0;

+        options.VcsCores = System.Environment.ProcessorCount;

         Dafny.DafnyOptions.Install(options);

         options.ApplyDefaultOptions();

 

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index e481f141..bfa49b21 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -130,6 +130,10 @@ namespace DafnyLanguage
       {

         if (disposing)

         {

+          if (lastRequestId != null)

+          {

+            Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);

+          }

           _buffer.Changed -= buffer_Changed;

           _errorProvider.Dispose();

           ClearCachedVerificationResults();

@@ -175,6 +179,7 @@ namespace DafnyLanguage
     bool verificationInProgress;  // this field is protected by "this".  Invariant:  !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0

     Thread verificationWorker;

     bool verificationDisabled;

+    string lastRequestId;

 

     public bool VerificationDisabled

     {

@@ -236,17 +241,17 @@ namespace DafnyLanguage
         // Notify to-whom-it-may-concern about the changes we just made

         NotifyAboutChangedTags(snap);

 

-        string requestId = null;

+        lastRequestId = null;

         lock (RequestIdToSnapshot)

         {

           do

           {

-            requestId = DateTime.UtcNow.Ticks.ToString();

-          } while (RequestIdToSnapshot.ContainsKey(requestId));

-          RequestIdToSnapshot[requestId] = snap;

+            lastRequestId = DateTime.UtcNow.Ticks.ToString();

+          } while (RequestIdToSnapshot.ContainsKey(lastRequestId));

+          RequestIdToSnapshot[lastRequestId] = snap;

         }

 

-        verificationWorker = new Thread(() => VerificationWorker(prog, snap, requestId, resolver));

+        verificationWorker = new Thread(() => VerificationWorker(prog, snap, lastRequestId, resolver));

         verificationWorker.IsBackground = true;

         if (_document != null)

         {

@@ -267,7 +272,7 @@ namespace DafnyLanguage
 

     public void StopVerification()

     {

-      verificationWorker.Abort();  // TODO(wuestholz): Make sure this kills the corresponding Z3 process.

+      Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);

       lock (this)

       {

         bufferChangesPreVerificationStart.Clear();