From d54c349601e9a4da8d28919008c85ca990447ead Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 2 Jul 2013 18:58:19 -0700
Subject: Worked on the parallelization.

---
 Source/Provers/SMTLib/ProverInterface.cs   |  9 +++++++++
 Source/Provers/SMTLib/SMTLibProcess.cs     | 10 ++++++----
 Source/Provers/SMTLib/TypeDeclCollector.cs | 13 +++++++++++++
 Source/Provers/SMTLib/Z3.cs                |  4 ++--
 Source/VCGeneration/Check.cs               |  5 +++++
 5 files changed, 35 insertions(+), 6 deletions(-)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 96dc02a6..6e01ef26 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -395,6 +395,15 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();
     }
 
+    public void Reset()
+    {
+      SendThisVC("(reset)");
+      common.Clear();
+      AxiomsAreSetup = false;
+      ctx.Clear();
+      DeclCollector.Reset();
+    }
+
     private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, 
                                  Dictionary<int,Dictionary<string,string>> varSubst)
     {
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index f4fa5e75..2374a157 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -63,12 +63,14 @@ namespace Microsoft.Boogie.SMTLib
 
 
       try {
-        prover = Process.Start(psi);
+        prover = new Process();
+        prover.StartInfo = psi;        
         prover.ErrorDataReceived += prover_ErrorDataReceived;
-        prover.OutputDataReceived += prover_OutputDataReceived;        
-        prover.BeginErrorReadLine();
-        prover.BeginOutputReadLine();
+        prover.OutputDataReceived += prover_OutputDataReceived;
+        prover.Start();
         toProver = prover.StandardInput;
+        prover.BeginErrorReadLine();
+        prover.BeginOutputReadLine();        
       } catch (System.ComponentModel.Win32Exception e) {
         throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));
       }
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 9d908138..2bbe4978 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -101,6 +101,19 @@ void ObjectInvariant()
         _KnownLBL.Push(new HashSet<string>());
     }
 
+    public void Reset()
+    {
+      _KnownFunctions.Clear();
+      _KnownVariables.Clear();
+      _KnownTypes.Clear();
+      _KnownStoreFunctions.Clear();
+      _KnownSelectFunctions.Clear();
+      _KnownLBL.Clear();
+      AllDecls.Clear();
+      IncDecls.Clear();
+      InitializeKnownDecls();
+    }
+
     public void Push()
     {
         Contract.Assert(_KnownFunctions.Count > 0);
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index bc9e6992..24071457 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -160,10 +160,10 @@ namespace Microsoft.Boogie.SMTLib
                 proc.StartInfo.UseShellExecute = false;
                 proc.StartInfo.CreateNoWindow = true;
                 proc.Start();
+                string answer = proc.StandardOutput.ReadToEnd();
                 proc.WaitForExit();
                 if (proc.ExitCode == 0)
-                {
-                    string answer = proc.StandardOutput.ReadToEnd();
+                {                    
                     var firstdot = answer.IndexOf('.');
                     if (firstdot >= 0)
                     {
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 3249708e..5fe0bcea 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -188,6 +188,7 @@ namespace Microsoft.Boogie {
         {
           TheoremProver.SetTimeOut(0);
         }
+        TheoremProver.Reset();
     }
 
     private static void Setup(Program prog, ProverContext ctx)
@@ -465,6 +466,10 @@ namespace Microsoft.Boogie {
     public virtual void Close() {
     }
 
+    public void Reset()
+    {
+    }
+
     /// <summary>
     /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta)
     /// for now it is only implemented by ProcessTheoremProver and still requires some
-- 
cgit v1.2.3