bunch of refactorings

- moved doomed and predication code into separate projects;
  for doomed there is a static dependency from BoogieDriver
  but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs

2 files changed, 9 insertions, 10 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 75ba7372..402b5c68 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -594,15 +594,6 @@ namespace Microsoft.Boogie {
         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

 

-      if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0) {

-        BlockPredicator.Predicate(program, false, false);

-        if (CommandLineOptions.Clo.PrintInstrumented) {

-          using (TokenTextWriter writer = new TokenTextWriter(Console.Out)) {

-            program.Emit(writer);

-          }

-        }

-      }

-

       Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;

       if (CommandLineOptions.Clo.ExtractLoops)

       {

@@ -668,7 +659,7 @@ namespace Microsoft.Boogie {
       try {

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

           vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        } else if(CommandLineOptions.Clo.StratifiedInlining > 0) {

+        } else if (CommandLineOptions.Clo.StratifiedInlining > 0) {

           vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

         } else {

           vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 9edd2df7..36795a68 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -226,6 +226,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Doomed\Doomed.csproj">

+      <Project>{884386a3-58e9-40bb-a273-b24976775553}</Project>

+      <Name>Doomed</Name>

+    </ProjectReference>

     <ProjectReference Include="..\Graph\Graph.csproj">

       <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

@@ -238,6 +242,10 @@
       <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Predication\Predication.csproj">

+      <Project>{afaa5ce1-c41b-44f0-88f8-fd8a43826d44}</Project>

+      <Name>Predication</Name>

+    </ProjectReference>

     <ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">

       <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>

       <Name>SMTLib</Name>