summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/AbsInt/AbsInt.csproj11
-rw-r--r--Source/Basetypes/Basetypes.csproj4
-rw-r--r--Source/Boogie.sln490
-rw-r--r--Source/BoogieDriver/BoogieDriver.csproj31
-rw-r--r--Source/CodeContractsExtender/CodeContractsExtender.csproj4
-rw-r--r--Source/Core/CommandLineOptions.cs11
-rw-r--r--Source/Core/Core.csproj4
-rw-r--r--Source/Doomed/Doomed.csproj18
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.csproj24
-rw-r--r--Source/Graph/Graph.csproj4
-rw-r--r--Source/Houdini/Houdini.csproj4
-rw-r--r--Source/Model/Model.cs319
-rw-r--r--Source/Model/Model.csproj5
-rw-r--r--Source/Model/ModelParser.cs755
-rw-r--r--Source/ModelViewer/Main.cs2
-rw-r--r--Source/ModelViewer/ModelViewer.csproj3
-rw-r--r--Source/ModelViewer/VccProvider.cs2
-rw-r--r--Source/ParserHelper/ParserHelper.csproj2
-rw-r--r--Source/Predication/Predication.csproj12
-rw-r--r--Source/Provers/SMTLib/CVC4.cs71
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs1473
-rw-r--r--Source/Provers/SMTLib/SMTLib.csproj7
-rw-r--r--Source/Provers/SMTLib/SMTLibProverOptions.cs17
-rw-r--r--Source/Provers/SMTLib/Z3.cs10
-rw-r--r--Source/VCExpr/VCExpr.csproj4
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs6
-rw-r--r--Source/VCGeneration/StratifiedVC.cs2
-rw-r--r--Source/VCGeneration/VCGeneration.csproj4
28 files changed, 1962 insertions, 1337 deletions
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 7e421eb1..2c5f836d 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for AbsInt.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -140,6 +142,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
<DebugSymbols>true</DebugSymbols>
@@ -156,6 +160,8 @@
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
<OutputPath>bin\x86\Release\</OutputPath>
@@ -172,6 +178,7 @@
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'z3apidebug|x86'">
<DebugSymbols>true</DebugSymbols>
@@ -187,6 +194,8 @@
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">
<DebugSymbols>true</DebugSymbols>
@@ -201,6 +210,8 @@
<CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index a7b7cb71..520300fd 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for Basetypes.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index b93bc31f..c83c8770 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}"
@@ -55,32 +55,6 @@ 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
@@ -107,58 +81,31 @@ 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
- {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
+ {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
{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
@@ -184,31 +131,6 @@ 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
@@ -234,31 +156,80 @@ 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
- {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
+ {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
{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
@@ -284,30 +255,6 @@ 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
@@ -333,31 +280,55 @@ 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
- {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
+ {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
{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
@@ -383,54 +354,58 @@ 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
- {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
+ {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
{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
@@ -455,11 +430,66 @@ 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
- EndGlobalSection
- GlobalSection(SolutionProperties) = preSolution
- HideSolutionNode = FALSE
+ {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
+ EndGlobalSection
+ GlobalSection(SolutionProperties) = preSolution
+ HideSolutionNode = FALSE
+ EndGlobalSection
EndGlobal
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index f407c0dd..d0cc2fe6 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for BoogieDriver.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
<DebugSymbols>true</DebugSymbols>
@@ -152,6 +156,8 @@
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">
<OutputPath>bin\x86\Release\</OutputPath>
@@ -168,6 +174,7 @@
<CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'z3apidebug|x86'">
<DebugSymbols>true</DebugSymbols>
@@ -183,6 +190,8 @@
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">
<DebugSymbols>true</DebugSymbols>
@@ -199,6 +208,8 @@
<CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
@@ -211,7 +222,7 @@
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\AbsInt\AbsInt.csproj">
- <Project>{0efa3e43-690b-48dc-a72c-384a3ea7f31f}</Project>
+ <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>
<Name>AbsInt</Name>
</ProjectReference>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
@@ -227,39 +238,39 @@
<Name>Core</Name>
</ProjectReference>
<ProjectReference Include="..\Doomed\Doomed.csproj">
- <Project>{884386a3-58e9-40bb-a273-b24976775553}</Project>
+ <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>
<Name>Doomed</Name>
</ProjectReference>
<ProjectReference Include="..\ExecutionEngine\ExecutionEngine.csproj">
- <Project>{eaa5eb79-d475-4601-a59b-825c191cd25f}</Project>
+ <Project>{EAA5EB79-D475-4601-A59B-825C191CD25F}</Project>
<Name>ExecutionEngine</Name>
</ProjectReference>
<ProjectReference Include="..\Graph\Graph.csproj">
- <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
<ProjectReference Include="..\Houdini\Houdini.csproj">
- <Project>{cf41e903-78eb-43ba-a355-e5feb5ececd4}</Project>
+ <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>
<Name>Houdini</Name>
</ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
<ProjectReference Include="..\Predication\Predication.csproj">
- <Project>{afaa5ce1-c41b-44f0-88f8-fd8a43826d44}</Project>
+ <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project>
<Name>Predication</Name>
</ProjectReference>
<ProjectReference Include="..\Provers\SMTLib\SMTLib.csproj">
- <Project>{9b163aa3-36bc-4afb-88ab-79bc9e97e401}</Project>
+ <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>
<Name>SMTLib</Name>
</ProjectReference>
<ProjectReference Include="..\VCExpr\VCExpr.csproj">
- <Project>{56ffdbca-7d14-43b8-a6ca-22a20e417ee1}</Project>
+ <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
<Name>VCExpr</Name>
</ProjectReference>
<ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
- <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
<Name>VCGeneration</Name>
</ProjectReference>
</ItemGroup>
diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj
index 9473cf40..f307e35e 100644
--- a/Source/CodeContractsExtender/CodeContractsExtender.csproj
+++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for CodeContractsExtender.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index a9bd25ee..a1a4d740 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -411,6 +411,7 @@ namespace Microsoft.Boogie {
public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
public string Z3ExecutablePath = null;
+ public string CVC4ExecutablePath = null;
public enum ProverWarnings {
None,
@@ -1268,6 +1269,12 @@ namespace Microsoft.Boogie {
}
return true;
+ case "cvc4exe":
+ if (ps.ConfirmArgumentCount(1)) {
+ CVC4ExecutablePath = args[ps.i];
+ }
+ return true;
+
case "doBitVectorAnalysis":
DoBitVectorAnalysis = true;
if (ps.ConfirmArgumentCount(1)) {
@@ -1843,6 +1850,10 @@ namespace Microsoft.Boogie {
3 - (default) any
/z3exe:<path>
path to Z3 executable
+
+ CVC4 specific options:
+ /cvc4exe:<path>
+ path to CVC4 executable
");
}
}
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index d41fb40b..f3db4f9a 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for Core.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -139,6 +141,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Doomed/Doomed.csproj b/Source/Doomed/Doomed.csproj
index c3319022..a2390a39 100644
--- a/Source/Doomed/Doomed.csproj
+++ b/Source/Doomed/Doomed.csproj
@@ -12,6 +12,8 @@
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <ProductVersion>12.0.0</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -55,35 +57,35 @@
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
<ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{accc0156-0921-43ed-8f67-ad8bdc8cde31}</Project>
+ <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
<Name>CodeContractsExtender</Name>
</ProjectReference>
<ProjectReference Include="..\Core\Core.csproj">
- <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
<ProjectReference Include="..\Graph\Graph.csproj">
- <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
<ProjectReference Include="..\Model\Model.csproj">
- <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>
+ <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
<Name>Model</Name>
</ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
<ProjectReference Include="..\VCExpr\VCExpr.csproj">
- <Project>{56ffdbca-7d14-43b8-a6ca-22a20e417ee1}</Project>
+ <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
<Name>VCExpr</Name>
</ProjectReference>
<ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
- <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
<Name>VCGeneration</Name>
</ProjectReference>
</ItemGroup>
diff --git a/Source/ExecutionEngine/ExecutionEngine.csproj b/Source/ExecutionEngine/ExecutionEngine.csproj
index 91f13ed4..bebe686d 100644
--- a/Source/ExecutionEngine/ExecutionEngine.csproj
+++ b/Source/ExecutionEngine/ExecutionEngine.csproj
@@ -14,6 +14,8 @@
<TargetFrameworkProfile>Client</TargetFrameworkProfile>
<SignAssembly>true</SignAssembly>
<AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+ <ProductVersion>12.0.0</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -44,47 +46,47 @@
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\AbsInt\AbsInt.csproj">
- <Project>{0efa3e43-690b-48dc-a72c-384a3ea7f31f}</Project>
+ <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>
<Name>AbsInt</Name>
</ProjectReference>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
<ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{accc0156-0921-43ed-8f67-ad8bdc8cde31}</Project>
+ <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
<Name>CodeContractsExtender</Name>
</ProjectReference>
<ProjectReference Include="..\Core\Core.csproj">
- <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
<ProjectReference Include="..\Doomed\Doomed.csproj">
- <Project>{884386a3-58e9-40bb-a273-b24976775553}</Project>
+ <Project>{884386A3-58E9-40BB-A273-B24976775553}</Project>
<Name>Doomed</Name>
</ProjectReference>
<ProjectReference Include="..\Graph\Graph.csproj">
- <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
<ProjectReference Include="..\Houdini\Houdini.csproj">
- <Project>{cf41e903-78eb-43ba-a355-e5feb5ececd4}</Project>
+ <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>
<Name>Houdini</Name>
</ProjectReference>
<ProjectReference Include="..\Model\Model.csproj">
- <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>
+ <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
<Name>Model</Name>
</ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
<ProjectReference Include="..\Predication\Predication.csproj">
- <Project>{afaa5ce1-c41b-44f0-88f8-fd8a43826d44}</Project>
+ <Project>{AFAA5CE1-C41B-44F0-88F8-FD8A43826D44}</Project>
<Name>Predication</Name>
</ProjectReference>
<ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
- <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
<Name>VCGeneration</Name>
</ProjectReference>
</ItemGroup>
diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj
index 718ced5d..9ed20759 100644
--- a/Source/Graph/Graph.csproj
+++ b/Source/Graph/Graph.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for Graph.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index 06d68dba..e4840d1d 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -64,6 +64,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
@@ -101,7 +103,7 @@
<Name>Graph</Name>
</ProjectReference>
<ProjectReference Include="..\Model\Model.csproj">
- <Project>{acef88d5-dadd-46da-bae1-2144d63f4c83}</Project>
+ <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
<Name>Model</Name>
</ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
diff --git a/Source/Model/Model.cs b/Source/Model/Model.cs
index 16dec8b0..b9a2dfcf 100644
--- a/Source/Model/Model.cs
+++ b/Source/Model/Model.cs
@@ -695,305 +695,24 @@ namespace Microsoft.Boogie
foreach (var f in functions) f.Substitute(mapping);
}
- class Parser
- {
- internal System.IO.TextReader rd;
- string lastLine = "";
- int lineNo;
- internal List<Model> resModels = new List<Model>();
- Model currModel;
-
- void BadModel(string msg)
- {
- throw new ArgumentException(string.Format("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));
- }
-
- static char[] seps = new char[] { ' ' };
-
- int CountOpenParentheses(string s, int n) {
- int f = n;
- foreach (char c in s) {
- if (c == '(')
- f++;
- else if (c == ')')
- f--;
- }
- if (f < 0) BadModel("mismatched parentheses in datatype term");
- return f;
- }
-
- static Regex bv = new Regex(@"\(_ BitVec (\d+)\)");
-
- /*
- List<object> GetFunctionTuple(string newLine) {
- if (newLine == null)
- return null;
- newLine = bv.Replace(newLine, "bv${1}");
- string line = newLine;
- int openParenCounter = CountOpenParentheses(newLine, 0);
- if (!newLine.Contains("}")) {
- while (openParenCounter > 0) {
- newLine = ReadLine();
- if (newLine == null) {
- return null;
- }
- line += newLine;
- openParenCounter = CountOpenParentheses(newLine, openParenCounter);
- }
- }
-
- line = line.Replace("(", " ( ");
- line = line.Replace(")", " ) ");
- line = line.Replace(",", " ");
- var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
-
- List<object> newTuple = new List<object>();
- Stack<int> wordStack = new Stack<int>();
- for (int i = 0; i < tuple.Length; i++) {
- string elem = tuple[i];
- if (elem == "(") {
- wordStack.Push(newTuple.Count - 1);
- }
- else if (elem == ")") {
- int openParenIndex = wordStack.Pop();
- List<object> ls = new List<object>();
- for (int j = openParenIndex; j < newTuple.Count; j++)
- {
- ls.Add(newTuple[j]);
- }
- newTuple.RemoveRange(openParenIndex, newTuple.Count - openParenIndex);
- newTuple.Add(ls);
- }
- else {
- newTuple.Add(elem);
- }
- }
- return newTuple;
- }
- */
-
- List<object> GetFunctionTuple(string newLine)
- {
- if (newLine == null)
- return null;
- newLine = bv.Replace(newLine, "bv${1}");
- string line = newLine;
- int openParenCounter = CountOpenParentheses(newLine, 0);
- if (!newLine.Contains("}"))
- {
- while (openParenCounter > 0)
- {
- newLine = ReadLine();
- if (newLine == null)
- {
- return null;
- }
- line += newLine;
- openParenCounter = CountOpenParentheses(newLine, openParenCounter);
- }
- }
-
- line = line.Replace("(", " ( ");
- line = line.Replace(")", " ) ");
- var tuple = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
-
- List<object> newTuple = new List<object>();
- Stack<List<object>> wordStack = new Stack<List<object>>();
- for (int i = 0; i < tuple.Length; i++)
- {
- string elem = tuple[i];
- if (elem == "(")
- {
- List<object> ls = new List<object>();
- wordStack.Push(ls);
- }
- else if (elem == ")")
- {
- List<object> ls = wordStack.Pop();
- if (wordStack.Count > 0)
- {
- wordStack.Peek().Add(ls);
- }
- else
- {
- newTuple.Add(ls);
- }
- }
- else if (wordStack.Count > 0)
- {
- wordStack.Peek().Add(elem);
- }
- else
- {
- newTuple.Add(elem);
- }
- }
- return newTuple;
- }
-
- string[] GetWords(string line)
- {
- if (line == null)
- return null;
- var words = line.Split(seps, StringSplitOptions.RemoveEmptyEntries);
- return words;
- }
-
- string ReadLine()
- {
- var l = rd.ReadLine();
- if (l != null) {
- lineNo++;
- lastLine = l;
- }
- return l;
- }
-
- Element GetElt(object o) {
- string s = o as string;
- if (s != null)
- return GetElt(s);
- List<object> os = (List<object>)o;
- List<Element> args = new List<Element>();
- for (int i = 1; i < os.Count; i++) {
- args.Add(GetElt(os[i]));
- }
- return new DatatypeValue(currModel, (string)os[0], args);
- }
-
- Element GetElt(string name) {
- Element ret = currModel.TryMkElement(name);
- if (ret == null)
- BadModel("invalid element name " + name);
- return ret;
- }
-
- void NewModel()
- {
- lastLine = "";
- currModel = new Model();
- resModels.Add(currModel);
- }
-
- internal void Run()
- {
- var selectFunctions = new Dictionary<int, Model.Func>();
- var storeFunctions = new Dictionary<int, Model.Func>();
- for (; ; ) {
- var line = ReadLine();
- if (line == null) break; // end of model, everything fine
-
- if (line == "Counterexample:" || line == "Z3 error model: " || line == "*** MODEL") {
- NewModel();
- continue;
- }
-
- if (line.EndsWith(": Invalid.") || line.EndsWith(": Valid.")|| line.StartsWith("labels:"))
- continue;
- if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
- continue;
-
- var words = GetFunctionTuple(line);
- if (words.Count == 0) continue;
- var lastWord = words[words.Count - 1];
-
- if (currModel == null)
- BadModel("model begin marker not found");
-
- if (line.StartsWith("*** STATE ")) {
- var name = line.Substring(10);
- CapturedState cs;
- if (name == "<initial>")
- cs = currModel.InitialState;
- else
- cs = currModel.MkState(name);
- for (; ; ) {
- var tmpline = ReadLine();
- if (tmpline == "*** END_STATE") break;
- var tuple = GetFunctionTuple(tmpline);
- if (tuple == null) BadModel("EOF in state table");
- if (tuple.Count == 0) continue;
- if (tuple.Count == 3 && tuple[0] is string && tuple[1] is string && ((string) tuple[1]) == "->")
- {
- cs.AddBinding((string)tuple[0], GetElt(tuple[2]));
- }
- else
- {
- BadModel("invalid state tuple definition");
- }
- }
- continue;
- }
-
- if (words.Count == 3 && words[1] is string && ((string) words[1]) == "->") {
- var funName = (string) words[0];
- Func fn = null;
-
- if (lastWord is string && ((string) lastWord) == "{") {
- fn = currModel.TryGetFunc(funName);
- for ( ; ; ) {
- var tuple = GetFunctionTuple(ReadLine());
- if (tuple == null) BadModel("EOF in function table");
- if (tuple.Count == 0) continue;
- string tuple0 = tuple[0] as string;
- if (tuple.Count == 1) {
- if (fn == null)
- fn = currModel.MkFunc(funName, 1);
- if (tuple0 == "}") break;
- if (fn.Else == null)
- fn.Else = GetElt(tuple[0]);
- continue;
- }
- string tuplePenultimate = tuple[tuple.Count - 2] as string;
- if (tuplePenultimate != "->") BadModel("invalid function tuple definition");
- var resultName = tuple[tuple.Count - 1];
- if (tuple0 == "else") {
- if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) {
- fn.Else = GetElt(resultName);
- }
- continue;
- }
-
- if (fn == null) {
- var arity = tuple.Count - 2;
- if (Regex.IsMatch(funName, "^MapType[0-9]*Select$")) {
- funName = string.Format("[{0}]", arity);
- if (!selectFunctions.TryGetValue(arity, out fn)) {
- fn = currModel.MkFunc(funName, arity);
- selectFunctions.Add(arity, fn);
- }
- } else if (Regex.IsMatch(funName, "^MapType[0-9]*Store$")) {
- funName = string.Format("[{0}:=]", arity);
- if (!storeFunctions.TryGetValue(arity, out fn)) {
- fn = currModel.MkFunc(funName, arity);
- storeFunctions.Add(arity, fn);
- }
- } else {
- fn = currModel.MkFunc(funName, arity);
- }
- }
- var args = new Element[fn.Arity];
- for (int i = 0; i < fn.Arity; ++i)
- args[i] = GetElt(tuple[i]);
- fn.AddApp(GetElt(resultName), args);
- }
- } else {
- fn = currModel.MkFunc(funName, 0);
- fn.SetConstant(GetElt(lastWord));
- }
- } else {
- BadModel("unidentified line");
- }
- }
- }
- }
-
- public static List<Model> ParseModels(System.IO.TextReader rd)
- {
- var p = new Parser();
- p.rd = rd;
- p.Run();
- return p.resModels;
- }
+ public static List<Model> ParseModels(System.IO.TextReader rd, string prover)
+ {
+ ModelParser p;
+
+ switch (prover)
+ {
+ case "SMTLIB2":
+ p = new ParserSMT();
+ break;
+ default:
+ p = new ParserZ3();
+ break;
+ }
+
+ p.rd = rd;
+ p.Run();
+
+ return p.resModels;
+ }
}
}
diff --git a/Source/Model/Model.csproj b/Source/Model/Model.csproj
index a14dde8e..cfd5f852 100644
--- a/Source/Model/Model.csproj
+++ b/Source/Model/Model.csproj
@@ -36,7 +36,7 @@
<SignAssembly>true</SignAssembly>
</PropertyGroup>
<PropertyGroup>
- <AssemblyOriginatorKeyFile>../InterimKey.snk</AssemblyOriginatorKeyFile>
+ <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -77,12 +77,15 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
</ItemGroup>
<ItemGroup>
<Compile Include="Model.cs" />
+ <Compile Include="ModelParser.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="..\version.cs" />
</ItemGroup>
diff --git a/Source/Model/ModelParser.cs b/Source/Model/ModelParser.cs
new file mode 100644
index 00000000..40fd3c9a
--- /dev/null
+++ b/Source/Model/ModelParser.cs
@@ -0,0 +1,755 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Linq;
+using System.Collections.Generic;
+using System.Text;
+using System.Diagnostics;
+using System.Text.RegularExpressions;
+
+namespace Microsoft.Boogie
+{
+ abstract internal class ModelParser
+ {
+ protected Model currModel;
+ int lineNo;
+ internal List<Model> resModels = new List<Model> ();
+ internal System.IO.TextReader rd;
+ string lastLine = "";
+ protected static char[] seps = new char[] { ' ' };
+ protected static Regex bv = new Regex (@"\(_ BitVec (\d+)\)");
+
+ protected void NewModel ()
+ {
+ lastLine = "";
+ currModel = new Model ();
+ resModels.Add (currModel);
+ }
+
+ protected void BadModel (string msg)
+ {
+ throw new ArgumentException (string.Format ("Invalid model: {0}, at line {1} ({2})", msg, lineNo, lastLine));
+ }
+
+ protected string ReadLine ()
+ {
+ var l = rd.ReadLine ();
+ if (l != null) {
+ lineNo++;
+ lastLine = l;
+ }
+ return l;
+ }
+
+ string[] GetWords (string line)
+ {
+ if (line == null)
+ return null;
+ var words = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+ return words;
+ }
+
+ Model.Element GetElt (string name)
+ {
+ Model.Element ret = currModel.TryMkElement (name);
+ if (ret == null)
+ BadModel ("invalid element name " + name);
+ return ret;
+ }
+
+ protected Model.Element GetElt (object o)
+ {
+ string s = o as string;
+ if (s != null)
+ return GetElt (s);
+ List<object> os = (List<object>)o;
+ List<Model.Element> args = new List<Model.Element> ();
+ for (int i = 1; i < os.Count; i++) {
+ args.Add (GetElt (os [i]));
+ }
+ return new Model.DatatypeValue (currModel, (string)os [0], args);
+ }
+
+ protected int CountOpenParentheses (string s, int n)
+ {
+ int f = n;
+ foreach (char c in s) {
+ if (c == '(')
+ f++;
+ else if (c == ')')
+ f--;
+ }
+ if (f < 0)
+ BadModel ("mismatched parentheses in datatype term");
+ return f;
+ }
+
+ abstract internal void Run ();
+ }
+
+ class ParserZ3 : ModelParser
+ {
+ List<object> GetFunctionTokens (string newLine)
+ {
+ if (newLine == null)
+ return null;
+ newLine = bv.Replace (newLine, "bv${1}");
+ string line = newLine;
+ int openParenCounter = CountOpenParentheses (newLine, 0);
+ if (!newLine.Contains ("}")) {
+ while (openParenCounter > 0) {
+ newLine = ReadLine ();
+ if (newLine == null) {
+ return null;
+ }
+ line += newLine;
+ openParenCounter = CountOpenParentheses (newLine, openParenCounter);
+ }
+ }
+
+ line = line.Replace ("(", " ( ");
+ line = line.Replace (")", " ) ");
+ var tuple = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+
+ List<object> newTuple = new List<object> ();
+ Stack<List<object>> wordStack = new Stack<List<object>> ();
+ for (int i = 0; i < tuple.Length; i++) {
+ string elem = tuple [i];
+ if (elem == "(") {
+ List<object> ls = new List<object> ();
+ wordStack.Push (ls);
+ } else if (elem == ")") {
+ List<object> ls = wordStack.Pop ();
+ if (wordStack.Count > 0) {
+ wordStack.Peek ().Add (ls);
+ } else {
+ newTuple.Add (ls);
+ }
+ } else if (wordStack.Count > 0) {
+ wordStack.Peek ().Add (elem);
+ } else {
+ newTuple.Add (elem);
+ }
+ }
+ return newTuple;
+ }
+
+ internal override void Run ()
+ {
+ var selectFunctions = new Dictionary<int, Model.Func> ();
+ var storeFunctions = new Dictionary<int, Model.Func> ();
+ for (; ;) {
+ var line = ReadLine ();
+ if (line == null)
+ break; // end of model, everything fine
+
+ if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") {
+ NewModel ();
+ continue;
+ }
+
+ if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:"))
+ continue;
+ if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
+ continue;
+
+ var words = GetFunctionTokens (line);
+ if (words.Count == 0)
+ continue;
+ var lastWord = words [words.Count - 1];
+
+ if (currModel == null)
+ BadModel ("model begin marker not found");
+
+ if (line.StartsWith ("*** STATE ")) {
+ var name = line.Substring (10);
+ Model.CapturedState cs;
+ if (name == "<initial>")
+ cs = currModel.InitialState;
+ else
+ cs = currModel.MkState (name);
+ for (; ;) {
+ var tmpline = ReadLine ();
+ if (tmpline == "*** END_STATE")
+ break;
+ var tuple = GetFunctionTokens (tmpline);
+ if (tuple == null)
+ BadModel ("EOF in state table");
+ if (tuple.Count == 0)
+ continue;
+ if (tuple.Count == 3 && tuple [0] is string && tuple [1] is string && ((string)tuple [1]) == "->") {
+ cs.AddBinding ((string)tuple [0], GetElt (tuple [2]));
+ } else {
+ BadModel ("invalid state tuple definition");
+ }
+ }
+ continue;
+ }
+
+ if (words.Count == 3 && words [1] is string && ((string)words [1]) == "->") {
+ var funName = (string)words [0];
+ Model.Func fn = null;
+
+ if (lastWord is string && ((string)lastWord) == "{") {
+ fn = currModel.TryGetFunc (funName);
+ for (; ;) {
+ var tuple = GetFunctionTokens (ReadLine ());
+ if (tuple == null)
+ BadModel ("EOF in function table");
+ if (tuple.Count == 0)
+ continue;
+ string tuple0 = tuple [0] as string;
+ if (tuple.Count == 1) {
+ if (fn == null)
+ fn = currModel.MkFunc (funName, 1);
+ if (tuple0 == "}")
+ break;
+ if (fn.Else == null)
+ fn.Else = GetElt (tuple [0]);
+ continue;
+ }
+ string tuplePenultimate = tuple [tuple.Count - 2] as string;
+ if (tuplePenultimate != "->")
+ BadModel ("invalid function tuple definition");
+ var resultName = tuple [tuple.Count - 1];
+ if (tuple0 == "else") {
+ if (fn != null && !(resultName is string && ((string)resultName) == "#unspecified") && fn.Else == null) {
+ fn.Else = GetElt (resultName);
+ }
+ continue;
+ }
+
+ if (fn == null) {
+ var arity = tuple.Count - 2;
+ if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
+ funName = string.Format ("[{0}]", arity);
+ if (!selectFunctions.TryGetValue (arity, out fn)) {
+ fn = currModel.MkFunc (funName, arity);
+ selectFunctions.Add (arity, fn);
+ }
+ } else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
+ funName = string.Format ("[{0}:=]", arity);
+ if (!storeFunctions.TryGetValue (arity, out fn)) {
+ fn = currModel.MkFunc (funName, arity);
+ storeFunctions.Add (arity, fn);
+ }
+ } else {
+ fn = currModel.MkFunc (funName, arity);
+ }
+ }
+ var args = new Model.Element[fn.Arity];
+ for (int i = 0; i < fn.Arity; ++i)
+ args [i] = GetElt (tuple [i]);
+ fn.AddApp (GetElt (resultName), args);
+ }
+ } else {
+ fn = currModel.MkFunc (funName, 0);
+ fn.SetConstant (GetElt (lastWord));
+ }
+ } else {
+ BadModel ("unidentified line");
+ }
+ }
+ }
+ }
+
+ class ParserSMT : ModelParser
+ {
+ string[] tokens;
+ List<string> output;
+ int arity;
+ int arrayNum;
+ int index;
+
+ void FindArity ()
+ {
+ arity = 0;
+ int p_count = 1;
+ int i = 4;
+
+ while (p_count > 0) {
+ if (i == tokens.Length - 1)
+ break;
+ else if (tokens [i] == ")")
+ p_count--;
+ else if (tokens [i] == "(" && tokens [i + 1] != "ite") {
+ p_count++;
+ arity++;
+ }
+
+ i++;
+ }
+ }
+
+ string GetValue (int idx)
+ {
+ string value = tokens [idx];
+
+ if (tokens [idx - 1] == "-") {
+ value = "(- " + value + ")";
+ } else if (tokens [idx - 2] == "_") {
+ value = tokens [idx - 1] + "[" + tokens [idx] + "]";
+ }
+
+ return value;
+ }
+
+ void SplitArrayExpression ()
+ {
+ output.Add ("as-array[k!" + arrayNum + "]");
+
+ if (output.Contains ("@SPLIT")) {
+ output.Add (" ");
+ output.Add ("}");
+ }
+
+ output.Add ("@SPLIT");
+ output.Add ("k!" + arrayNum);
+ output.Add ("->");
+ output.Add ("{");
+ output.Add (" ");
+
+ arrayNum++;
+ }
+
+ void ParseArrayExpr ()
+ {
+ while (tokens [index] != "as-array" && tokens [index] != "store" && tokens [index] != "__array_store_all__")
+ index++;
+
+ if (tokens [index] == "store") {
+ SplitArrayExpression ();
+
+ List<string> args = new List<string> ();
+ int p_count = 1;
+ index += 4;
+
+ while (p_count > 0) {
+ if (tokens [index] == ")")
+ p_count--;
+ else if (tokens [index] == "(")
+ p_count++;
+ index++;
+ }
+
+ if ((tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") ||
+ (tokens [index] == "(" && tokens [index + 1] == "store")) {
+ SplitArrayExpression ();
+ } else {
+ while (args.Count < 3) {
+ if (tokens [index] == ")")
+ index++;
+ else if (tokens [index] == "(") {
+ while (tokens [index] != ")")
+ index++;
+ args.Add (GetValue (index - 1));
+ } else {
+ args.Add (GetValue (index));
+ }
+
+ index++;
+ }
+
+ output.Add (args [1]);
+ output.Add ("->");
+ output.Add (args [2]);
+ output.Add (" ");
+ output.Add ("else");
+ output.Add ("->");
+ output.Add (args [0]);
+ }
+ } else if (tokens [index] == "__array_store_all__") {
+ SplitArrayExpression ();
+
+ while (tokens[index] == "__array_store_all__") {
+ int p_count = 1;
+ index += 2;
+
+ while (p_count > 0) {
+ if (tokens [index] == ")")
+ p_count--;
+ else if (tokens [index] == "(")
+ p_count++;
+ index++;
+ }
+
+ if (tokens [index] == "(" && tokens [index + 1] == "__array_store_all__") {
+ SplitArrayExpression ();
+ index++;
+ } else {
+ if (tokens [index] == ")")
+ index++;
+ else if (tokens [index] == "(") {
+ while (tokens [index] != ")")
+ index++;
+ output.Add (GetValue (index - 1));
+ } else {
+ output.Add (GetValue (index));
+ }
+
+ index++;
+ }
+ }
+ } else if (tokens [index] == "as-array") {
+ output.Add ("as-array[" + tokens [index + 1] + "]");
+ }
+ }
+
+ void ParseIteExpr ()
+ {
+ List<string> args = new List<string> ();
+ List<string> results = new List<string> ();
+
+ FindArity ();
+
+ int occurrences = 0;
+
+ foreach (string tok in tokens) {
+ if (tok == "_ufmt_1")
+ occurrences++;
+ }
+
+ for (; ;) {
+ index++;
+
+ if (tokens [index] == "=") {
+ index += 2;
+
+ if (tokens [index] == "(") {
+ while (tokens [index] != ")")
+ index++;
+ args.Add (GetValue (index - 1));
+ } else {
+ args.Add (GetValue (index));
+ }
+ }
+
+ if ((args.Count > 0 && args.Count % arity == 0) ||
+ (results.Count > 0 && occurrences <= 2 && occurrences > 0)) {
+ index += 2;
+
+ if (tokens [index] == "(") {
+ while (tokens [index] != ")")
+ index++;
+ results.Add (GetValue (index - 1));
+ } else {
+ results.Add (GetValue (index));
+ }
+
+ while (index < tokens.Length - 1 && tokens[index + 1] != "=")
+ index++;
+
+ if (index == tokens.Length - 1) {
+ while (tokens[index] == ")")
+ index += -1;
+ results.Add (GetValue (index));
+ break;
+ }
+ }
+ }
+
+ int i = 0;
+
+ for (int j = 0; j < results.Count - 1; j++) {
+ if (occurrences > 2) {
+ for (int r = 0; r < arity; r++) {
+ output.Add (args [i]);
+ i++;
+ }
+ } else if (occurrences > 0) {
+ if (arity == 1) {
+ output.Add (args [i]);
+ i++;
+ } else {
+ output.Add (args [0]);
+
+ for (int r = 1; r < arity; r++) {
+ i++;
+ output.Add (args [i]);
+ }
+ }
+ } else {
+ for (int r = 0; r < arity; r++) {
+ output.Add (args [i]);
+ i++;
+ }
+ }
+
+ output.Add ("->");
+ output.Add (results [j]);
+ output.Add (" ");
+ }
+
+ output.Add ("else");
+ output.Add ("->");
+ output.Add (results [results.Count - 1]);
+ }
+
+ void ParseEndOfExpr ()
+ {
+ index++;
+
+ if (index == tokens.Length && output.Count == 2) {
+ index += -2;
+
+ if (tokens [index] == ")") {
+ index += -1;
+ output.Add (GetValue (index));
+ } else {
+ output.Add (GetValue (index));
+ }
+ }
+
+ if (index == tokens.Length && output.Contains ("{")) {
+ output.Add (" ");
+ output.Add ("}");
+ }
+ }
+
+ List<string>[] TrySplitExpr (List<string> expr)
+ {
+ int splits = 1;
+ foreach (string tok in expr)
+ if (tok.Equals ("@SPLIT"))
+ splits++;
+
+ List<string>[] newExpr = new List<string>[splits];
+
+ for (int s = 0; s < splits; s++)
+ newExpr [s] = new List<string> ();
+
+ int i = 0;
+ foreach (string tok in expr) {
+ if (tok.Equals ("@SPLIT")) {
+ i++;
+ continue;
+ }
+
+ newExpr [i].Add (tok);
+ }
+
+ return newExpr;
+ }
+
+ List<string> GetParsedTokens (string newLine)
+ {
+ if (newLine == null)
+ return null;
+
+ newLine = bv.Replace (newLine, "bv${1}");
+
+ string line = newLine;
+ int openParenCounter = CountOpenParentheses (newLine, 0);
+
+ while (openParenCounter > 0) {
+ newLine = ReadLine ();
+ if (newLine == null) {
+ return null;
+ }
+ line += newLine;
+ openParenCounter = CountOpenParentheses (newLine, openParenCounter);
+ }
+
+ line = line.Replace ("(", " ( ");
+ line = line.Replace (")", " ) ");
+
+ tokens = line.Split (seps, StringSplitOptions.RemoveEmptyEntries);
+ output = new List<string> ();
+
+ index = 0;
+ bool doneParsing = false;
+
+ while (!doneParsing) {
+ switch (tokens [index]) {
+ case ")":
+ ParseEndOfExpr ();
+ break;
+
+ case "define-fun":
+ output.Add (GetValue (index + 1));
+ output.Add ("->");
+ index += 2;
+ break;
+
+ case "Array":
+ ParseArrayExpr ();
+ break;
+
+ case "ite":
+ ParseIteExpr ();
+ break;
+
+ case "_ufmt_1":
+ case "x!1":
+ output.Add ("{");
+ output.Add (" ");
+ index++;
+ break;
+
+ default:
+ index++;
+ break;
+ }
+
+ if (index == tokens.Length)
+ doneParsing = true;
+ }
+
+ return output;
+ }
+
+ internal override void Run ()
+ {
+ var selectFunctions = new Dictionary<int, Model.Func> ();
+ var storeFunctions = new Dictionary<int, Model.Func> ();
+ arrayNum = 0;
+
+ for (; ;) {
+ var line = ReadLine ();
+ if (line == null)
+ break; // end of model, everything fine
+ if (line == "Counterexample:" || line == "Error model: " || line == "*** MODEL") {
+ NewModel ();
+ continue;
+ }
+ if (line.EndsWith (": Invalid.") || line.EndsWith (": Valid.") || line.StartsWith ("labels:"))
+ continue;
+ if (line == "END_OF_MODEL" || line == "." || line == "*** END_MODEL")
+ continue;
+
+ //Console.WriteLine("\n\n# :: " + line);
+
+ var words = GetParsedTokens (line);
+ if (words.Count == 0)
+ continue;
+ var exprs = TrySplitExpr (words);
+
+ foreach (List<string> expr in exprs) {
+ /*Console.WriteLine ("");
+ for (int i = 0; i < expr.Count; i++) {
+ Console.Write (expr [i] + " ");
+ }*/
+
+ var lastToken = expr [expr.Count - 1];
+ if (currModel == null)
+ BadModel ("model begin marker not found");
+
+ if (expr.Count > 3 && expr [1] == "->") {
+ var funName = (string)expr [0];
+ Model.Func fn = null;
+ int i = 4;
+
+ if (expr [2] != "{" && expr [6] != "{")
+ BadModel ("unidentified function definition 5");
+
+ fn = currModel.TryGetFunc (funName);
+
+ for (; ;) {
+ if (expr [i] == "}") {
+ if (i == expr.Count - 1) {
+ if (fn == null)
+ fn = currModel.MkFunc (funName, 1);
+ break;
+ } else {
+ i++;
+ continue;
+ }
+ }
+
+ for (; ;) {
+ if (expr [i] == " ") {
+ i++;
+ break;
+ }
+
+ if ((i == 4 || i == 8) && expr [i - 1] == " " && expr [i + 1] == " ") {
+ if (fn.Else == null)
+ fn.Else = GetElt (expr [i]);
+ i++;
+ continue;
+ }
+
+ if (expr [i] == "else") {
+ if (expr [i + 1] == "->") {
+ i += 2;
+
+ if (expr [i] == "}")
+ BadModel ("unidentified function definition 1");
+
+ if (expr [i] == "{") {
+ i++;
+ continue;
+ } else {
+ if (fn != null && !(expr [i] == "#unspecified") && fn.Else == null)
+ fn.Else = GetElt (expr [i]);
+ i++;
+ continue;
+ }
+ } else
+ BadModel ("unidentified function definition 2");
+ }
+
+ int arity = 0;
+ for (; ;) {
+ arity++;
+ if (expr [arity + i] == " ") {
+ arity -= 2;
+ break;
+ }
+ }
+
+ if (expr [i + arity] == "->") {
+ i += arity + 1;
+
+ if (expr [i] == "}")
+ BadModel ("unidentified function definition 3");
+ } else
+ BadModel ("unidentified function definition 4");
+
+ if (fn == null) {
+ if (Regex.IsMatch (funName, "^MapType[0-9]*Select$")) {
+ funName = string.Format ("[{0}]", arity);
+
+ if (!selectFunctions.TryGetValue (arity, out fn)) {
+ fn = currModel.MkFunc (funName, arity);
+ selectFunctions.Add (arity, fn);
+ }
+ } else if (Regex.IsMatch (funName, "^MapType[0-9]*Store$")) {
+ funName = string.Format ("[{0}:=]", arity);
+
+ if (!storeFunctions.TryGetValue (arity, out fn)) {
+ fn = currModel.MkFunc (funName, arity);
+ storeFunctions.Add (arity, fn);
+ }
+ } else {
+ fn = currModel.MkFunc (funName, arity);
+ }
+ }
+
+ var args = new Model.Element[fn.Arity];
+
+ for (var idx = 0; idx < fn.Arity; ++idx)
+ args [idx] = GetElt (expr [idx + i - arity - 1]);
+
+ fn.AddApp (GetElt (expr [i]), args);
+
+ i++;
+ break;
+ }
+ }
+ } else if (expr.Count == 3 && expr [1] == "->") {
+ var funName = (string)expr [0];
+ Model.Func fn = null;
+
+ fn = currModel.MkFunc (funName, 0);
+ fn.SetConstant (GetElt (lastToken));
+ } else
+ BadModel ("unidentified line");
+ }
+ }
+ }
+ }
+}
diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 2e612aa1..09dce05f 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -99,7 +99,7 @@ namespace Microsoft.Boogie.ModelViewer
if (!string.IsNullOrWhiteSpace(modelFileName) && File.Exists(modelFileName)) {
using (var rd = File.OpenText(modelFileName)) {
- allModels = Model.ParseModels(rd).ToArray();
+ allModels = Model.ParseModels(rd,"").ToArray();
}
modelId = setModelIdTo;
diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index ae46767b..49965d5e 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -97,6 +97,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
@@ -123,6 +125,7 @@
<DependentUpon>Main.cs</DependentUpon>
</Compile>
<Compile Include="..\Model\Model.cs" />
+ <Compile Include="..\Model\ModelParser.cs" />
<Compile Include="Namer.cs" />
<Compile Include="Program.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
diff --git a/Source/ModelViewer/VccProvider.cs b/Source/ModelViewer/VccProvider.cs
index c226d646..b4540717 100644
--- a/Source/ModelViewer/VccProvider.cs
+++ b/Source/ModelViewer/VccProvider.cs
@@ -274,7 +274,7 @@ namespace Microsoft.Boogie.ModelViewer.Vcc
new string[] {
"$_pow2", "$as_composite_field", "$as_field_with_type", "$as_in_range_t",
"$as_primitive_field", "$base", "$call_transition", "tickleBool", "Ctor",
- "@MV_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",
+ "$mv_state", "$field", "$field_arr_root", "$field_kind", "$field_offset",
"$field_parent_type", "$field_type", "$file_name_is", "$good_state",
"$good_state_ext", "$function_arg_type", "$has_field_at0", "$map_domain",
"$map_range", "$map_t", "$ptr_to", "$ptr_to_i1", "$ptr_to_i2",
diff --git a/Source/ParserHelper/ParserHelper.csproj b/Source/ParserHelper/ParserHelper.csproj
index cd665a75..f8155b61 100644
--- a/Source/ParserHelper/ParserHelper.csproj
+++ b/Source/ParserHelper/ParserHelper.csproj
@@ -99,6 +99,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj
index 8060f52f..663de263 100644
--- a/Source/Predication/Predication.csproj
+++ b/Source/Predication/Predication.csproj
@@ -12,6 +12,8 @@
<TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ <ProductVersion>12.0.0</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
@@ -52,23 +54,23 @@
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\Basetypes\Basetypes.csproj">
- <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
<Name>Basetypes</Name>
</ProjectReference>
<ProjectReference Include="..\Core\Core.csproj">
- <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
<Name>Core</Name>
</ProjectReference>
<ProjectReference Include="..\Graph\Graph.csproj">
- <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
<ProjectReference Include="..\ParserHelper\ParserHelper.csproj">
- <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>
+ <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
<Name>ParserHelper</Name>
</ProjectReference>
<ProjectReference Include="..\VCGeneration\VCGeneration.csproj">
- <Project>{e1f10180-c7b9-4147-b51f-fa1b701966dc}</Project>
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
<Name>VCGeneration</Name>
</ProjectReference>
</ItemGroup>
diff --git a/Source/Provers/SMTLib/CVC4.cs b/Source/Provers/SMTLib/CVC4.cs
new file mode 100644
index 00000000..0ac2ec20
--- /dev/null
+++ b/Source/Provers/SMTLib/CVC4.cs
@@ -0,0 +1,71 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.IO;
+using System.Text.RegularExpressions;
+
+namespace Microsoft.Boogie.SMTLib
+{
+ class CVC4
+ {
+ static string _proverPath;
+
+ static string CodebaseString()
+ {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));
+ }
+
+ public static string ExecutablePath()
+ {
+ if (_proverPath == null)
+ FindExecutable();
+ return _proverPath;
+ }
+
+ static void FindExecutable()
+ // throws ProverException, System.IO.FileNotFoundException;
+ {
+ Contract.Ensures(_proverPath != null);
+
+ // Command line option 'cvc4exe' always has priority if set
+ if (CommandLineOptions.Clo.CVC4ExecutablePath != null)
+ {
+ _proverPath = CommandLineOptions.Clo.CVC4ExecutablePath;
+ if (!File.Exists(_proverPath))
+ {
+ throw new ProverException("Cannot find prover specified with cvc4exe: " + _proverPath);
+ }
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+
+ var proverExe = "cvc4.exe";
+
+ if (_proverPath == null)
+ {
+ // Initialize '_proverPath'
+ _proverPath = Path.Combine(CodebaseString(), proverExe);
+ string firstTry = _proverPath;
+
+ if (File.Exists(firstTry))
+ {
+ if (CommandLineOptions.Clo.Trace)
+ {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+ else
+ {
+ throw new ProverException("Cannot find executable: " + firstTry);
+ }
+ }
+ }
+ }
+}
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index ee955def..815e5a45 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -8,6 +8,7 @@ using System.Collections;
using System.Collections.Generic;
using System.Threading;
using System.IO;
+
//using ExternalProver;
using System.Linq;
using System.Diagnostics;
@@ -18,555 +19,509 @@ using Microsoft.Boogie.VCExprAST;
using Microsoft.Boogie.Clustering;
using Microsoft.Boogie.TypeErasure;
using System.Text;
-
using RPFP = Microsoft.Boogie.RPFP;
namespace Microsoft.Boogie.SMTLib
{
- public class SMTLibProcessTheoremProver : ProverInterface
- {
- private readonly SMTLibProverContext ctx;
- private readonly VCExpressionGenerator gen;
- private readonly SMTLibProverOptions options;
- private bool usingUnsatCore;
- private RPFP rpfp = null;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(ctx != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(DeclCollector != null);
- Contract.Invariant(cce.NonNullElements(Axioms));
- Contract.Invariant(cce.NonNullElements(TypeDecls));
- Contract.Invariant(_backgroundPredicates != null);
-
- }
-
-
- [NotDelayed]
- public SMTLibProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,
- SMTLibProverContext ctx)
- {
- Contract.Requires(options != null);
- Contract.Requires(gen != null);
- Contract.Requires(ctx != null);
- InitializeGlobalInformation("UnivBackPred2.smt2");
-
- this.options = (SMTLibProverOptions)options;
- this.ctx = ctx;
- this.gen = gen;
- this.usingUnsatCore = false;
-
- SetupAxiomBuilder(gen);
-
- Namer = new SMTLibNamer();
- ctx.parent = this;
- this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);
-
- SetupProcess();
-
- if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)
- {
- // Prepare for ApiChecker usage
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile("");
- }
- if (CommandLineOptions.Clo.ContractInfer)
- {
- SendThisVC("(set-option :produce-unsat-cores true)");
- this.usingUnsatCore = true;
- }
- PrepareCommon();
- }
- }
-
- private void SetupAxiomBuilder(VCExpressionGenerator gen)
- {
- switch (CommandLineOptions.Clo.TypeEncodingMethod)
- {
- case CommandLineOptions.TypeEncoding.Arguments:
- AxBuilder = new TypeAxiomBuilderArguments(gen);
- AxBuilder.Setup();
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- AxBuilder = new TypeAxiomBuilderPremisses(gen);
- break;
- default:
- AxBuilder = new TypeAxiomBuilderPremisses(gen);
- AxBuilder.Setup();
- break;
- }
- }
-
- ProcessStartInfo ComputeProcessStartInfo()
- {
- var path = this.options.ProverPath;
- switch (options.Solver) {
- case SolverKind.Z3:
- if (path == null)
- path = Z3.ExecutablePath();
- return SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");
- case SolverKind.CVC3:
- if (path == null)
- path = "cvc3";
- return SMTLibProcess.ComputerProcessStartInfo(path, "-lang smt2 +interactive -showPrompt");
- case SolverKind.CVC4:
- if (path == null)
- path = "cvc4";
- return SMTLibProcess.ComputerProcessStartInfo(path, "--smtlib2 --no-strict-parsing");
- default:
- Debug.Assert(false);
- return null;
- }
- }
-
- void SetupProcess()
- {
- if (Process != null) return;
-
- var psi = ComputeProcessStartInfo();
- Process = new SMTLibProcess(psi, this.options);
- Process.ErrorHandler += this.HandleProverError;
- }
-
-
- void PossiblyRestart()
- {
- if (Process != null && Process.NeedsRestart) {
- Process.Close();
- Process = null;
- SetupProcess();
- Process.Send(common.ToString());
- }
- }
-
- public override ProverContext Context
- {
- get
- {
- Contract.Ensures(Contract.Result<ProverContext>() != null);
-
- return ctx;
- }
- }
-
- internal TypeAxiomBuilder AxBuilder { get; private set; }
- internal readonly UniqueNamer Namer;
- readonly TypeDeclCollector DeclCollector;
- SMTLibProcess Process;
- readonly List<string> proverErrors = new List<string>();
- readonly List<string> proverWarnings = new List<string>();
- readonly StringBuilder common = new StringBuilder();
- TextWriter currentLogFile;
- volatile ErrorHandler currentErrorHandler;
-
- private void FeedTypeDeclsToProver()
- {
- foreach (string s in DeclCollector.GetNewDeclarations()) {
- Contract.Assert(s != null);
- AddTypeDecl(s);
- }
- }
-
- private string Sanitize(string msg)
- {
- var idx = msg.IndexOf('\n');
- if (idx > 0)
- msg = msg.Replace("\r", "").Replace("\n", "\r\n");
- return msg;
- }
-
- private void SendCommon(string s)
- {
- Send(s, true);
- }
-
- private void SendThisVC(string s)
- {
- Send(s, false);
- }
-
- private void Send(string s, bool isCommon)
- {
- s = Sanitize(s);
-
- if (isCommon)
- common.Append(s).Append("\r\n");
-
- if (Process != null)
- Process.Send(s);
- if (currentLogFile != null)
- currentLogFile.WriteLine(s);
- }
-
- private void FindDependentTypes(Type type, List<CtorType> dependentTypes)
- {
- MapType mapType = type as MapType;
- if (mapType != null)
- {
- foreach (Type t in mapType.Arguments)
- {
- FindDependentTypes(t, dependentTypes);
- }
- FindDependentTypes(mapType.Result, dependentTypes);
- }
- CtorType ctorType = type as CtorType;
- if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey(ctorType))
- {
- dependentTypes.Add(ctorType);
- }
- }
-
- private void PrepareCommon()
- {
- if (common.Length == 0)
- {
- SendCommon("(set-option :print-success false)");
- SendCommon("(set-info :smt-lib-version 2.0)");
- if (options.ProduceModel())
- SendCommon("(set-option :produce-models true)");
- foreach (var opt in options.SmtOptions)
- {
- SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
- }
-
- if (!string.IsNullOrEmpty(options.Logic))
- {
- SendCommon("(set-logic " + options.Logic + ")");
- }
-
- SendCommon("; done setting options\n");
- SendCommon(_backgroundPredicates);
-
- if (options.UseTickleBool)
- {
- SendCommon("(declare-fun tickleBool (Bool) Bool)");
- SendCommon("(assert (and (tickleBool true) (tickleBool false)))");
- }
-
- if (ctx.KnownDatatypeConstructors.Count > 0)
- {
- GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();
- foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys)
- {
- dependencyGraph.AddSource(datatype);
- foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
- {
- List<CtorType> dependentTypes = new List<CtorType>();
- foreach (Variable v in f.InParams)
- {
- FindDependentTypes(v.TypedIdent.Type, dependentTypes);
- }
- foreach (CtorType result in dependentTypes)
- {
- dependencyGraph.AddEdge(datatype, result);
- }
- }
- }
- GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType>(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);
- sccs.Compute();
- foreach (GraphUtil.SCC<CtorType> scc in sccs)
- {
- string datatypeString = "";
- foreach (CtorType datatype in scc)
- {
- datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";
- foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
- {
- string quotedConstructorName = Namer.GetQuotedName(f, f.Name);
- if (f.InParams.Length == 0)
- {
- datatypeString += quotedConstructorName + " ";
- }
- else
- {
- datatypeString += "(" + quotedConstructorName + " ";
- foreach (Variable v in f.InParams)
- {
- string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);
- datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
- }
- datatypeString += ") ";
- }
- }
- datatypeString += ") ";
- }
- List<string> decls = DeclCollector.GetNewDeclarations();
- foreach (string decl in decls)
- {
- SendCommon(decl);
- }
- SendCommon("(declare-datatypes () (" + datatypeString + "))");
- }
- }
- }
-
- if (!AxiomsAreSetup)
- {
- var axioms = ctx.Axioms;
- var nary = axioms as VCExprNAry;
- if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
- foreach (var expr in nary.UniformArguments)
- {
- var str = VCExpr2String(expr, -1);
- if (str != "true")
- AddAxiom(str);
- }
- else
- AddAxiom(VCExpr2String(axioms, -1));
- AxiomsAreSetup = true;
- }
- }
-
- public override int FlushAxiomsToTheoremProver()
- {
- // we feed the axioms when begincheck is called.
- return 0;
- }
-
- private void FlushAxioms()
- {
- TypeDecls.Iter(SendCommon);
- TypeDecls.Clear();
- foreach (string s in Axioms) {
- Contract.Assert(s != null);
- if (s != "true")
- SendCommon("(assert " + s + ")");
- }
- Axioms.Clear();
- //FlushPushedAssertions();
- }
-
- private void CloseLogFile()
- {
- if (currentLogFile != null) {
- currentLogFile.Close();
- currentLogFile = null;
- }
- }
-
- private void FlushLogFile()
- {
- if (currentLogFile != null) {
- currentLogFile.Flush();
- }
- }
-
- public override void Close()
- {
- base.Close();
- CloseLogFile();
- if (Process != null)
- Process.Close();
- }
-
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- rpfp = null;
-
- if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen
-
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile(descriptiveName);
- currentLogFile.Write(common.ToString());
- }
-
- PrepareCommon();
- string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
- FlushAxioms();
-
- PossiblyRestart();
-
- SendThisVC("(push 1)");
- SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
- SendThisVC(vcString);
- FlushLogFile();
-
- if (Process != null) {
- Process.PingPong(); // flush any errors
-
- if (Process.Inspector != null)
- Process.Inspector.NewProblem(descriptiveName, vc, handler);
- }
-
- SendThisVC("(check-sat)");
- FlushLogFile();
- }
-
- public override void Reset()
- {
- SendThisVC("(reset)");
+ public class SMTLibProcessTheoremProver : ProverInterface
+ {
+ private readonly SMTLibProverContext ctx;
+ private readonly VCExpressionGenerator gen;
+ private readonly SMTLibProverOptions options;
+ private bool usingUnsatCore;
+ private RPFP rpfp = null;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant ()
+ {
+ Contract.Invariant (ctx != null);
+ Contract.Invariant (AxBuilder != null);
+ Contract.Invariant (Namer != null);
+ Contract.Invariant (DeclCollector != null);
+ Contract.Invariant (cce.NonNullElements (Axioms));
+ Contract.Invariant (cce.NonNullElements (TypeDecls));
+ Contract.Invariant (_backgroundPredicates != null);
+
+ }
+
+ [NotDelayed]
+ public SMTLibProcessTheoremProver (ProverOptions options, VCExpressionGenerator gen,
+ SMTLibProverContext ctx)
+ {
+ Contract.Requires (options != null);
+ Contract.Requires (gen != null);
+ Contract.Requires (ctx != null);
+ InitializeGlobalInformation ("UnivBackPred2.smt2");
+
+ this.options = (SMTLibProverOptions)options;
+ this.ctx = ctx;
+ this.gen = gen;
+ this.usingUnsatCore = false;
+
+ SetupAxiomBuilder (gen);
+
+ Namer = new SMTLibNamer ();
+ ctx.parent = this;
+ this.DeclCollector = new TypeDeclCollector ((SMTLibProverOptions)options, Namer);
+
+ SetupProcess ();
+
+ if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer) {
+ // Prepare for ApiChecker usage
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile ("");
+ }
+ if (CommandLineOptions.Clo.ContractInfer) {
+ SendThisVC ("(set-option :produce-unsat-cores true)");
+ this.usingUnsatCore = true;
+ }
+ PrepareCommon ();
+ }
+ }
+
+ private void SetupAxiomBuilder (VCExpressionGenerator gen)
+ {
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ AxBuilder = new TypeAxiomBuilderArguments (gen);
+ AxBuilder.Setup ();
+ break;
+ case CommandLineOptions.TypeEncoding.Monomorphic:
+ AxBuilder = new TypeAxiomBuilderPremisses (gen);
+ break;
+ default:
+ AxBuilder = new TypeAxiomBuilderPremisses (gen);
+ AxBuilder.Setup ();
+ break;
+ }
+ }
+
+ ProcessStartInfo ComputeProcessStartInfo ()
+ {
+ var path = this.options.ProverPath;
+ switch (options.Solver) {
+ case SolverKind.Z3:
+ if (path == null)
+ path = Z3.ExecutablePath ();
+ return SMTLibProcess.ComputerProcessStartInfo (path, "AUTO_CONFIG=false -smt2 -in");
+ case SolverKind.CVC4:
+ if (path == null)
+ path = "cvc4";
+ return SMTLibProcess.ComputerProcessStartInfo (path, "--lang=smt --no-strict-parsing --no-condense-function-values --incremental");
+ default:
+ Debug.Assert (false);
+ return null;
+ }
+ }
+
+ void SetupProcess ()
+ {
+ if (Process != null)
+ return;
+
+ var psi = ComputeProcessStartInfo ();
+ Process = new SMTLibProcess (psi, this.options);
+ Process.ErrorHandler += this.HandleProverError;
+ }
+
+ void PossiblyRestart ()
+ {
+ if (Process != null && Process.NeedsRestart) {
+ Process.Close ();
+ Process = null;
+ SetupProcess ();
+ Process.Send (common.ToString ());
+ }
+ }
+
+ public override ProverContext Context {
+ get {
+ Contract.Ensures (Contract.Result<ProverContext> () != null);
+
+ return ctx;
+ }
+ }
+
+ internal TypeAxiomBuilder AxBuilder { get; private set; }
+
+ internal readonly UniqueNamer Namer;
+ readonly TypeDeclCollector DeclCollector;
+ SMTLibProcess Process;
+ readonly List<string> proverErrors = new List<string> ();
+ readonly List<string> proverWarnings = new List<string> ();
+ readonly StringBuilder common = new StringBuilder ();
+ TextWriter currentLogFile;
+ volatile ErrorHandler currentErrorHandler;
+
+ private void FeedTypeDeclsToProver ()
+ {
+ foreach (string s in DeclCollector.GetNewDeclarations()) {
+ Contract.Assert (s != null);
+ AddTypeDecl (s);
+ }
+ }
+
+ private string Sanitize (string msg)
+ {
+ var idx = msg.IndexOf ('\n');
+ if (idx > 0)
+ msg = msg.Replace ("\r", "").Replace ("\n", "\r\n");
+ return msg;
+ }
+
+ private void SendCommon (string s)
+ {
+ Send (s, true);
+ }
+
+ private void SendThisVC (string s)
+ {
+ Send (s, false);
+ }
+
+ private void Send (string s, bool isCommon)
+ {
+ s = Sanitize (s);
+
+ if (isCommon)
+ common.Append (s).Append ("\r\n");
+
+ if (Process != null)
+ Process.Send (s);
+ if (currentLogFile != null)
+ currentLogFile.WriteLine (s);
+ }
+
+ private void FindDependentTypes (Type type, List<CtorType> dependentTypes)
+ {
+ MapType mapType = type as MapType;
+ if (mapType != null) {
+ foreach (Type t in mapType.Arguments) {
+ FindDependentTypes (t, dependentTypes);
+ }
+ FindDependentTypes (mapType.Result, dependentTypes);
+ }
+ CtorType ctorType = type as CtorType;
+ if (ctorType != null && ctx.KnownDatatypeConstructors.ContainsKey (ctorType)) {
+ dependentTypes.Add (ctorType);
+ }
+ }
+
+ private void PrepareCommon ()
+ {
+ if (common.Length == 0) {
+ SendCommon ("(set-option :print-success false)");
+ SendCommon ("(set-info :smt-lib-version 2.0)");
+ if (options.ProduceModel ())
+ SendCommon ("(set-option :produce-models true)");
+ foreach (var opt in options.SmtOptions) {
+ SendCommon ("(set-option :" + opt.Option + " " + opt.Value + ")");
+ }
+
+ if (!string.IsNullOrEmpty (options.Logic)) {
+ SendCommon ("(set-logic " + options.Logic + ")");
+ }
+
+ SendCommon ("; done setting options\n");
+ SendCommon (_backgroundPredicates);
+
+ if (options.UseTickleBool) {
+ SendCommon ("(declare-fun tickleBool (Bool) Bool)");
+ SendCommon ("(assert (and (tickleBool true) (tickleBool false)))");
+ }
+
+ if (ctx.KnownDatatypeConstructors.Count > 0) {
+ GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType> ();
+ foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {
+ dependencyGraph.AddSource (datatype);
+ foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
+ List<CtorType> dependentTypes = new List<CtorType> ();
+ foreach (Variable v in f.InParams) {
+ FindDependentTypes (v.TypedIdent.Type, dependentTypes);
+ }
+ foreach (CtorType result in dependentTypes) {
+ dependencyGraph.AddEdge (datatype, result);
+ }
+ }
+ }
+ GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType> (dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);
+ sccs.Compute ();
+ foreach (GraphUtil.SCC<CtorType> scc in sccs) {
+ string datatypeString = "";
+ foreach (CtorType datatype in scc) {
+ datatypeString += "(" + SMTLibExprLineariser.TypeToString (datatype) + " ";
+ foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
+ string quotedConstructorName = Namer.GetQuotedName (f, f.Name);
+ if (f.InParams.Length == 0) {
+ datatypeString += quotedConstructorName + " ";
+ } else {
+ datatypeString += "(" + quotedConstructorName + " ";
+ foreach (Variable v in f.InParams) {
+ string quotedSelectorName = Namer.GetQuotedName (v, v.Name + "#" + f.Name);
+ datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg (v.TypedIdent.Type) + ") ";
+ }
+ datatypeString += ") ";
+ }
+ }
+ datatypeString += ") ";
+ }
+ List<string> decls = DeclCollector.GetNewDeclarations ();
+ foreach (string decl in decls) {
+ SendCommon (decl);
+ }
+ SendCommon ("(declare-datatypes () (" + datatypeString + "))");
+ }
+ }
+ }
+
+ if (!AxiomsAreSetup) {
+ var axioms = ctx.Axioms;
+ var nary = axioms as VCExprNAry;
+ if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
+ foreach (var expr in nary.UniformArguments) {
+ var str = VCExpr2String (expr, -1);
+ if (str != "true")
+ AddAxiom (str);
+ }
+ else
+ AddAxiom (VCExpr2String (axioms, -1));
+ AxiomsAreSetup = true;
+ }
+ }
+
+ public override int FlushAxiomsToTheoremProver ()
+ {
+ // we feed the axioms when begincheck is called.
+ return 0;
+ }
+
+ private void FlushAxioms ()
+ {
+ TypeDecls.Iter (SendCommon);
+ TypeDecls.Clear ();
+ foreach (string s in Axioms) {
+ Contract.Assert (s != null);
+ if (s != "true")
+ SendCommon ("(assert " + s + ")");
+ }
+ Axioms.Clear ();
+ //FlushPushedAssertions();
+ }
+
+ private void CloseLogFile ()
+ {
+ if (currentLogFile != null) {
+ currentLogFile.Close ();
+ currentLogFile = null;
+ }
+ }
+
+ private void FlushLogFile ()
+ {
+ if (currentLogFile != null) {
+ currentLogFile.Flush ();
+ }
+ }
+
+ public override void Close ()
+ {
+ base.Close ();
+ CloseLogFile ();
+ if (Process != null)
+ Process.Close ();
+ }
+
+ public override void BeginCheck (string descriptiveName, VCExpr vc, ErrorHandler handler)
+ {
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ rpfp = null;
+
+ if (options.SeparateLogFiles)
+ CloseLogFile (); // shouldn't really happen
+
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile (descriptiveName);
+ currentLogFile.Write (common.ToString ());
+ }
+
+ PrepareCommon ();
+ string vcString = "(assert (not\n" + VCExpr2String (vc, 1) + "\n))";
+ FlushAxioms ();
+
+ PossiblyRestart ();
+
+ SendThisVC ("(push 1)");
+ SendThisVC ("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId (descriptiveName) + ")");
+ SendThisVC (vcString);
+ FlushLogFile ();
+
+ if (Process != null) {
+ Process.PingPong (); // flush any errors
+
+ if (Process.Inspector != null)
+ Process.Inspector.NewProblem (descriptiveName, vc, handler);
+ }
+
+ SendThisVC ("(check-sat)");
+ FlushLogFile ();
+ }
+
+ public override void Reset ()
+ {
+ if (options.Solver == SolverKind.Z3) {
+ SendThisVC ("(reset)");
- if (0 < common.Length)
- {
- var c = common.ToString();
- Process.Send(c);
- if (currentLogFile != null)
- {
- currentLogFile.WriteLine(c);
- }
- }
- }
-
- public override void FullReset()
- {
- Namer.Reset();
- common.Clear();
- SetupAxiomBuilder(gen);
- Axioms.Clear();
- TypeDecls.Clear();
- AxiomsAreSetup = false;
- ctx.Reset();
- ctx.KnownDatatypeConstructors.Clear();
- ctx.parent = this;
- DeclCollector.Reset();
- SendThisVC("; doing a full reset...");
- }
-
- private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler,
- Dictionary<int,Dictionary<string,string>> varSubst)
- {
- Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node>();
- Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node>();
-
- foreach(var node in rpfp.nodes)
- pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name,node);
-
- RPFP.Node topnode = null;
- var lines = resp.Arguments;
-
- // last line of derivation is from query, skip it
- for (int i = 0; i < lines.Length-1; i++)
- {
- var line = lines[i];
- if (line.ArgCount != 6)
- {
- HandleProverError("bad derivation line from prover: " + line.ToString());
- return null;
- }
- var name = line[0];
- var conseq = line[1];
- var rule = line[2];
- var subst = line[3];
- var labs = line[4];
- var refs = line[5];
- var predName = conseq.Name;
- {
- string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
- int pos = predName.LastIndexOf(spacer);
- if (pos >= 0)
- predName = predName.Substring(0, pos);
- }
- RPFP.Node node = null;
- if (!pmap.TryGetValue(predName, out node))
- {
- HandleProverError("unknown predicate from prover: " + predName.ToString());
- return null;
- }
- RPFP.Node cexnode = rpfp.CloneNode(node);
- cexnode.map = node;
- nmap.Add(name.Name, cexnode);
- List<RPFP.Node> Chs = new List<RPFP.Node>();
-
- if (refs.Name != "ref")
- {
- HandleProverError("bad references from prover: " + refs.ToString());
- return null;
- }
- foreach (var c in refs.Arguments)
- {
- if (c.Name == "true")
- Chs.Add(null);
- else
- {
- RPFP.Node ch = null;
- if (!nmap.TryGetValue(c.Name, out ch))
- {
- HandleProverError("unknown reference from prover: " + c.ToString());
- return null;
- }
- Chs.Add(ch);
- }
- }
-
- if (!rule.Name.StartsWith("rule!"))
- {
- HandleProverError("bad rule name from prover: " + refs.ToString());
- return null;
- }
- int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;
- if (ruleNum < 0 || ruleNum > rpfp.edges.Count)
- {
- HandleProverError("bad rule name from prover: " + refs.ToString());
- return null;
- }
- RPFP.Edge orig_edge = rpfp.edges[ruleNum];
- RPFP.Edge e = rpfp.CreateEdge(cexnode, orig_edge.F, Chs.ToArray());
- e.map = orig_edge;
- topnode = cexnode;
-
- if (labs.Name != "labels")
- {
- HandleProverError("bad labels from prover: " + labs.ToString());
- return null;
- }
- e.labels = new HashSet<string>();
- foreach (var l in labs.Arguments)
- e.labels.Add(l.Name);
-
- if (subst.Name != "subst")
- {
- HandleProverError("bad subst from prover: " + subst.ToString());
- return null;
- }
- Dictionary<string, string> dict = new Dictionary<string, string>();
- varSubst[e.number] = dict;
- foreach (var s in subst.Arguments)
- {
- if (s.Name != "=" || s.Arguments.Length != 2)
- {
- HandleProverError("bad equation from prover: " + s.ToString());
- return null;
- }
- string uniqueName = s.Arguments[0].Name;
- string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
- int pos = uniqueName.LastIndexOf(spacer);
- if (pos >= 0)
- uniqueName = uniqueName.Substring(0, pos);
- dict.Add(uniqueName, s.Arguments[1].ToString());
- }
-
- }
- if (topnode == null)
- {
- HandleProverError("empty derivation from prover: " + resp.ToString());
- }
- return topnode;
- }
-
- private Model SExprToModel(SExpr resp, ErrorHandler handler)
- {
- // Concatenate all the arguments
- string modelString = resp[0].Name;
- // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"
- var models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelString));
- if (models == null || models.Count == 0)
- {
- HandleProverError("no model from prover: " + resp.ToString());
- }
- return models[0];
- }
-
- private string QuantifiedVCExpr2String(VCExpr x)
- {
- return VCExpr2String(x, 1);
+ if (0 < common.Length) {
+ var c = common.ToString ();
+ Process.Send (c);
+ if (currentLogFile != null) {
+ currentLogFile.WriteLine (c);
+ }
+ }
+ }
+ }
+
+ public override void FullReset ()
+ {
+ if (options.Solver == SolverKind.Z3) {
+ Namer.Reset ();
+ common.Clear ();
+ SetupAxiomBuilder (gen);
+ Axioms.Clear ();
+ TypeDecls.Clear ();
+ AxiomsAreSetup = false;
+ ctx.Reset ();
+ ctx.KnownDatatypeConstructors.Clear ();
+ ctx.parent = this;
+ DeclCollector.Reset ();
+ SendThisVC ("; doing a full reset...");
+ }
+ }
+
+ private RPFP.Node SExprToCex (SExpr resp, ErrorHandler handler,
+ Dictionary<int,Dictionary<string,string>> varSubst)
+ {
+ Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node> ();
+ Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();
+
+ foreach (var node in rpfp.nodes)
+ pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);
+
+ RPFP.Node topnode = null;
+ var lines = resp.Arguments;
+
+ // last line of derivation is from query, skip it
+ for (int i = 0; i < lines.Length-1; i++) {
+ var line = lines [i];
+ if (line.ArgCount != 6) {
+ HandleProverError ("bad derivation line from prover: " + line.ToString ());
+ return null;
+ }
+ var name = line [0];
+ var conseq = line [1];
+ var rule = line [2];
+ var subst = line [3];
+ var labs = line [4];
+ var refs = line [5];
+ var predName = conseq.Name;
+ {
+ string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
+ int pos = predName.LastIndexOf (spacer);
+ if (pos >= 0)
+ predName = predName.Substring (0, pos);
+ }
+ RPFP.Node node = null;
+ if (!pmap.TryGetValue (predName, out node)) {
+ HandleProverError ("unknown predicate from prover: " + predName.ToString ());
+ return null;
+ }
+ RPFP.Node cexnode = rpfp.CloneNode (node);
+ cexnode.map = node;
+ nmap.Add (name.Name, cexnode);
+ List<RPFP.Node> Chs = new List<RPFP.Node> ();
+
+ if (refs.Name != "ref") {
+ HandleProverError ("bad references from prover: " + refs.ToString ());
+ return null;
+ }
+ foreach (var c in refs.Arguments) {
+ if (c.Name == "true")
+ Chs.Add (null);
+ else {
+ RPFP.Node ch = null;
+ if (!nmap.TryGetValue (c.Name, out ch)) {
+ HandleProverError ("unknown reference from prover: " + c.ToString ());
+ return null;
+ }
+ Chs.Add (ch);
+ }
+ }
+
+ if (!rule.Name.StartsWith ("rule!")) {
+ HandleProverError ("bad rule name from prover: " + refs.ToString ());
+ return null;
+ }
+ int ruleNum = Convert.ToInt32 (rule.Name.Substring (5)) - 1;
+ if (ruleNum < 0 || ruleNum > rpfp.edges.Count) {
+ HandleProverError ("bad rule name from prover: " + refs.ToString ());
+ return null;
+ }
+ RPFP.Edge orig_edge = rpfp.edges [ruleNum];
+ RPFP.Edge e = rpfp.CreateEdge (cexnode, orig_edge.F, Chs.ToArray ());
+ e.map = orig_edge;
+ topnode = cexnode;
+
+ if (labs.Name != "labels") {
+ HandleProverError ("bad labels from prover: " + labs.ToString ());
+ return null;
+ }
+ e.labels = new HashSet<string> ();
+ foreach (var l in labs.Arguments)
+ e.labels.Add (l.Name);
+
+ if (subst.Name != "subst") {
+ HandleProverError ("bad subst from prover: " + subst.ToString ());
+ return null;
+ }
+ Dictionary<string, string> dict = new Dictionary<string, string> ();
+ varSubst [e.number] = dict;
+ foreach (var s in subst.Arguments) {
+ if (s.Name != "=" || s.Arguments.Length != 2) {
+ HandleProverError ("bad equation from prover: " + s.ToString ());
+ return null;
+ }
+ string uniqueName = s.Arguments [0].Name;
+ string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!
+ int pos = uniqueName.LastIndexOf (spacer);
+ if (pos >= 0)
+ uniqueName = uniqueName.Substring (0, pos);
+ dict.Add (uniqueName, s.Arguments [1].ToString ());
+ }
+
+ }
+ if (topnode == null) {
+ HandleProverError ("empty derivation from prover: " + resp.ToString ());
+ }
+ return topnode;
+ }
+
+ private Model SExprToModel (SExpr resp, ErrorHandler handler)
+ {
+ // Concatenate all the arguments
+ string modelString = resp [0].Name;
+ // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"
+ var models = Model.ParseModels (new StringReader ("Z3 error model: \n" + modelString), "");
+ if (models == null || models.Count == 0) {
+ HandleProverError ("no model from prover: " + resp.ToString ());
+ }
+ return models [0];
+ }
+
+ private string QuantifiedVCExpr2String (VCExpr x)
+ {
+ return VCExpr2String (x, 1);
#if false
if (!(x is VCExprQuantifier))
return VCExpr2String(x, 1);
@@ -594,122 +549,112 @@ namespace Microsoft.Boogie.SMTLib
string res = wr.ToString();
return res;
#endif
- }
-
- public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler,
- out RPFP.Node cex,
- Dictionary<int,Dictionary<string,string>> varSubst)
- {
- //Contract.Requires(descriptiveName != null);
- //Contract.Requires(vc != null);
- //Contract.Requires(handler != null);
- rpfp = _rpfp;
- cex = null;
-
- if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen
-
- if (options.LogFilename != null && currentLogFile == null)
- {
- currentLogFile = OpenOutputFile(descriptiveName);
- currentLogFile.Write(common.ToString());
- }
-
- Push();
- SendThisVC("(fixedpoint-push)");
- foreach (var node in rpfp.nodes)
- {
- DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);
- }
-
- PrepareCommon();
-
- LineariserOptions.Default.LabelsBelowQuantifiers = true;
- List<string> ruleStrings = new List<string>();
- foreach (var edge in rpfp.edges)
- {
- string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";
- ruleStrings.Add(ruleString);
- }
- string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n :engine duality\n :print-certificate true\n";
+ }
+
+ public override Outcome CheckRPFP (string descriptiveName, RPFP _rpfp, ErrorHandler handler,
+ out RPFP.Node cex,
+ Dictionary<int,Dictionary<string,string>> varSubst)
+ {
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ rpfp = _rpfp;
+ cex = null;
+
+ if (options.SeparateLogFiles)
+ CloseLogFile (); // shouldn't really happen
+
+ if (options.LogFilename != null && currentLogFile == null) {
+ currentLogFile = OpenOutputFile (descriptiveName);
+ currentLogFile.Write (common.ToString ());
+ }
+
+ Push ();
+ SendThisVC ("(fixedpoint-push)");
+ foreach (var node in rpfp.nodes) {
+ DeclCollector.RegisterRelation ((node.Name as VCExprBoogieFunctionOp).Func);
+ }
+
+ PrepareCommon ();
+
+ LineariserOptions.Default.LabelsBelowQuantifiers = true;
+ List<string> ruleStrings = new List<string> ();
+ foreach (var edge in rpfp.edges) {
+ string ruleString = "(rule " + QuantifiedVCExpr2String (rpfp.GetRule (edge)) + "\n)";
+ ruleStrings.Add (ruleString);
+ }
+ string queryString = "(query " + QuantifiedVCExpr2String (rpfp.GetQuery ()) + "\n :engine duality\n :print-certificate true\n";
#if true
- if (CommandLineOptions.Clo.StratifiedInlining != 0)
- queryString += " :stratified-inlining true\n";
- if (CommandLineOptions.Clo.RecursionBound > 0)
- queryString += " :recursion-bound " + Convert.ToString(CommandLineOptions.Clo.RecursionBound) + "\n";
+ if (CommandLineOptions.Clo.StratifiedInlining != 0)
+ queryString += " :stratified-inlining true\n";
+ if (CommandLineOptions.Clo.RecursionBound > 0)
+ queryString += " :recursion-bound " + Convert.ToString (CommandLineOptions.Clo.RecursionBound) + "\n";
#endif
- queryString += ")";
- LineariserOptions.Default.LabelsBelowQuantifiers = false;
- FlushAxioms();
+ queryString += ")";
+ LineariserOptions.Default.LabelsBelowQuantifiers = false;
+ FlushAxioms ();
- PossiblyRestart();
+ PossiblyRestart ();
- SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
- foreach(var rs in ruleStrings)
- SendThisVC(rs);
- FlushLogFile();
+ SendThisVC ("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId (descriptiveName) + ")");
+ foreach (var rs in ruleStrings)
+ SendThisVC (rs);
+ FlushLogFile ();
- if (Process != null)
- {
- Process.PingPong(); // flush any errors
+ if (Process != null) {
+ Process.PingPong (); // flush any errors
#if false
// TODO: this is not going to work
if (Process.Inspector != null)
Process.Inspector.NewProblem(descriptiveName, vc, handler);
#endif
- }
+ }
- SendThisVC(queryString);
- FlushLogFile();
+ SendThisVC (queryString);
+ FlushLogFile ();
- var result = Outcome.Undetermined;
+ var result = Outcome.Undetermined;
- if (Process != null)
- {
+ if (Process != null) {
- var resp = Process.GetProverResponse();
+ var resp = Process.GetProverResponse ();
- switch (resp.Name)
- {
- case "unsat":
- result = Outcome.Valid;
- break;
- case "sat":
- result = Outcome.Invalid;
- break;
- case "unknown":
- result = Outcome.Invalid;
- break;
- default:
- HandleProverError("Unexpected prover response: " + resp.ToString());
- break;
- }
+ switch (resp.Name) {
+ case "unsat":
+ result = Outcome.Valid;
+ break;
+ case "sat":
+ result = Outcome.Invalid;
+ break;
+ case "unknown":
+ result = Outcome.Invalid;
+ break;
+ default:
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ break;
+ }
- switch (result)
- {
- case Outcome.Invalid:
- {
- resp = Process.GetProverResponse();
- if (resp.Name == "derivation")
- {
- cex = SExprToCex(resp, handler,varSubst);
- }
- else
- HandleProverError("Unexpected prover response: " + resp.ToString());
- resp = Process.GetProverResponse();
- if (resp.Name == "model")
- {
- var model = SExprToModel(resp, handler);
- cex.owner.SetBackgroundModel(model);
- }
- else
- HandleProverError("Unexpected prover response: " + resp.ToString());
- break;
- }
- default:
- break;
- }
+ switch (result) {
+ case Outcome.Invalid:
+ {
+ resp = Process.GetProverResponse ();
+ if (resp.Name == "derivation") {
+ cex = SExprToCex (resp, handler, varSubst);
+ } else
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ resp = Process.GetProverResponse ();
+ if (resp.Name == "model") {
+ var model = SExprToModel (resp, handler);
+ cex.owner.SetBackgroundModel (model);
+ } else
+ HandleProverError ("Unexpected prover response: " + resp.ToString ());
+ break;
+ }
+ default:
+ break;
+ }
#if false
while (true)
@@ -720,121 +665,121 @@ namespace Microsoft.Boogie.SMTLib
HandleProverError("Unexpected prover response: " + resp.ToString());
}
#endif
- }
- SendThisVC("(fixedpoint-pop)");
- Pop();
- AxiomsAreSetup = false;
- return result;
- }
-
- private static HashSet<string> usedLogNames = new HashSet<string>();
-
- private TextWriter OpenOutputFile(string descriptiveName)
- {
- Contract.Requires(descriptiveName != null);
- Contract.Ensures(Contract.Result<TextWriter>() != null);
-
- string filename = options.LogFilename;
- filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
- var curFilename = filename;
-
- lock (usedLogNames) {
- int n = 1;
- while (usedLogNames.Contains(curFilename)) {
- curFilename = filename + "." + n++;
- }
- usedLogNames.Add(curFilename);
- }
-
- return new StreamWriter(curFilename, false);
- }
-
- private void FlushProverWarnings()
- {
- var handler = currentErrorHandler;
- if (handler != null) {
- lock (proverWarnings) {
- proverWarnings.Iter(handler.OnProverWarning);
- proverWarnings.Clear();
- }
- }
- }
-
- private void HandleProverError(string s)
- {
- s = s.Replace("\r", "");
- lock (proverWarnings) {
- while (s.StartsWith("WARNING: ")) {
- var idx = s.IndexOf('\n');
- var warn = s;
- if (idx > 0) {
- warn = s.Substring(0, idx);
- s = s.Substring(idx + 1);
- } else {
- s = "";
- }
- warn = warn.Substring(9);
- proverWarnings.Add(warn);
- }
- }
-
- FlushProverWarnings();
-
- if (s == "") return;
-
- lock (proverErrors) {
- proverErrors.Add(s);
- Console.WriteLine("Prover error: " + s);
- }
- }
-
- [NoDefaultContract]
- public override Outcome CheckOutcome(ErrorHandler handler)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- var result = CheckOutcomeCore(handler);
- SendThisVC("(pop 1)");
- FlushLogFile();
+ }
+ SendThisVC ("(fixedpoint-pop)");
+ Pop ();
+ AxiomsAreSetup = false;
+ return result;
+ }
+
+ private static HashSet<string> usedLogNames = new HashSet<string> ();
+
+ private TextWriter OpenOutputFile (string descriptiveName)
+ {
+ Contract.Requires (descriptiveName != null);
+ Contract.Ensures (Contract.Result<TextWriter> () != null);
+
+ string filename = options.LogFilename;
+ filename = Helpers.SubstituteAtPROC (descriptiveName, cce.NonNull (filename));
+ var curFilename = filename;
+
+ lock (usedLogNames) {
+ int n = 1;
+ while (usedLogNames.Contains(curFilename)) {
+ curFilename = filename + "." + n++;
+ }
+ usedLogNames.Add (curFilename);
+ }
+
+ return new StreamWriter (curFilename, false);
+ }
+
+ private void FlushProverWarnings ()
+ {
+ var handler = currentErrorHandler;
+ if (handler != null) {
+ lock (proverWarnings) {
+ proverWarnings.Iter (handler.OnProverWarning);
+ proverWarnings.Clear ();
+ }
+ }
+ }
+
+ private void HandleProverError (string s)
+ {
+ s = s.Replace ("\r", "");
+ lock (proverWarnings) {
+ while (s.StartsWith("WARNING: ")) {
+ var idx = s.IndexOf ('\n');
+ var warn = s;
+ if (idx > 0) {
+ warn = s.Substring (0, idx);
+ s = s.Substring (idx + 1);
+ } else {
+ s = "";
+ }
+ warn = warn.Substring (9);
+ proverWarnings.Add (warn);
+ }
+ }
+
+ FlushProverWarnings ();
+
+ if (s == "")
+ return;
+
+ lock (proverErrors) {
+ proverErrors.Add (s);
+ Console.WriteLine ("Prover error: " + s);
+ }
+ }
+
+ [NoDefaultContract]
+ public override Outcome CheckOutcome (ErrorHandler handler)
+ {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException> (true);
+
+ var result = CheckOutcomeCore (handler);
+ SendThisVC ("(pop 1)");
+ FlushLogFile ();
+
+ return result;
+ }
+
+ [NoDefaultContract]
+ public override Outcome CheckOutcomeCore (ErrorHandler handler)
+ {
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException> (true);
+
+ var result = Outcome.Undetermined;
- return result;
- }
+ if (Process == null)
+ return result;
- [NoDefaultContract]
- public override Outcome CheckOutcomeCore(ErrorHandler handler)
- {
- Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
-
- var result = Outcome.Undetermined;
+ try {
+ currentErrorHandler = handler;
+ FlushProverWarnings ();
- if (Process == null)
- return result;
+ var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
+ if (errorsLeft < 1)
+ errorsLeft = 1;
- try {
- currentErrorHandler = handler;
- FlushProverWarnings();
+ var globalResult = Outcome.Undetermined;
- var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;
- if (errorsLeft < 1)
- errorsLeft = 1;
+ while (true) {
+ errorsLeft--;
+ string[] labels = null;
- var globalResult = Outcome.Undetermined;
+ result = GetResponse ();
+ if (globalResult == Outcome.Undetermined)
+ globalResult = result;
- while (true) {
- errorsLeft--;
- string[] labels = null;
-
- result = GetResponse();
- if (globalResult == Outcome.Undetermined)
- globalResult = result;
-
- if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {
- IList<string> xlabels;
- if (CommandLineOptions.Clo.UseLabels) {
- labels = GetLabelsInfo();
- if (labels == null)
- {
- xlabels = new string[] { };
+ if (result == Outcome.Invalid || result == Outcome.TimeOut || result == Outcome.OutOfMemory) {
+ IList<string> xlabels;
+ if (CommandLineOptions.Clo.UseLabels) {
+ labels = GetLabelsInfo ();
+ if (labels == null) {
+ xlabels = new string[] { };
}
else
{
@@ -905,6 +850,8 @@ namespace Microsoft.Boogie.SMTLib
else if (resp.ArgCount != 0)
break;
path.Add(v);
+ if (v.Equals("0"))
+ throw new UnexpectedProverOutputException("because of (get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");
SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");
}
return path.ToArray();
@@ -925,7 +872,11 @@ namespace Microsoft.Boogie.SMTLib
string modelStr = null;
if (resp.Name == "model" && resp.ArgCount >= 1) {
- modelStr = resp[0].Name;
+ modelStr = resp.Arguments[0] + "\n";
+ for (int i = 1; i < resp.ArgCount; i++) {
+ if (resp.Arguments[i].ToString().Contains("define-fun") &&!resp.Arguments[i].ToString().Contains("not"))
+ modelStr += resp.Arguments[i] + "\n";
+ }
}
else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {
modelStr = resp.Name;
@@ -934,9 +885,23 @@ namespace Microsoft.Boogie.SMTLib
HandleProverError("Unexpected prover response getting model: " + resp.ToString());
}
List<Model> models = null;
- try {
- models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));
- }
+ try {
+ switch (options.Solver) {
+ case SolverKind.Z3:
+ if (options.SMTLib2Model) {
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");
+ } else {
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "");
+ }
+ break;
+ case SolverKind.CVC4:
+ models = Model.ParseModels(new StringReader("Error model: \n" + modelStr), "SMTLIB2");
+ break;
+ default:
+ Debug.Assert(false);
+ return null;
+ }
+ }
catch (ArgumentException exn) {
HandleProverError("Model parsing error: " + exn.Message);
}
diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index c58d3349..bc1b7e02 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for SMTLib.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
@@ -157,6 +161,7 @@
<Compile Include="TypeDeclCollector.cs" />
<Compile Include="..\..\version.cs" />
<Compile Include="Z3.cs" />
+ <Compile Include="CVC4.cs" />
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
@@ -172,7 +177,7 @@
<Name>Core</Name>
</ProjectReference>
<ProjectReference Include="..\..\Graph\Graph.csproj">
- <Project>{69a2b0b8-bcac-4101-ae7a-556fcc58c06e}</Project>
+ <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>
<Name>Graph</Name>
</ProjectReference>
<ProjectReference Include="..\..\Model\Model.csproj">
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index d336252e..84d0ba47 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -27,7 +27,7 @@ namespace Microsoft.Boogie.SMTLib
}
}
- public enum SolverKind { Z3, CVC3, CVC4 };
+ public enum SolverKind { Z3, CVC4 };
public class SMTLibProverOptions : ProverOptions
{
@@ -43,6 +43,7 @@ namespace Microsoft.Boogie.SMTLib
// Z3 specific (at the moment; some of them make sense also for other provers)
public string Inspector = null;
public bool OptimizeForBv = false;
+ public bool SMTLib2Model = false;
public bool ProduceModel() {
return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate ||
@@ -89,16 +90,12 @@ namespace Microsoft.Boogie.SMTLib
case "z3":
Solver = SolverKind.Z3;
break;
- case "cvc3":
- Solver = SolverKind.CVC3;
- Logic = "ALL";
- break;
case "cvc4":
Solver = SolverKind.CVC4;
- Logic = "ALL_SUPPORTED";
+ Logic = "QF_ALL_SUPPORTED";
break;
default:
- ReportError("Invalid SOLVER value; must be 'z3', 'cvc3' or 'cvc4'");
+ ReportError("Invalid SOLVER value; must be 'z3' or 'cvc4'");
return false;
}
return true;
@@ -119,6 +116,7 @@ namespace Microsoft.Boogie.SMTLib
ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||
ParseString(opt, "INSPECTOR", ref Inspector) ||
ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
+ ParseBool(opt, "SMTLIB2_MODEL", ref SMTLib2Model) ||
ParseString(opt, "LOGIC", ref Logic) ||
base.Parse(opt);
}
@@ -138,18 +136,19 @@ namespace Microsoft.Boogie.SMTLib
@"
SMT-specific options:
~~~~~~~~~~~~~~~~~~~~~
-SOLVER=<string> Use the given SMT solver (z3, cvc3, cvc4; default: z3)
+SOLVER=<string> Use the given SMT solver (z3 or cvc4; default: z3)
USE_WEIGHTS=<bool> Pass :weight annotations on quantified formulas (default: true)
VERBOSITY=<int> 1 - print prover output (default: 0)
O:<name>=<value> Pass (set-option :<name> <value>) to the SMT solver.
C:<string> Pass <string> to the SMT on the command line.
-LOGIC=<string> Pass (set-logic <string>) to the prover (default: empty, 'ALL' for CVC3 or 'ALL_SUPPORTED' for CVC4)
+LOGIC=<string> Pass (set-logic <string>) to the prover (default: empty, 'ALL_SUPPORTED' for CVC4)
Z3-specific options:
~~~~~~~~~~~~~~~~~~~~
MULTI_TRACES=<bool> Report errors with multiple paths leading to the same assertion.
INSPECTOR=<string> Use the specified Z3Inspector binary.
OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
+SMTLIB2_MODEL=<bool> Use the SMTLIB2 output model. Defaults to false.
" + base.Help;
}
}
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 24071457..5865a333 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -283,9 +283,17 @@ namespace Microsoft.Boogie.SMTLib
//options.AddWeakSmtOption("MODEL_PARTIAL", "true");
//options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");
options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");
- options.AddWeakSmtOption("MODEL_V2", "true");
options.AddWeakSmtOption("ASYNC_COMMANDS", "false");
+ if (options.SMTLib2Model)
+ {
+ options.AddWeakSmtOption("pp-bv-literals", "false");;
+ }
+ else
+ {
+ options.AddWeakSmtOption("MODEL_V2", "true");
+ }
+
if (!options.OptimizeForBv)
{
// Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj
index bd426125..19873dbc 100644
--- a/Source/VCExpr/VCExpr.csproj
+++ b/Source/VCExpr/VCExpr.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for VCExpr.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 8afbf027..ad2b7e68 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -234,7 +234,7 @@ namespace Microsoft.Boogie {
Model m = Model;
ApplyRedirections(m);
- var mvstates = m.TryGetFunc("@MV_state");
+ var mvstates = m.TryGetFunc("$mv_state");
if (MvInfo == null || mvstates == null)
return m;
@@ -1700,11 +1700,11 @@ namespace VC {
{
public readonly List<Variable> AllVariables = new List<Variable>();
public readonly List<Mapping> CapturePoints = new List<Mapping>();
- public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "@MV_state",
+ public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "$mv_state",
new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),
new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));
- public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "@MV_state_const", Bpl.Type.Int));
+ public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "$mv_state_const", Bpl.Type.Int));
public ModelViewInfo(Program program, Implementation impl) {
Contract.Requires(program != null);
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index b4db817f..f90788d7 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2444,7 +2444,7 @@ namespace VC {
private void GetModelWithStates(Model m) {
if (m == null) return;
var mvInfo = mainInfo.mvInfo;
- var mvstates = m.TryGetFunc("@MV_state");
+ var mvstates = m.TryGetFunc("$mv_state");
if (mvstates == null)
return;
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index f724307b..a7be5827 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -97,6 +97,8 @@
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>Migrated rules for VCGeneration.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
<DebugSymbols>true</DebugSymbols>
@@ -137,6 +139,8 @@
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ <WarningLevel>4</WarningLevel>
+ <Optimize>false</Optimize>
</PropertyGroup>
<ItemGroup>
<Reference Include="System" />