diff options
| -rw-r--r-- | Source/BVD/App.config | 6 | ||||
| -rw-r--r-- | Source/BVD/BVD.csproj | 99 | ||||
| -rw-r--r-- | Source/BVD/Program.cs (renamed from Source/ModelViewer/Program.cs) | 0 | ||||
| -rw-r--r-- | Source/BVD/Properties/AssemblyInfo.cs | 36 | ||||
| -rw-r--r-- | Source/Boogie.sln | 516 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 6 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 93 | ||||
| -rw-r--r-- | Source/Houdini/CandidateDependenceAnalyser.cs | 211 | ||||
| -rw-r--r-- | Source/Houdini/Checker.cs | 48 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 110 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.csproj | 3 | ||||
| -rw-r--r-- | Source/Houdini/StagedHoudini.cs | 348 | ||||
| -rw-r--r-- | Source/ModelViewer/Main.cs | 51 | ||||
| -rw-r--r-- | Source/ModelViewer/ModelViewer.csproj | 14 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProcess.cs | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 17 |
16 files changed, 1065 insertions, 494 deletions
diff --git a/Source/BVD/App.config b/Source/BVD/App.config new file mode 100644 index 00000000..fad249e4 --- /dev/null +++ b/Source/BVD/App.config @@ -0,0 +1,6 @@ +<?xml version="1.0" encoding="utf-8" ?>
+<configuration>
+ <startup>
+ <supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5" />
+ </startup>
+</configuration>
\ No newline at end of file diff --git a/Source/BVD/BVD.csproj b/Source/BVD/BVD.csproj new file mode 100644 index 00000000..0b32dd22 --- /dev/null +++ b/Source/BVD/BVD.csproj @@ -0,0 +1,99 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProjectGuid>{8A05D14E-F2BF-4890-BBE0-D76B18A50797}</ProjectGuid>
+ <OutputType>WinExe</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>
+ <AssemblyName>BVD</AssemblyName>
+ <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <PublishUrl>publish\</PublishUrl>
+ <Install>true</Install>
+ <InstallFrom>Disk</InstallFrom>
+ <UpdateEnabled>false</UpdateEnabled>
+ <UpdateMode>Foreground</UpdateMode>
+ <UpdateInterval>7</UpdateInterval>
+ <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+ <UpdatePeriodically>false</UpdatePeriodically>
+ <UpdateRequired>false</UpdateRequired>
+ <MapFileExtensions>true</MapFileExtensions>
+ <ApplicationRevision>0</ApplicationRevision>
+ <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+ <IsWebBootstrapper>false</IsWebBootstrapper>
+ <UseApplicationTrust>false</UseApplicationTrust>
+ <BootstrapperEnabled>true</BootstrapperEnabled>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup>
+ <StartupObject />
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Deployment" />
+ <Reference Include="System.Drawing" />
+ <Reference Include="System.Numerics" />
+ <Reference Include="System.Windows.Forms" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="Program.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="App.config" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\ModelViewer\ModelViewer.csproj">
+ <Project>{a678c6eb-b329-46a9-bbfc-7585f01acd7c}</Project>
+ <Name>ModelViewer</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <BootstrapperPackage Include=".NETFramework,Version=v4.5">
+ <Visible>False</Visible>
+ <ProductName>Microsoft .NET Framework 4.5 %28x86 and x64%29</ProductName>
+ <Install>true</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+ <Install>false</Install>
+ </BootstrapperPackage>
+ <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+ <Visible>False</Visible>
+ <ProductName>.NET Framework 3.5 SP1</ProductName>
+ <Install>false</Install>
+ </BootstrapperPackage>
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/ModelViewer/Program.cs b/Source/BVD/Program.cs index 669ea995..669ea995 100644 --- a/Source/ModelViewer/Program.cs +++ b/Source/BVD/Program.cs diff --git a/Source/BVD/Properties/AssemblyInfo.cs b/Source/BVD/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..3512374e --- /dev/null +++ b/Source/BVD/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("BVD")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("BVD")]
+[assembly: AssemblyCopyright("Copyright © 2013")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("00610a12-cf4c-4c29-af30-31a99d22b9d8")]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index c83c8770..cadcaacb 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -3,12 +3,12 @@ Microsoft Visual Studio Solution File, Format Version 12.00 # Visual Studio 2012
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"
-EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbsInt", "AbsInt\AbsInt.csproj", "{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SMTLib.csproj", "{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}"
+EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "VCGeneration\VCGeneration.csproj", "{E1F10180-C7B9-4147-B51F-FA1B701966DC}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csproj", "{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}"
@@ -35,6 +35,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed", "Doomed\Doomed.csp EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "ExecutionEngine\ExecutionEngine.csproj", "{EAA5EB79-D475-4601-A59B-825C191CD25F}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8A05D14E-F2BF-4890-BBE0-D76B18A50797}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Checked|.NET = Checked|.NET
@@ -55,6 +57,32 @@ Global z3apidebug|x86 = z3apidebug|x86
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|.NET.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|.NET.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.Build.0 = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|x86.ActiveCfg = Release|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
+ {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.Build.0 = z3apidebug|x86
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|.NET.ActiveCfg = Checked|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -81,31 +109,58 @@ Global {0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.Build.0 = z3apidebug|x86
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|x86.ActiveCfg = Checked|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|x86.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|.NET.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.Build.0 = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|x86.ActiveCfg = Release|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|.NET.ActiveCfg = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|.NET.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.Build.0 = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|x86.ActiveCfg = Release|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|.NET.ActiveCfg = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|.NET.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.Build.0 = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|x86.ActiveCfg = Release|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Checked|.NET.ActiveCfg = Checked|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -131,6 +186,31 @@ Global {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|.NET.ActiveCfg = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|.NET.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.Build.0 = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|x86.ActiveCfg = Release|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|.NET.ActiveCfg = Checked|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -156,80 +236,31 @@ Global {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|.NET.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Checked|x86.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Debug|x86.ActiveCfg = Debug|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|.NET.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.Release|x86.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
- {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|x86.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|x86.ActiveCfg = Checked|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|.NET.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Debug|x86.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|.NET.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Any CPU.Build.0 = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Release|x86.ActiveCfg = Release|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|.NET.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Any CPU.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.Build.0 = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.ActiveCfg = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.Build.0 = Checked|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|.NET.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Any CPU.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.Build.0 = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.ActiveCfg = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.Build.0 = Debug|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|.NET.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Any CPU.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.Build.0 = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.Build.0 = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|.NET.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Any CPU.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.Build.0 = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.ActiveCfg = Release|x86
- {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.Build.0 = Release|x86
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|.NET.ActiveCfg = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|.NET.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Any CPU.Build.0 = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.Release|x86.ActiveCfg = Release|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
+ {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Checked|.NET.ActiveCfg = Checked|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -255,6 +286,30 @@ Global {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|.NET.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Any CPU.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|Mixed Platforms.Build.0 = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.ActiveCfg = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Checked|x86.Build.0 = Checked|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|.NET.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Any CPU.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|Mixed Platforms.Build.0 = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.ActiveCfg = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Debug|x86.Build.0 = Debug|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|.NET.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Any CPU.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|Mixed Platforms.Build.0 = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.Release|x86.Build.0 = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|.NET.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Any CPU.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|Mixed Platforms.Build.0 = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.ActiveCfg = Release|x86
+ {A678C6EB-B329-46A9-BBFC-7585F01ACD7C}.z3apidebug|x86.Build.0 = Release|x86
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|.NET.ActiveCfg = Checked|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.Checked|Any CPU.Build.0 = Checked|Any CPU
@@ -280,55 +335,31 @@ Global {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|x86.ActiveCfg = Release|Any CPU
{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|x86.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|.NET.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|x86.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|x86.ActiveCfg = Debug|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|.NET.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|x86.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
- {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|x86.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Checked|x86.ActiveCfg = Checked|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Debug|x86.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|.NET.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Any CPU.Build.0 = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.Release|x86.ActiveCfg = Release|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {B230A69C-C466-4065-B9C1-84D80E76D802}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|.NET.ActiveCfg = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Any CPU.Build.0 = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|x86.ActiveCfg = Checked|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|.NET.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.Build.0 = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|x86.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.Build.0 = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU
@@ -354,58 +385,54 @@ Global {CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU
{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.Build.0 = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Checked|x86.ActiveCfg = Checked|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|x86.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|.NET.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Any CPU.Build.0 = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Release|x86.ActiveCfg = Release|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.ActiveCfg = z3apidebug|x86
- {DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.z3apidebug|x86.Build.0 = z3apidebug|x86
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|x86.ActiveCfg = Checked|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|x86.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|.NET.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.Build.0 = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|x86.ActiveCfg = Release|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|.NET.ActiveCfg = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.ActiveCfg = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Any CPU.Build.0 = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU
- {E1F10180-C7B9-4147-B51F-FA1B701966DC}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Checked|x86.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.Release|x86.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Checked|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.Release|x86.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {884386A3-58E9-40BB-A273-B24976775553}.z3apidebug|x86.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.Checked|.NET.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.Checked|Any CPU.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.Checked|Any CPU.Build.0 = Release|Any CPU
@@ -430,66 +457,35 @@ Global {EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|x86.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|.NET.ActiveCfg = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Any CPU.ActiveCfg = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Any CPU.Build.0 = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.ActiveCfg = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|Mixed Platforms.Build.0 = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Checked|x86.ActiveCfg = Checked|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|.NET.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|x86.ActiveCfg = Debug|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|.NET.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.Build.0 = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|x86.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU
- {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.Build.0 = Release|Any CPU
- EndGlobalSection
- GlobalSection(NestedProjects) = preSolution
- {9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
- EndGlobalSection
- GlobalSection(MonoDevelopProperties) = preSolution
- StartupItem = Provers\SMTLib\SMTLib.csproj
- Policies = $0
- $0.DotNetNamingPolicy = $1
- $1.DirectoryNamespaceAssociation = None
- $1.ResourceNamePolicy = FileFormatDefault
- $0.TextStylePolicy = $2
- $2.FileWidth = 120
- $2.TabWidth = 2
- $2.IndentWidth = 2
- $2.inheritsSet = Mono
- $2.inheritsScope = text/plain
- $2.scope = text/x-csharp
- $0.CSharpFormattingPolicy = $3
- $3.ElseIfNewLinePlacement = SameLine
- $3.AfterDelegateDeclarationParameterComma = True
- $3.inheritsSet = Mono
- $3.inheritsScope = text/x-csharp
- $3.scope = text/x-csharp
- $0.TextStylePolicy = $4
- $4.FileWidth = 120
- $4.TabWidth = 2
- $4.IndentWidth = 2
- $4.inheritsSet = Mono
- $4.inheritsScope = text/plain
- $4.scope = text/plain
- $0.StandardHeader = $5
- $5.Text =
- $5.IncludeInNewFiles = True
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|x86.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|.NET.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|x86.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|x86.ActiveCfg = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
+ GlobalSection(NestedProjects) = preSolution
+ {9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
+ EndGlobalSection
EndGlobal
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 802c3afd..46d030d2 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -401,6 +401,7 @@ namespace Microsoft.Boogie { public bool DebugStagedHoudini = false;
public bool StagedHoudiniReachabilityAnalysis = false;
public bool StagedHoudiniMergeIgnoredCandidates = false;
+ public int StagedHoudiniThreads = 2;
public string VariableDependenceIgnore = null;
public string AbstractHoudini = null;
public bool UseUnsatCoreForContractInfer = false;
@@ -903,6 +904,11 @@ namespace Microsoft.Boogie { return true;
}
+ case "stagedHoudiniThreads": {
+ ps.GetNumericArgument(ref StagedHoudiniThreads);
+ return true;
+ }
+
case "stagedHoudiniReachabilityAnalysis": {
if (ps.ConfirmArgumentCount(0)) {
StagedHoudiniReachabilityAnalysis = true;
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 96c294ea..e988c638 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -457,21 +457,6 @@ namespace Microsoft.Boogie EliminateDeadVariablesAndInline(program);
- if (CommandLineOptions.Clo.StagedHoudini > 0)
- {
- var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program);
- candidateDependenceAnalyser.Analyse();
- candidateDependenceAnalyser.ApplyStages();
- if (CommandLineOptions.Clo.Trace)
- {
- candidateDependenceAnalyser.dump();
- int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
- CommandLineOptions.Clo.PrintUnstructured = 2;
- PrintBplFile("staged.bpl", program, false, false);
- CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
- }
- }
-
var stats = new PipelineStatistics();
oc = InferAndVerify(program, stats);
switch (oc)
@@ -1107,8 +1092,67 @@ namespace Microsoft.Boogie return RunAbstractHoudini(program, stats, er);
}
- Houdini.Houdini houdini = new Houdini.Houdini(program);
+ if (CommandLineOptions.Clo.StagedHoudini != null)
+ {
+ return RunStagedHoudini(program, stats, er);
+ }
+
+ Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
+ Houdini.Houdini houdini = new Houdini.Houdini(program, houdiniStats);
Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ houdini.Close();
+
+ if (CommandLineOptions.Clo.PrintAssignment)
+ {
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment)
+ {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
+ }
+
+ if (CommandLineOptions.Clo.Trace)
+ {
+ int numTrueAssigns = 0;
+ foreach (var x in outcome.assignment)
+ {
+ if (x.Value)
+ numTrueAssigns++;
+ }
+ Console.WriteLine("Number of true assignments = " + numTrueAssigns);
+ Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
+ Console.WriteLine("Prover time = " + houdiniStats.proverTime.ToString("F2"));
+ Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings);
+ }
+
+ foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
+ {
+ ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
+ ProcessErrors(x.errors, x.outcome, Console.Out, er);
+ }
+
+ return PipelineOutcome.Done;
+ }
+
+ private static Program ProgramFromFile(string filename) {
+ Program p = ParseBoogieProgram(new List<string> { filename }, false);
+ System.Diagnostics.Debug.Assert(p != null);
+ LinearTypechecker linearTypechecker;
+ PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(p, filename, out linearTypechecker);
+ System.Diagnostics.Debug.Assert(oc == PipelineOutcome.ResolvedAndTypeChecked);
+ return p;
+ }
+
+ private static PipelineOutcome RunStagedHoudini(Program program, PipelineStatistics stats, ErrorReporterDelegate er)
+ {
+ Houdini.HoudiniSession.HoudiniStatistics houdiniStats = new Houdini.HoudiniSession.HoudiniStatistics();
+ // TODO - pass this in somewhere
+
+ Houdini.StagedHoudini houdini = new Houdini.StagedHoudini(program, ProgramFromFile);
+ Houdini.HoudiniOutcome outcome = houdini.PerformStagedHoudiniInference();
if (CommandLineOptions.Clo.PrintAssignment)
{
@@ -1129,11 +1173,11 @@ namespace Microsoft.Boogie }
Console.WriteLine("Number of true assignments = " + numTrueAssigns);
Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
- Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime.ToString("F2"));
- Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime.ToString("F2"));
- Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
- Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
- Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
+ Console.WriteLine("Prover time = " + houdiniStats.proverTime.ToString("F2"));
+ Console.WriteLine("Unsat core prover time = " + houdiniStats.unsatCoreProverTime.ToString("F2"));
+ Console.WriteLine("Number of prover queries = " + houdiniStats.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + houdiniStats.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + houdiniStats.numUnsatCorePrunings);
}
foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
@@ -1141,12 +1185,9 @@ namespace Microsoft.Boogie ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);
ProcessErrors(x.errors, x.outcome, Console.Out, er);
}
- //errorCount = outcome.ErrorCount;
- //verified = outcome.Verified;
- //inconclusives = outcome.Inconclusives;
- //timeOuts = outcome.TimeOuts;
- //outOfMemories = 0;
+
return PipelineOutcome.Done;
+
}
diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 09cef241..9a2eb404 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -6,13 +6,13 @@ using Microsoft.Boogie.GraphUtil; using Microsoft.Basetypes;
using System.Diagnostics;
-namespace Microsoft.Boogie {
+namespace Microsoft.Boogie.Houdini {
public class CandidateDependenceAnalyser {
- private const int COARSE_STAGES = 1;
- private const int FINE_STAGES = 2;
- private const int BALANCED_STAGES = 3;
+ private const string COARSE_STAGES = "COARSE";
+ private const string FINE_STAGES = "FINE";
+ private const string BALANCED_STAGES = "BALANCED";
private Program prog;
private IVariableDependenceAnalyser varDepAnalyser;
@@ -22,6 +22,7 @@ namespace Microsoft.Boogie { private Graph<string> CandidateDependences;
private StronglyConnectedComponents<string> SCCs;
private Graph<SCC<string>> StagesDAG;
+ private StagedHoudiniPlan Plan;
public CandidateDependenceAnalyser(Program prog) {
this.prog = prog;
@@ -193,7 +194,7 @@ namespace Microsoft.Boogie { if (p != null)
{
string c;
- if(Houdini.Houdini.MatchCandidate(p.Expr, candidates, out c)) {
+ if(Houdini.MatchCandidate(p.Expr, candidates, out c)) {
yield return new CandidateInstance(c, impl.Name, p.Expr);
}
}
@@ -206,14 +207,14 @@ namespace Microsoft.Boogie { foreach (Requires r in proc.Requires)
{
string c;
- if(Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) {
+ if(Houdini.MatchCandidate(r.Condition, candidates, out c)) {
yield return new CandidateInstance(c, proc.Name, r.Condition);
}
}
foreach (Ensures e in proc.Ensures)
{
string c;
- if(Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) {
+ if(Houdini.MatchCandidate(e.Condition, candidates, out c)) {
yield return new CandidateInstance(c, proc.Name, e.Condition);
}
}
@@ -355,35 +356,33 @@ namespace Microsoft.Boogie { }
- public void ApplyStages() {
+ public StagedHoudiniPlan ApplyStages() {
if (NoStages())
{
- return;
+ return null;
}
#region Assign candidates to stages at a given level of granularity
-
- Dictionary<string, int> candidateToStage;
switch(CommandLineOptions.Clo.StagedHoudini) {
case COARSE_STAGES:
- candidateToStage = ComputeCoarseStages();
+ Plan = ComputeCoarseStages();
break;
case FINE_STAGES:
- candidateToStage = ComputeFineStages();
+ Plan = ComputeFineStages();
break;
case BALANCED_STAGES:
- candidateToStage = ComputeBalancedStages();
+ Plan = ComputeBalancedStages();
break;
default:
Debug.Assert(false);
- candidateToStage = null;
+ Plan = null;
break;
}
foreach(var c in candidates) {
- Debug.Assert(candidateToStage.ContainsKey(c));
+ Debug.Assert(Plan.StageForCandidate(c) != null);
}
#endregion
@@ -391,21 +390,21 @@ namespace Microsoft.Boogie { var stageToActiveBoolean = new Dictionary<int, Constant>();
var stageToCompleteBoolean = new Dictionary<int, Constant>();
- foreach (var stage in new HashSet<int>(candidateToStage.Values))
+ foreach (var stage in Plan)
{
var stageActive = new Constant(Token.NoToken,
- new TypedIdent(Token.NoToken, "_stage_" + stage + "_active", Type.Bool),
+ new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_active", Type.Bool),
false);
- stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage)) });
+ stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });
prog.TopLevelDeclarations.Add(stageActive);
- stageToActiveBoolean[stage] = stageActive;
+ stageToActiveBoolean[stage.GetId()] = stageActive;
var stageComplete = new Constant(Token.NoToken,
- new TypedIdent(Token.NoToken, "_stage_" + stage + "_complete", Type.Bool),
+ new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_complete", Type.Bool),
false);
- stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage)) });
+ stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });
prog.TopLevelDeclarations.Add(stageComplete);
- stageToCompleteBoolean[stage] = stageComplete;
+ stageToCompleteBoolean[stage.GetId()] = stageComplete;
}
#endregion
@@ -417,12 +416,12 @@ namespace Microsoft.Boogie { {
var a = cmd as AssertCmd;
string c;
- if (a != null && (Houdini.Houdini.MatchCandidate(a.Expr, candidates, out c)))
+ if (a != null && (Houdini.MatchCandidate(a.Expr, candidates, out c)))
{
- newCmds.Add(new AssertCmd(a.tok, Houdini.Houdini.AddConditionToCandidate(a.Expr,
- new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c), a.Attributes));
- newCmds.Add(new AssumeCmd(a.tok, Houdini.Houdini.AddConditionToCandidate(a.Expr,
- new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c), a.Attributes));
+ newCmds.Add(new AssertCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr,
+ new IdentifierExpr(Token.NoToken, stageToActiveBoolean[Plan.StageForCandidate(c).GetId()]), c), a.Attributes));
+ newCmds.Add(new AssumeCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr,
+ new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c), a.Attributes));
}
else
{
@@ -441,14 +440,14 @@ namespace Microsoft.Boogie { RequiresSeq newRequires = new RequiresSeq();
foreach(Requires r in p.Requires) {
string c;
- if (Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) {
+ if (Houdini.MatchCandidate(r.Condition, candidates, out c)) {
newRequires.Add(new Requires(r.tok, false,
- Houdini.Houdini.AddConditionToCandidate(r.Condition,
- new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c),
+ Houdini.AddConditionToCandidate(r.Condition,
+ new IdentifierExpr(Token.NoToken, stageToActiveBoolean[Plan.StageForCandidate(c).GetId()]), c),
r.Comment, r.Attributes));
newRequires.Add(new Requires(r.tok, true,
- Houdini.Houdini.AddConditionToCandidate(r.Condition,
- new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c),
+ Houdini.AddConditionToCandidate(r.Condition,
+ new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c),
r.Comment, r.Attributes));
} else {
newRequires.Add(r);
@@ -461,16 +460,16 @@ namespace Microsoft.Boogie { EnsuresSeq newEnsures = new EnsuresSeq();
foreach(Ensures e in p.Ensures) {
string c;
- if (Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) {
- int stage = candidateToStage[c];
+ if (Houdini.MatchCandidate(e.Condition, candidates, out c)) {
+ int stage = Plan.StageForCandidate(c).GetId();
Constant activeBoolean = stageToActiveBoolean[stage];
newEnsures.Add(new Ensures(e.tok, false,
- Houdini.Houdini.AddConditionToCandidate(e.Condition,
+ Houdini.AddConditionToCandidate(e.Condition,
new IdentifierExpr(Token.NoToken, activeBoolean), c),
e.Comment, e.Attributes));
newEnsures.Add(new Ensures(e.tok, true,
- Houdini.Houdini.AddConditionToCandidate(e.Condition,
- new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c),
+ Houdini.AddConditionToCandidate(e.Condition,
+ new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[stage]), c),
e.Comment, e.Attributes));
} else {
newEnsures.Add(e);
@@ -482,6 +481,8 @@ namespace Microsoft.Boogie { }
#endregion
+ return Plan;
+
}
private int FindLargestStage() {
@@ -489,78 +490,110 @@ namespace Microsoft.Boogie { }
- private Dictionary<string, int> ComputeCoarseStages()
+ private StagedHoudiniPlan ComputeCoarseStages()
{
- var result = new Dictionary<string, int>();
- HashSet<SCC<string>> done = new HashSet<SCC<string>> { GetStartNodeOfStagesDAG() };
- for(int stageId = 0; done.Count() != StagesDAG.Nodes.Count(); stageId++)
+ foreach(var n in StagesDAG.Nodes) {
+ Debug.Assert(!StagesDAG.Successors(n).Contains(n));
+ }
+
+ Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();
+
+ var done = new Dictionary<SCC<string>, ScheduledStage>();
+ done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());
+
+ for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)
{
- foreach (var n in StagesDAG.Nodes.Where(Item => !done.Contains(Item)))
+ var Stage = new ScheduledStage(stageId, new HashSet<string>());
+ HashSet<SCC<string>> AssignedToThisStage = new HashSet<SCC<string>>();
+
+ foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))
{
- if(StagesDAG.Successors(n).Where(Item => !done.Contains(Item)).Count() == 0) {
+ if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) {
+ foreach(var s in StagesDAG.Successors(n)) {
+ Debug.Assert(s != n);
+ Debug.Assert(Stage != done[s]);
+ Dependences.AddEdge(Stage, done[s]);
+ }
foreach (var c in n)
{
- result[c] = stageId;
+ Stage.AddCandidate(c);
}
- done.Add(n);
+ Console.Write(n.Count() + ", ");
+ AssignedToThisStage.Add(n);
}
}
+
+ Console.WriteLine("total: " + Stage.Count());
+
+ foreach(var n in AssignedToThisStage) {
+ done[n] = Stage;
+ }
}
- return result;
+ return new StagedHoudiniPlan(Dependences);
}
- private Dictionary<string, int> ComputeBalancedStages()
+ private StagedHoudiniPlan ComputeBalancedStages()
{
- int maxStageSize = 200;
- var result = new Dictionary<string, int>();
- HashSet<SCC<string>> done = new HashSet<SCC<string>> { GetStartNodeOfStagesDAG() };
- for(int stageId = 0; done.Count() != StagesDAG.Nodes.Count(); stageId++)
+ Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();
+ var done = new Dictionary<SCC<string>, ScheduledStage>();
+ done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());
+
+ int maxStageSize = 200;
+
+ for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)
+ {
+ int stageSize = 0;
+ ScheduledStage Stage = new ScheduledStage(stageId, new HashSet<string>());
+ HashSet<SCC<string>> AddedToThisStage = new HashSet<SCC<string>>();
+
+ foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))
{
- int stageSize = 0;
- foreach (var n in StagesDAG.Nodes.Where(Item => !done.Contains(Item)))
- {
- if(stageSize + n.Count() > maxStageSize) {
- continue;
+ if(stageSize + n.Count() > maxStageSize) {
+ continue;
+ }
+ if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) {
+ foreach (var c in n)
+ {
+ Stage.AddCandidate(c);
+ stageSize++;
}
- if(StagesDAG.Successors(n).Where(Item => !done.Contains(Item)).Count() == 0) {
- foreach (var c in n)
- {
- result[c] = stageId;
- stageSize++;
- }
- done.Add(n);
+ foreach(var s in StagesDAG.Successors(n)) {
+ Dependences.AddEdge(Stage, done[s]);
}
+ AddedToThisStage.Add(n);
}
- if(stageSize == 0) {
- maxStageSize *= 2;
- }
}
- return result;
+ foreach(var n in AddedToThisStage) {
+ done[n] = Stage;
+ }
+ if(stageSize == 0) {
+ maxStageSize *= 2;
+ }
+ }
+ return new StagedHoudiniPlan(Dependences);
}
- private Dictionary<string, int> ComputeFineStages()
+ private StagedHoudiniPlan ComputeFineStages()
{
-
- var result = new Dictionary<string, int>();
- List<SCC<string>> components = StagesDAG.TopologicalSort().ToList();
- components.Reverse();
+ Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();
+ var done = new Dictionary<SCC<string>, ScheduledStage>();
- System.Diagnostics.Debug.Assert(components[0].Count() == 0);
- for (int i = 1; i < components.Count(); i++)
- {
- foreach (var c in components[i])
- {
- result[c] = i - 1;
- }
+ List<SCC<string>> components = StagesDAG.TopologicalSort().ToList();
+ components.Reverse();
+ for (int i = 0; i < components.Count(); i++)
+ {
+ ScheduledStage Stage = new ScheduledStage(i, new HashSet<string>());
+ done[components[i]] = Stage;
+ foreach (var c in components[i])
+ {
+ Stage.AddCandidate(c);
}
-
- foreach(var c in candidates) {
- Debug.Assert(result.ContainsKey(c));
+ foreach(var s in StagesDAG.Successors(components[i])) {
+ Dependences.AddEdge(Stage, done[s]);
}
-
- return result;
-
+ }
+ return new StagedHoudiniPlan(Dependences);
}
private SCC<string> GetStartNodeOfStagesDAG()
@@ -608,7 +641,7 @@ namespace Microsoft.Boogie { AssertCmd assertCmd = cmd as AssertCmd;
if(assertCmd != null) {
string c;
- if(Houdini.Houdini.MatchCandidate(assertCmd.Expr, candidates, out c)) {
+ if(Houdini.MatchCandidate(assertCmd.Expr, candidates, out c)) {
AddCandidateOccurrence(c, b);
}
}
@@ -619,7 +652,7 @@ namespace Microsoft.Boogie { foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
foreach(Requires r in proc.Requires) {
string c;
- if(Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) {
+ if(Houdini.MatchCandidate(r.Condition, candidates, out c)) {
AddCandidateOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));
}
}
@@ -629,7 +662,7 @@ namespace Microsoft.Boogie { foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
foreach(Ensures e in proc.Ensures) {
string c;
- if(Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) {
+ if(Houdini.MatchCandidate(e.Condition, candidates, out c)) {
AddCandidateOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.POST));
}
}
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index a64cece0..b29aa933 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -94,14 +94,20 @@ namespace Microsoft.Boogie.Houdini { }
}
+
+
public class HoudiniSession {
- public static double proverTime = 0;
- public static int numProverQueries = 0;
- public static double unsatCoreProverTime = 0;
- public static int numUnsatCoreProverQueries = 0;
- public static int numUnsatCorePrunings = 0;
+
+ public class HoudiniStatistics {
+ public double proverTime = 0;
+ public int numProverQueries = 0;
+ public double unsatCoreProverTime = 0;
+ public int numUnsatCoreProverQueries = 0;
+ public int numUnsatCorePrunings = 0;
+ }
public string descriptiveName;
+ public HoudiniStatistics stats;
private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
ConditionGeneration.CounterexampleCollector collector;
@@ -115,20 +121,18 @@ namespace Microsoft.Boogie.Houdini { private HashSet<Variable> explainConstantsNegative;
private Dictionary<string, Tuple<Variable, Variable>> constantToControl;
- Houdini houdini;
- Implementation implementation;
-
public bool InUnsatCore(Variable constant) {
if (unsatCoreSet == null)
return true;
if (unsatCoreSet.Contains(constant))
return true;
- numUnsatCorePrunings++;
+ stats.numUnsatCorePrunings++;
return false;
}
- public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl) {
- descriptiveName = impl.Name;
+ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats) {
+ this.descriptiveName = impl.Name;
+ this.stats = stats;
collector = new ConditionGeneration.CounterexampleCollector();
collector.OnProgress("HdnVCGen", 0, 0, 0.0);
@@ -170,8 +174,6 @@ namespace Microsoft.Boogie.Houdini { handler = new VCGen.ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, vcgen.incarnationOriginMap, collector, mvInfo, proverInterface.Context, program);
}
- this.houdini = houdini;
- this.implementation = impl;
}
private VCExpr BuildAxiom(ProverInterface proverInterface, Dictionary<Variable, bool> currentAssignment) {
@@ -213,6 +215,10 @@ namespace Microsoft.Boogie.Houdini { }
*/
+ if(CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Houdini assignment axiom: " + expr);
+ }
+
return expr;
}
@@ -229,8 +235,8 @@ namespace Microsoft.Boogie.Houdini { ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);
double queryTime = (DateTime.UtcNow - now).TotalSeconds;
- proverTime += queryTime;
- numProverQueries++;
+ stats.proverTime += queryTime;
+ stats.numProverQueries++;
if (CommandLineOptions.Clo.Trace) {
Console.WriteLine("Time taken = " + queryTime);
}
@@ -387,20 +393,20 @@ namespace Microsoft.Boogie.Houdini { }
foreach (var r in reason)
{
- Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, implementation.Name);
+ Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, descriptiveName);
}
} while (false);
if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)
{
- Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", implementation.Name);
+ Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, "TimeOut", descriptiveName);
}
CommandLineOptions.Clo.ProverCCLimit = el;
double queryTime = (DateTime.UtcNow - now).TotalSeconds;
- proverTime += queryTime;
- numProverQueries++;
+ stats.proverTime += queryTime;
+ stats.numProverQueries++;
if (CommandLineOptions.Clo.Trace)
{
Console.WriteLine("Time taken = " + queryTime);
@@ -434,8 +440,8 @@ namespace Microsoft.Boogie.Houdini { proverInterface.Pop();
double unsatCoreQueryTime = (DateTime.UtcNow - now).TotalSeconds;
- unsatCoreProverTime += unsatCoreQueryTime;
- numUnsatCoreProverQueries++;
+ stats.unsatCoreProverTime += unsatCoreQueryTime;
+ stats.numUnsatCoreProverQueries++;
}
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index abc5a7e8..a91c0082 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -38,7 +38,6 @@ namespace Microsoft.Boogie.Houdini { public abstract class HoudiniObserver {
public virtual void UpdateStart(Program program, int numConstants) { }
- public virtual void UpdateStage(int stage) { }
public virtual void UpdateIteration() { }
public virtual void UpdateImplementation(Implementation implementation) { }
public virtual void UpdateAssignment(Dictionary<Variable, bool> assignment) { }
@@ -133,10 +132,6 @@ namespace Microsoft.Boogie.Houdini { currentIteration = -1;
wr.Flush();
}
- public override void UpdateStage(int stage) {
- wr.WriteLine("Houdini stage " + stage);
- wr.Flush();
- }
public override void UpdateIteration() {
currentIteration++;
wr.WriteLine("---------------------------------------");
@@ -215,9 +210,6 @@ namespace Microsoft.Boogie.Houdini { NotifyDelegate notifyDelegate = (NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStart(program, numConstants); };
Notify(notifyDelegate);
}
- protected void NotifyStage(int stage) {
- Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateStage(stage); });
- }
protected void NotifyIteration() {
Notify((NotifyDelegate)delegate(HoudiniObserver r) { r.UpdateIteration(); });
}
@@ -323,12 +315,15 @@ namespace Microsoft.Boogie.Houdini { private HoudiniState currentHoudiniState;
private CrossDependencies crossDependencies;
+ private string cexTraceFile;
+
public HoudiniState CurrentHoudiniState { get { return currentHoudiniState; } }
public static TextWriter explainHoudiniDottyFile;
- public Houdini(Program program) {
+ public Houdini(Program program, HoudiniSession.HoudiniStatistics stats, string cexTraceFile = "houdiniCexTrace.bpl") {
this.program = program;
+ this.cexTraceFile = cexTraceFile;
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Collecting existential constants...");
@@ -360,7 +355,7 @@ namespace Microsoft.Boogie.Houdini { try {
if (CommandLineOptions.Clo.Trace)
Console.WriteLine("Generating VC for {0}", impl.Name);
- HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl);
+ HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats);
houdiniSessions.Add(impl, session);
}
catch (VCGenException) {
@@ -370,7 +365,6 @@ namespace Microsoft.Boogie.Houdini { }
}
this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
- currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));
if (CommandLineOptions.Clo.ExplainHoudini)
{
@@ -683,7 +677,7 @@ namespace Microsoft.Boogie.Houdini { return nonCandidateErrors.Count > 0;
}
- private void FlushWorkList() {
+ private void FlushWorkList(int stage, IEnumerable<int> completedStages) {
this.NotifyFlushStart();
while (currentHoudiniState.WorkQueue.Count > 0) {
this.NotifyIteration();
@@ -694,7 +688,7 @@ namespace Microsoft.Boogie.Houdini { HoudiniSession session;
houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session);
List<Counterexample> errors;
- ProverInterface.Outcome outcome = TryCatchVerify(session, out errors);
+ ProverInterface.Outcome outcome = TryCatchVerify(session, stage, completedStages, out errors);
UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors);
this.NotifyOutcome(outcome);
@@ -707,7 +701,7 @@ namespace Microsoft.Boogie.Houdini { private void UpdateAssignment(RefutedAnnotation refAnnot) {
if (CommandLineOptions.Clo.Trace) {
Console.WriteLine("Removing " + refAnnot.Constant);
- using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))
+ using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true))
cexWriter.WriteLine("Removing " + refAnnot.Constant);
}
currentHoudiniState.Assignment.Remove(refAnnot.Constant);
@@ -750,7 +744,7 @@ namespace Microsoft.Boogie.Houdini { #region Extra debugging output
if (CommandLineOptions.Clo.Trace)
{
- using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))
+ using (var cexWriter = new System.IO.StreamWriter(cexTraceFile, true))
{
cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);
cexWriter.Write(error.ToString());
@@ -820,17 +814,15 @@ namespace Microsoft.Boogie.Houdini { }
public class HoudiniState {
- private WorkQueue _workQueue;
- private HashSet<string> blackList;
- private Dictionary<Variable, bool> _assignment;
- private int _stage;
- private Implementation _implementation;
- private HoudiniOutcome _outcome;
+ public WorkQueue _workQueue;
+ public HashSet<string> blackList;
+ public Dictionary<Variable, bool> _assignment;
+ public Implementation _implementation;
+ public HoudiniOutcome _outcome;
public HoudiniState(WorkQueue workQueue, Dictionary<Variable, bool> currentAssignment) {
this._workQueue = workQueue;
this._assignment = currentAssignment;
- this._stage = 0;
this._implementation = null;
this._outcome = new HoudiniOutcome();
this.blackList = new HashSet<string>();
@@ -842,9 +834,6 @@ namespace Microsoft.Boogie.Houdini { public Dictionary<Variable, bool> Assignment {
get { return this._assignment; }
}
- public int Stage {
- get { return this._stage; }
- }
public Implementation Implementation {
get { return this._implementation; }
set { this._implementation = value; }
@@ -858,53 +847,45 @@ namespace Microsoft.Boogie.Houdini { public void addToBlackList(string funcName) {
blackList.Add(funcName);
}
- internal void incrementStage() {
- _stage++;
- }
}
- public HoudiniOutcome PerformHoudiniInference() {
+ public HoudiniOutcome PerformHoudiniInference(int stage = 0,
+ IEnumerable<int> completedStages = null,
+ Dictionary<string, bool> initialAssignment = null) {
this.NotifyStart(program, houdiniConstants.Count);
- foreach (Implementation impl in vcgenFailures) {
- currentHoudiniState.addToBlackList(impl.Name);
- }
- while(currentHoudiniState.Stage < NumberOfStages()) {
+ currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));
- if (CommandLineOptions.Clo.Trace) {
- Console.WriteLine("Current stage is " + currentHoudiniState.Stage + " of " + (NumberOfStages() - 1));
+ if(initialAssignment != null) {
+ foreach(var v in CurrentHoudiniState.Assignment.Keys.ToList()) {
+ CurrentHoudiniState.Assignment[v] = initialAssignment[v.Name];
}
+ }
- this.NotifyStage(currentHoudiniState.Stage);
-
- while (currentHoudiniState.WorkQueue.Count > 0) {
- this.NotifyIteration();
-
- currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek();
- this.NotifyImplementation(currentHoudiniState.Implementation);
-
- HoudiniSession session;
- this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session);
- HoudiniVerifyCurrent(session);
- }
+ foreach (Implementation impl in vcgenFailures) {
+ currentHoudiniState.addToBlackList(impl.Name);
+ }
- currentHoudiniState.incrementStage();
+ while (currentHoudiniState.WorkQueue.Count > 0) {
+ this.NotifyIteration();
- #region Re-populate work list for next stage
- if (currentHoudiniState.Stage < NumberOfStages()) {
- var workList = BuildWorkList(program);
- while(workList.Count > 0) {
- currentHoudiniState.WorkQueue.Enqueue(workList.Dequeue());
- }
- }
- #endregion
+ currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek();
+ this.NotifyImplementation(currentHoudiniState.Implementation);
+ HoudiniSession session;
+ this.houdiniSessions.TryGetValue(currentHoudiniState.Implementation, out session);
+ HoudiniVerifyCurrent(session, stage, completedStages);
}
+
this.NotifyEnd(true);
Dictionary<string, bool> assignment = new Dictionary<string, bool>();
foreach (var x in currentHoudiniState.Assignment)
assignment[x.Key.Name] = x.Value;
currentHoudiniState.Outcome.assignment = assignment;
+ return currentHoudiniState.Outcome;
+ }
+
+ public void Close() {
vcgen.Close();
proverInterface.Close();
if (CommandLineOptions.Clo.ExplainHoudini)
@@ -912,7 +893,6 @@ namespace Microsoft.Boogie.Houdini { explainHoudiniDottyFile.WriteLine("};");
explainHoudiniDottyFile.Close();
}
- return currentHoudiniState.Outcome;
}
private int NumberOfStages()
@@ -1067,10 +1047,10 @@ namespace Microsoft.Boogie.Houdini { return null;
}
- private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, out List<Counterexample> errors) {
+ private ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
ProverInterface.Outcome outcome;
try {
- outcome = session.Verify(proverInterface, GetAssignmentWithStages(), out errors);
+ outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors);
}
catch (UnexpectedProverOutputException upo) {
Contract.Assume(upo != null);
@@ -1080,7 +1060,7 @@ namespace Microsoft.Boogie.Houdini { return outcome;
}
- private Dictionary<Variable, bool> GetAssignmentWithStages()
+ private Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)
{
Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);
foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
@@ -1088,24 +1068,24 @@ namespace Microsoft.Boogie.Houdini { int stageActive = QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1);
if (stageActive != -1)
{
- result[c] = (stageActive == currentHoudiniState.Stage);
+ result[c] = (stageActive == currentStage);
}
int stageComplete = QKeyValue.FindIntAttribute(c.Attributes, "stage_complete", -1);
if (stageComplete != -1)
{
- result[c] = (stageComplete < currentHoudiniState.Stage);
+ result[c] = (completedStages.Contains(stageComplete));
}
}
return result;
}
- private void HoudiniVerifyCurrent(HoudiniSession session) {
+ private void HoudiniVerifyCurrent(HoudiniSession session, int stage, IEnumerable<int> completedStages) {
while (true) {
this.NotifyAssignment(currentHoudiniState.Assignment);
//check the VC with the current assignment
List<Counterexample> errors;
- ProverInterface.Outcome outcome = TryCatchVerify(session, out errors);
+ ProverInterface.Outcome outcome = TryCatchVerify(session, stage, completedStages, out errors);
this.NotifyOutcome(outcome);
DebugRefutedCandidates(currentHoudiniState.Implementation, errors);
@@ -1133,7 +1113,7 @@ namespace Microsoft.Boogie.Houdini { if (UpdateHoudiniOutcome(currentHoudiniState.Outcome, currentHoudiniState.Implementation, outcome, errors)) { // abort
currentHoudiniState.WorkQueue.Dequeue();
this.NotifyDequeue();
- FlushWorkList();
+ FlushWorkList(stage, completedStages);
return;
}
else if (UpdateAssignmentWorkList(outcome, errors)) {
diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index e4840d1d..6c98c2a8 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -84,6 +84,7 @@ <Compile Include="Checker.cs" />
<Compile Include="CandidateDependenceAnalyser.cs" />
<Compile Include="Houdini.cs" />
+ <Compile Include="StagedHoudini.cs" />
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs new file mode 100644 index 00000000..39915f7f --- /dev/null +++ b/Source/Houdini/StagedHoudini.cs @@ -0,0 +1,348 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+using System.Threading.Tasks;
+using System.Threading;
+using Microsoft.Boogie;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie.Houdini
+{
+ public class StagedHoudini
+ {
+
+ private Program program;
+ private Func<string, Program> ProgramFromFile;
+ private StagedHoudiniPlan plan;
+ private List<Houdini>[] houdiniInstances;
+ private List<StagedHoudiniTask> tasks = new List<StagedHoudiniTask>();
+ private Dictionary<ScheduledStage, HoudiniOutcome> outcomes = new Dictionary<ScheduledStage,HoudiniOutcome>();
+
+ private const string tempFilename = "__stagedHoudiniTemp.bpl";
+
+ public StagedHoudini(Program program, Func<string, Program> ProgramFromFile) {
+ this.program = program;
+ this.ProgramFromFile = ProgramFromFile;
+ this.houdiniInstances = new List<Houdini>[CommandLineOptions.Clo.StagedHoudiniThreads];
+ for (int i = 0; i < CommandLineOptions.Clo.StagedHoudiniThreads; i++) {
+ houdiniInstances[i] = new List<Houdini>();
+ }
+
+ var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program);
+ candidateDependenceAnalyser.Analyse();
+ this.plan = candidateDependenceAnalyser.ApplyStages();
+ if (CommandLineOptions.Clo.Trace)
+ {
+ candidateDependenceAnalyser.dump();
+ EmitProgram("staged.bpl");
+ }
+ }
+
+ public HoudiniOutcome PerformStagedHoudiniInference()
+ {
+
+ EmitProgram(tempFilename);
+
+ #region Prepare the tasks, but do not launch them
+ foreach (var s in plan) {
+ Debug.Assert(!plan.GetDependences(s).Contains(s));
+ tasks.Add(new StagedHoudiniTask(s, new Task(() => {
+ ExecuteStage(s);
+ }, TaskCreationOptions.LongRunning)));
+ }
+ #endregion
+
+ #region Launch the tasks, and wait for them to finish
+ foreach (var t in tasks) {
+ t.parallelTask.Start();
+ }
+ Task.WaitAll(tasks.Select(Item => Item.parallelTask).ToArray());
+ int count = 0;
+ foreach(var h in houdiniInstances) {
+ if(h.Count() > 0) {
+ count++;
+ System.Diagnostics.Debug.Assert(h.Count() == 1);
+ h[0].Close();
+ }
+ }
+ Console.WriteLine("Used " + count + " houdini instances");
+ #endregion
+
+ return UnifyOutcomes();
+
+ }
+
+ private HoudiniOutcome UnifyOutcomes()
+ {
+ HoudiniOutcome result = new HoudiniOutcome();
+ var scheduledStages = outcomes.Keys.ToList();
+
+ result.assignment = new Dictionary<string,bool>();
+ foreach(var c in outcomes[scheduledStages[0]].assignment.Keys) {
+ result.assignment[c] = outcomes.Select(Item => Item.Value).Select(Item => Item.assignment[c]).All(Item => Item);
+ }
+
+ result.implementationOutcomes = new Dictionary<string,VCGenOutcome>();
+ foreach(var p in outcomes[scheduledStages[0]].implementationOutcomes.Keys) {
+ var unifiedImplementationOutcome = outcomes[scheduledStages[0]].implementationOutcomes[p];
+ for(int i = 1; i < scheduledStages.Count(); i++) {
+ unifiedImplementationOutcome = ChooseOutcome(unifiedImplementationOutcome,
+ outcomes[scheduledStages[i]].implementationOutcomes[p]);
+ }
+ result.implementationOutcomes[p] = unifiedImplementationOutcome;
+ }
+
+ return result;
+ }
+
+ private void ExecuteStage(ScheduledStage s)
+ {
+ Task.WaitAll(tasks.Where(
+ Item => plan.GetDependences(s).Contains(Item.stage)).
+ Select(Item => Item.parallelTask).ToArray());
+
+ List<Houdini> h = AcquireHoudiniInstance();
+
+ if (h.Count() == 0)
+ {
+ h.Add(new Houdini(ProgramFromFile(tempFilename), new HoudiniSession.HoudiniStatistics(), "houdiniCexTrace_" + s.GetId() + ".bpl"));
+ }
+
+ System.Diagnostics.Debug.Assert(h.Count() == 1);
+
+ Dictionary<string, bool> mergedAssignment = null;
+
+ List<Dictionary<string, bool>> relevantAssignments;
+ IEnumerable<int> completedStages;
+ lock (outcomes)
+ {
+ relevantAssignments =
+ outcomes.Where(Item => plan.Contains(Item.Key)).
+ Select(Item => Item.Value).
+ Select(Item => Item.assignment).ToList();
+ //outcomes.Values.Select(Item => Item.assignment).ToList();
+ completedStages = plan.GetDependences(s).Select(Item => Item.GetId());
+ //completedStages = outcomes.Keys.Select(Item => Item.GetId());
+ }
+
+ if (relevantAssignments.Count() > 0)
+ {
+ mergedAssignment = new Dictionary<string, bool>();
+ foreach (var v in relevantAssignments[0].Keys)
+ {
+ mergedAssignment[v] = relevantAssignments.Select(Item => Item[v]).ToList().All(Item => Item);
+ }
+ }
+
+ HoudiniOutcome outcome = h[0].PerformHoudiniInference(
+ s.GetId(),
+ completedStages,
+ mergedAssignment);
+
+ lock (outcomes)
+ {
+ outcomes[s] = outcome;
+ }
+
+ ReleaseHoudiniInstance(h);
+
+ }
+
+ private static void ReleaseHoudiniInstance(List<Houdini> h)
+ {
+ Monitor.Exit(h);
+ }
+
+ private List<Houdini> AcquireHoudiniInstance()
+ {
+ List<Houdini> h = null;
+ do
+ {
+ foreach (var houdini in houdiniInstances)
+ {
+ if (Monitor.TryEnter(houdini))
+ {
+ h = houdini;
+ break;
+ }
+ else
+ {
+ Thread.Sleep(20);
+ }
+ }
+ } while (h == null);
+ return h;
+ }
+
+ private void EmitProgram(string filename)
+ {
+ using (TokenTextWriter writer = new TokenTextWriter(filename, true))
+ {
+ int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintUnstructured = 2;
+ program.Emit(writer);
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
+ }
+
+
+ private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2) {
+ var vcOutcome1 = o1.outcome;
+ var vcOutcome2 = o2.outcome;
+
+ if(vcOutcome1 == vcOutcome2) {
+ return o1;
+ }
+
+ // Errors trump everything else
+ if(vcOutcome1 == VC.ConditionGeneration.Outcome.Errors) {
+ return o1;
+ }
+ if(vcOutcome2 == VC.ConditionGeneration.Outcome.Errors) {
+ return o2;
+ }
+
+ // If one outcome is Correct, return the other in case it is "worse"
+ if(vcOutcome1 == VC.ConditionGeneration.Outcome.Correct) {
+ return o2;
+ }
+ if(vcOutcome2 == VC.ConditionGeneration.Outcome.Correct) {
+ return o1;
+ }
+
+ // Neither outcome is correct, so if one outcome is ReachedBound, return the other in case it is "worse"
+ if(vcOutcome1 == VC.ConditionGeneration.Outcome.ReachedBound) {
+ return o2;
+ }
+ if(vcOutcome2 == VC.ConditionGeneration.Outcome.ReachedBound) {
+ return o1;
+ }
+
+ // Both outcomes must be timeout or memout; arbitrarily choose the first
+ return o1;
+ }
+
+ internal class StagedHoudiniTask {
+ internal ScheduledStage stage;
+ internal Task parallelTask;
+ internal StagedHoudiniTask(ScheduledStage stage, Task parallelTask) {
+ this.stage = stage;
+ this.parallelTask = parallelTask;
+ }
+ }
+
+ }
+
+ public class StagedHoudiniPlan : IEnumerable<ScheduledStage> {
+
+ private Graph<ScheduledStage> ScheduledStages;
+ private Dictionary<string, ScheduledStage> CandidateToStage;
+
+ internal StagedHoudiniPlan(Graph<ScheduledStage> ScheduledStages) {
+ this.ScheduledStages = ScheduledStages;
+ this.CandidateToStage = new Dictionary<string, ScheduledStage>();
+ foreach(var s in this) {
+ Debug.Assert(!GetDependences(s).Contains(s));
+ }
+ }
+
+ public IEnumerable<ScheduledStage> GetDependences(ScheduledStage s) {
+ IEnumerable<ScheduledStage> result;
+ lock(ScheduledStages) {
+ result = ScheduledStages.Successors(s);
+ }
+ return result;
+ }
+
+
+ private static int CompareStages(ScheduledStage s1, ScheduledStage s2) {
+ if(s1.GetId() < s2.GetId()) {
+ return -1;
+ }
+ if(s2.GetId() < s1.GetId()) {
+ return 1;
+ }
+ return 0;
+ }
+
+ public IEnumerator<ScheduledStage> GetEnumerator() {
+ List<ScheduledStage> sortedStages = ScheduledStages.Nodes.ToList();
+ sortedStages.Sort(CompareStages);
+ return sortedStages.GetEnumerator();
+ }
+
+ System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator()
+ {
+ return this.GetEnumerator();
+ }
+
+ internal ScheduledStage StageForCandidate(string c) {
+ if(CandidateToStage.ContainsKey(c)) {
+ return CandidateToStage[c];
+ }
+ foreach(var s in ScheduledStages.Nodes) {
+ if(s.ContainsCandidate(c)) {
+ CandidateToStage[c] = s;
+ return s;
+ }
+ }
+ return null;
+ }
+
+ public override string ToString()
+ {
+ string result = "";
+ foreach(ScheduledStage s in this) {
+ result += "Stage " + s;
+
+ result += " depends on stages: ";
+ foreach(var id in GetDependences(s).Select(Item => Item.GetId())) {
+ result += id + " ";
+ }
+ result += "\n";
+ }
+ return result;
+ }
+ }
+
+ public class ScheduledStage {
+ private int Id;
+ private HashSet<string> Candidates;
+
+ public ScheduledStage(int Id, HashSet<string> Candidates) {
+ this.Id = Id;
+ this.Candidates = Candidates;
+ }
+
+ internal void AddCandidate(string c) {
+ Candidates.Add(c);
+ }
+
+ internal bool ContainsCandidate(string c) {
+ return Candidates.Contains(c);
+ }
+
+ public int GetId() {
+ return Id;
+ }
+
+ public int Count() {
+ return Candidates.Count();
+ }
+
+ public override string ToString()
+ {
+ string result = "ID: " + Id + "{ ";
+ foreach(var c in Candidates) {
+ result += c + " ";
+ }
+ result += "}\n";
+ return result;
+ }
+ }
+
+
+}
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs index 09dce05f..bd01cc16 100644 --- a/Source/ModelViewer/Main.cs +++ b/Source/ModelViewer/Main.cs @@ -10,6 +10,7 @@ using System.Windows.Forms; using System.IO;
using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
namespace Microsoft.Boogie.ModelViewer
{
@@ -92,6 +93,18 @@ namespace Microsoft.Boogie.ModelViewer }
}
+ public void ReadModel(string model, int setModelIdTo = 0)
+ {
+ Contract.Requires(model != null);
+
+ using (var rd = new StringReader(model))
+ {
+ allModels = Model.ParseModels(rd).ToArray();
+ }
+
+ AddAndLoadModel(setModelIdTo);
+ }
+
public void ReadModels(string modelFileName, int setModelIdTo)
{
this.lastModelFileName = modelFileName;
@@ -102,28 +115,34 @@ namespace Microsoft.Boogie.ModelViewer allModels = Model.ParseModels(rd,"").ToArray();
}
- modelId = setModelIdTo;
-
- if (modelId >= allModels.Length)
- modelId = 0;
-
- currentModel = allModels[modelId];
- AddModelMenu();
-
- foreach (var p in Providers()) {
- if (p.IsMyModel(currentModel)) {
- this.langProvider = p;
- break;
- }
- }
-
- LoadModel(modelId);
+ AddAndLoadModel(setModelIdTo);
} else {
currentModel = new Model();
}
this.SetWindowTitle(modelFileName);
+ }
+
+ private void AddAndLoadModel(int setModelIdTo)
+ {
+ modelId = setModelIdTo;
+
+ if (modelId >= allModels.Length)
+ modelId = 0;
+
+ currentModel = allModels[modelId];
+ AddModelMenu();
+
+ foreach (var p in Providers())
+ {
+ if (p.IsMyModel(currentModel))
+ {
+ this.langProvider = p;
+ break;
+ }
+ }
+ LoadModel(modelId);
}
private void LoadModel(int idx)
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj index 49965d5e..75e5521c 100644 --- a/Source/ModelViewer/ModelViewer.csproj +++ b/Source/ModelViewer/ModelViewer.csproj @@ -6,10 +6,10 @@ <ProductVersion>8.0.30703</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}</ProjectGuid>
- <OutputType>WinExe</OutputType>
+ <OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>
- <AssemblyName>BVD</AssemblyName>
+ <AssemblyName>ModelViewer</AssemblyName>
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<TargetFrameworkProfile>Client</TargetFrameworkProfile>
<FileAlignment>512</FileAlignment>
@@ -100,18 +100,17 @@ <WarningLevel>4</WarningLevel>
<Optimize>false</Optimize>
</PropertyGroup>
+ <PropertyGroup>
+ <StartupObject />
+ </PropertyGroup>
<ItemGroup>
<Reference Include="System" />
<Reference Include="System.Core" />
- <Reference Include="System.Numerics" />
- <Reference Include="System.Xml.Linq" />
- <Reference Include="System.Data.DataSetExtensions" />
- <Reference Include="Microsoft.CSharp" />
<Reference Include="System.Data" />
+ <Reference Include="System.Numerics" />
<Reference Include="System.Deployment" />
<Reference Include="System.Drawing" />
<Reference Include="System.Windows.Forms" />
- <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
<Compile Include="BaseProvider.cs" />
@@ -127,7 +126,6 @@ <Compile Include="..\Model\Model.cs" />
<Compile Include="..\Model\ModelParser.cs" />
<Compile Include="Namer.cs" />
- <Compile Include="Program.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="SourceView.cs">
<SubType>Form</SubType>
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 2374a157..48a07820 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -114,6 +114,7 @@ namespace Microsoft.Boogie.SMTLib var sx = GetProverResponse();
if (sx == null) {
this.NeedsRestart = true;
+ Debug.Assert(false);
HandleError("Prover died");
return;
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index ad2b7e68..0d6e2aab 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -203,15 +203,18 @@ namespace Microsoft.Boogie { var filename = CommandLineOptions.Clo.ModelViewFile;
if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;
- var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();
+ if (!ModelHasStatesAlready) {
+ PopulateModelWithStates();
+ ModelHasStatesAlready = true;
+ }
if (filename == "-") {
- m.Write(tw);
+ Model.Write(tw);
tw.Flush();
} else {
using (var wr = new StreamWriter(filename, !firstModelFile)) {
firstModelFile = false;
- m.Write(wr);
+ Model.Write(wr);
}
}
}
@@ -227,16 +230,16 @@ namespace Microsoft.Boogie { m.Substitute(mapping);
}
- public Model GetModelWithStates()
+ public void PopulateModelWithStates()
{
- if (Model == null) return null;
+ Contract.Requires(Model != null);
Model m = Model;
ApplyRedirections(m);
var mvstates = m.TryGetFunc("$mv_state");
if (MvInfo == null || mvstates == null)
- return m;
+ return;
Contract.Assert(mvstates.Arity == 2);
@@ -282,8 +285,6 @@ namespace Microsoft.Boogie { Contract.Assume(false);
}
}
-
- return m;
}
private Model.Element GetModelValue(Model m, Variable v) {
|