Some changes to support expanded use of z3api.

Should not affect function
of other provers. There is an option added in Check.cs to  allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).

1 files changed, 65 insertions, 3 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 52714dc9..de5fecd8 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -40,7 +40,7 @@
     <DebugSymbols>true</DebugSymbols>

     <DebugType>full</DebugType>

     <Optimize>false</Optimize>

-    <OutputPath>..\..\Binaries\</OutputPath>

+    <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>

     <DefineConstants>TRACE;DEBUG</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

@@ -86,10 +86,10 @@
   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\z3apidebug\</OutputPath>

+    <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>

     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

+    <PlatformTarget>x86</PlatformTarget>

     <CodeAnalysisRuleAssemblies>

     </CodeAnalysisRuleAssemblies>

     <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

@@ -138,6 +138,68 @@
     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\x86\Debug\</OutputPath>

+    <DefineConstants>TRACE;DEBUG</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <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>

+  </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x86'">

+    <OutputPath>bin\x86\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <Optimize>true</Optimize>

+    <DebugType>pdbonly</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\Release\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <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>

+    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>

+  </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'z3apidebug|x86'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\x86\z3apidebug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>bin\z3apidebug\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>Migrated rules for BoogieDriver.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

+    <CodeAnalysisIgnoreBuiltInRuleSets>false</CodeAnalysisIgnoreBuiltInRuleSets>

+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

+  </PropertyGroup>

+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|x86'">

+    <DebugSymbols>true</DebugSymbols>

+    <OutputPath>bin\x86\Checked\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <DebugType>full</DebugType>

+    <PlatformTarget>x86</PlatformTarget>

+    <CodeAnalysisLogFile>..\..\Binaries\Boogie.exe.CodeAnalysisLog.xml</CodeAnalysisLogFile>

+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

+    <ErrorReport>prompt</ErrorReport>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets;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;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

+    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Data" />