From 8accc49386be42c1ef7ecd1a8df044d8f2ed60a9 Mon Sep 17 00:00:00 2001
From: Anh-Dung Phan <t-anphan@microsoft.com>
Date: Fri, 27 Dec 2013 11:39:50 -0800
Subject: [PATCH] Add a README for MSF plugin

---
 examples/msf/README                           | 20 ++++++++
 .../SolverFoundation.Plugin.Z3.csproj         | 50 ++-----------------
 examples/msf/Validator/Validator.csproj       | 30 ++---------
 3 files changed, 30 insertions(+), 70 deletions(-)
 create mode 100644 examples/msf/README

diff --git a/examples/msf/README b/examples/msf/README
new file mode 100644
index 000000000..ab69fb0fe
--- /dev/null
+++ b/examples/msf/README
@@ -0,0 +1,20 @@
+In order to use Z3 MSF plugin, follow the following steps:
+1. Compile latest Z3 .NET API (from any branch consisting of opt features) and copy 'libz3.dll' and 'Microsoft.Z3.dll' to the folder of 'Z3MSFPlugin.sln'.
+2. Retrieve 'Microsoft.Solver.Foundation.dll' from http://archive.msdn.microsoft.com/solverfoundation/Release/ProjectReleases.aspx?ReleaseId=1799,
+   preferably using DLL only version. Copy 'Microsoft.Solver.Foundation.dll' to the folder of 'Z3MSFPlugin.sln'
+3. Build 'Z3MSFPlugin.sln'
+
+The solution consists of a plugin project, a test project with a few simple test cases and a command line projects for external OML, MPS and SMPS models.
+To retrieve SMT2 models which are native to Z3, set the logging file in corresponding directives or solver params e.g.
+
+   var p = new Z3MILPParams();
+   p.SMT2LogFile = "model.smt2";
+
+For more details, check out the commands in 'Validator\Program.cs'.
+
+Enjoy!
+
+
+ 
+ 
+   
\ No newline at end of file
diff --git a/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj b/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj
index 6a4a22aec..9f6b71f34 100644
--- a/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj
+++ b/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj
@@ -14,11 +14,7 @@
     <FileAlignment>512</FileAlignment>
     <SignAssembly>false</SignAssembly>
     <AssemblyOriginatorKeyFile>
-    </AssemblyOriginatorKeyFile>
-    <FileUpgradeFlags>
-    </FileUpgradeFlags>
-    <OldToolsVersion>3.5</OldToolsVersion>
-    <UpgradeBackupLocation />
+    </AssemblyOriginatorKeyFile>    
     <PublishUrl>publish\</PublishUrl>
     <Install>true</Install>
     <InstallFrom>Disk</InstallFrom>
@@ -61,13 +57,7 @@
     <Optimize>true</Optimize>
     <DebugType>pdbonly</DebugType>
     <PlatformTarget>AnyCPU</PlatformTarget>
-    <CodeAnalysisLogFile>bin\Release\Z3Solver.dll.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>
-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
   </PropertyGroup>
   <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'commercial_64|AnyCPU'">
     <OutputPath>bin\commercial_64\</OutputPath>
@@ -75,15 +65,7 @@
     <Optimize>true</Optimize>
     <DebugType>pdbonly</DebugType>
     <PlatformTarget>AnyCPU</PlatformTarget>
-    <CodeAnalysisLogFile>bin\Release\Z3Solver.dll.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>
-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
-    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
   </PropertyGroup>
   <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x86'">
     <DebugSymbols>true</DebugSymbols>
@@ -119,8 +101,6 @@
     <DebugType>pdbonly</DebugType>
     <PlatformTarget>x86</PlatformTarget>
     <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisIgnoreBuiltInRules>false</CodeAnalysisIgnoreBuiltInRules>
   </PropertyGroup>
   <ItemGroup>
     <Reference Include="Microsoft.Solver.Foundation">
