mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

Add binding redirects

Browse source
This commit is contained in:
Anh-Dung Phan 2013-12-27 14:38:57 -08:00
parent 8accc49386
commit e223e386fe
3 changed files with 16 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
examples/msf/README
View file

@ -2,7 +2,7 @@ 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'
3. Build 'Z3MSFPlugin.sln'. Note that you have to compile using x86 target for Microsoft.Z3.dll 32-bit and x64 target for Microsoft.Z3.dll 64-bit.
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.

16
examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj
View file

@ -14,7 +14,7 @@
<FileAlignment>512</FileAlignment>
<SignAssembly>false</SignAssembly>
<AssemblyOriginatorKeyFile>
</AssemblyOriginatorKeyFile>
</AssemblyOriginatorKeyFile>
<PublishUrl>publish\</PublishUrl>
<Install>true</Install>
<InstallFrom>Disk</InstallFrom>
@ -106,16 +106,17 @@
<Reference Include="Microsoft.Solver.Foundation">
<HintPath>..\Microsoft.Solver.Foundation.dll</HintPath>
</Reference>
<Reference Include="Microsoft.Z3">
<Reference Include="Microsoft.Z3, Version=4.3.2.0, Culture=neutral, processorArchitecture=x86">
<SpecificVersion>False</SpecificVersion>
<HintPath>..\Microsoft.Z3.dll</HintPath>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core">
<Reference Include="System.Core">
</Reference>
<Reference Include="System.Numerics" />
<Reference Include="System.Xml.Linq">
<Reference Include="System.Xml.Linq">
</Reference>
<Reference Include="System.Data.DataSetExtensions">
<Reference Include="System.Data.DataSetExtensions">
</Reference>
<Reference Include="System.Data" />
<Reference Include="System.Xml" />
@ -133,7 +134,10 @@
<Compile Include="Z3TermDirective.cs" />
<Compile Include="Z3TermParams.cs" />
<Compile Include="Z3TermSolver.cs" />
</ItemGroup>
</ItemGroup>
<ItemGroup>
<None Include="App.config" />
</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.

5
examples/msf/Z3MSFPlugin.sln
View file

@ -7,6 +7,11 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SolverFoundation.Plugin.Z3.
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Validator", "Validator\Validator.csproj", "{54835857-129F-44C9-B529-A42158647B36}"
EndProject
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Solution Items", "Solution Items", "{F1E99540-BA5E-46DF-9E29-6146A309CD18}"
ProjectSection(SolutionItems) = preProject
README = README
EndProjectSection
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
commercial_64|Any CPU = commercial_64|Any CPU