@@ -130,15 +110,12 @@
       <HintPath>..\Microsoft.Z3.dll</HintPath>
     </Reference>
     <Reference Include="System" />
-    <Reference Include="System.Core">
-      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    <Reference Include="System.Core">      
     </Reference>
     <Reference Include="System.Numerics" />
-    <Reference Include="System.Xml.Linq">
-      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    <Reference Include="System.Xml.Linq">      
     </Reference>
-    <Reference Include="System.Data.DataSetExtensions">
-      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    <Reference Include="System.Data.DataSetExtensions">      
     </Reference>
     <Reference Include="System.Data" />
     <Reference Include="System.Xml" />
@@ -156,24 +133,7 @@
     <Compile Include="Z3TermDirective.cs" />
     <Compile Include="Z3TermParams.cs" />
     <Compile Include="Z3TermSolver.cs" />
-  </ItemGroup>
-  <ItemGroup>
-    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
-      <Visible>False</Visible>
-      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
-      <Install>false</Install>
-    </BootstrapperPackage>
-    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
-      <Visible>False</Visible>
-      <ProductName>.NET Framework 3.5 SP1</ProductName>
-      <Install>true</Install>
-    </BootstrapperPackage>
-    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
-      <Visible>False</Visible>
-      <ProductName>Windows Installer 3.1</ProductName>
-      <Install>true</Install>
-    </BootstrapperPackage>
-  </ItemGroup>
+  </ItemGroup>  
   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 
        Other similar extension points exist, see Microsoft.Common.targets.
diff --git a/examples/msf/Validator/Validator.csproj b/examples/msf/Validator/Validator.csproj
index 97d00331d..cfea3c80b 100644
--- a/examples/msf/Validator/Validator.csproj
+++ b/examples/msf/Validator/Validator.csproj
@@ -11,12 +11,7 @@
     <RootNamespace>Validator</RootNamespace>
     <AssemblyName>Validator</AssemblyName>
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
-    <FileAlignment>512</FileAlignment>
-    <FileUpgradeFlags>
-    </FileUpgradeFlags>
-    <UpgradeBackupLocation>
-    </UpgradeBackupLocation>
-    <OldToolsVersion>3.5</OldToolsVersion>
+    <FileAlignment>512</FileAlignment>    
     <PublishUrl>publish\</PublishUrl>
     <Install>true</Install>
     <InstallFrom>Disk</InstallFrom>
@@ -94,14 +89,11 @@
       <HintPath>..\Microsoft.Solver.Foundation.dll</HintPath>
     </Reference>
     <Reference Include="System" />
-    <Reference Include="System.Core">
-      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    <Reference Include="System.Core">      
     </Reference>
-    <Reference Include="System.Xml.Linq">
-      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    <Reference Include="System.Xml.Linq">      
     </Reference>
-    <Reference Include="System.Data.DataSetExtensions">
-      <RequiredTargetFramework>3.5</RequiredTargetFramework>
+    <Reference Include="System.Data.DataSetExtensions">      
     </Reference>
     <Reference Include="System.Data" />
     <Reference Include="System.Xml" />
@@ -113,19 +105,7 @@
   <ItemGroup>
     <None Include="App.config" />
     <None Include="MicrosoftSolverFoundationForExcel.dll.config" />
-  </ItemGroup>
-  <ItemGroup>
-    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
-      <Visible>False</Visible>
-      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
-      <Install>false</Install>
-    </BootstrapperPackage>
-    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
-      <Visible>False</Visible>
-      <ProductName>.NET Framework 3.5 SP1</ProductName>
-      <Install>true</Install>
-    </BootstrapperPackage>
-  </ItemGroup>
+  </ItemGroup>  
   <ItemGroup>
     <ProjectReference Include="..\SolverFoundation.Plugin.Z3\SolverFoundation.Plugin.Z3.csproj">
       <Project>{7340e664-f648-4ff7-89b2-f4da424996d3}</Project>