mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-11-14 11:31:49 -08:00
commit 1f95f97459
3 changed files with 30 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

8
package/Microsoft.Z3.x64.nuspec
View file

@ -5,10 +5,9 @@
<version>$(releaseVersion)</version> <version>$(releaseVersion)</version>
<copyright>© Microsoft Corporation. All rights reserved.</copyright> <copyright>© Microsoft Corporation. All rights reserved.</copyright>
<authors>Microsoft</authors> <authors>Microsoft</authors>
<owners>Microsoft,Z3Prover</owners> <iconUrl>https://raw.githubusercontent.com/Z3Prover/z3/$(releaseCommitHash)/package/icon.jpg</iconUrl>
<iconUrl>$(iconUrlFromReleaseCommit)</iconUrl>
<projectUrl>https://github.com/Z3Prover/z3</projectUrl> <projectUrl>https://github.com/Z3Prover/z3</projectUrl>
<licenseUrl>$(licenseUrlFromReleaseCommit)</licenseUrl> <licenseUrl>https://raw.githubusercontent.com/Z3Prover/z3/$(releaseCommitHash)/LICENSE.txt</licenseUrl>
<repository <repository
type="git" type="git"
url="https://github.com/Z3Prover/z3.git" url="https://github.com/Z3Prover/z3.git"
@ -16,7 +15,8 @@
commit="$(releaseCommitHash)" commit="$(releaseCommitHash)"
/> />
<requireLicenseAcceptance>true</requireLicenseAcceptance> <requireLicenseAcceptance>true</requireLicenseAcceptance>
<description>Z3 is a constraint/SMT solver and theorem prover from Microsoft Research.</description> <description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</description>
<tags>smt constraint solver theorem prover</tags> <tags>smt constraint solver theorem prover</tags>
<language>en</language>
</metadata> </metadata>
</package> </package>

6
package/PackageCreationDirections.md
View file

@ -15,11 +15,9 @@
| +-- Microsoft.Z3.x64.targets | +-- Microsoft.Z3.x64.targets
| +-- libz3.dll | +-- libz3.dll
``` ```
4. Open the nuspec file and fill in the appropriate macro values (note that for all URLs, preserve link integrity by linking to a specific commit): 4. Open the nuspec file and fill in the appropriate macro values:
* $(releaseVersion) - the Z3 version being released in this package * $(releaseVersion) - the Z3 version being released in this package
* $(iconUrlFromReleaseCommit) - URL for the Z3 icon file * $(releaseCommitHash) - hash of the release commit (there are several of these)
* $(licenseUrlFromReleaseCommit) - URL for the Z3 repo license
* $(releaseCommitHash) - hash of the release commit
5. Run `nuget pack Microsoft.Z3.x64\Microsoft.Z3.x64.nuspec` 5. Run `nuget pack Microsoft.Z3.x64\Microsoft.Z3.x64.nuspec`
6. Test the resulting nupkg file (described below) then submit the package for signing before uploading to NuGet.org 6. Test the resulting nupkg file (described below) then submit the package for signing before uploading to NuGet.org

14
scripts/mk_util.py
View file

@ -61,6 +61,7 @@ PATTERN_COMPONENT='pattern'
UTIL_COMPONENT='util' UTIL_COMPONENT='util'
API_COMPONENT='api' API_COMPONENT='api'
DOTNET_COMPONENT='dotnet' DOTNET_COMPONENT='dotnet'
DOTNET_CORE_COMPONENT='dotnetcore'
JAVA_COMPONENT='java' JAVA_COMPONENT='java'
ML_COMPONENT='ml' ML_COMPONENT='ml'
CPP_COMPONENT='cpp' CPP_COMPONENT='cpp'
@ -454,6 +455,10 @@ def check_dotnet():
if r != 0: if r != 0:
raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.')
def check_dotnet_core():
# TBD: check DOTNET
pass
def check_ml(): def check_ml():
t = TempFile('hello.ml') t = TempFile('hello.ml')
t.add('print_string "Hello world!\n";;') t.add('print_string "Hello world!\n";;')
@ -2357,7 +2362,7 @@ class DotNetExampleComponent(ExampleComponent):
ExampleComponent.__init__(self, name, path) ExampleComponent.__init__(self, name, path)
def is_example(self): def is_example(self):
return is_dotnet_enabled() return is_dotnet_enabled() or is_dotnet_core_enabled()
def mk_makefile(self, out): def mk_makefile(self, out):
if is_dotnet_enabled(): if is_dotnet_enabled():
@ -2385,6 +2390,8 @@ class DotNetExampleComponent(ExampleComponent):
out.write(os.path.join(relative_path, csfile)) out.write(os.path.join(relative_path, csfile))
out.write('\n') out.write('\n')
out.write('_ex_%s: %s\n\n' % (self.name, exefile)) out.write('_ex_%s: %s\n\n' % (self.name, exefile))
if is_dotnet_core_enabled():
print("TBD: build script for dotnet_example on core")
class JavaExampleComponent(ExampleComponent): class JavaExampleComponent(ExampleComponent):
def __init__(self, name, path): def __init__(self, name, path):
@ -3172,6 +3179,9 @@ def mk_bindings(api_files):
if is_dotnet_enabled(): if is_dotnet_enabled():
check_dotnet() check_dotnet()
mk_z3consts_dotnet(api_files) mk_z3consts_dotnet(api_files)
if is_dotnet_core_enabled():
check_dotnet_core()
mk_z3consts_dotnet(api_files)
# Extract enumeration types from API files, and add python definitions. # Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files): def mk_z3consts_py(api_files):
@ -3190,6 +3200,8 @@ def mk_z3consts_py(api_files):
# Extract enumeration types from z3_api.h, and add .Net definitions # Extract enumeration types from z3_api.h, and add .Net definitions
def mk_z3consts_dotnet(api_files): def mk_z3consts_dotnet(api_files):
dotnet = get_component(DOTNET_COMPONENT) dotnet = get_component(DOTNET_COMPONENT)
if not dotnet:
dotnet = get_component(DOTNET_CORE_COMPONENT)
full_path_api_files = [] full_path_api_files = []
for api_file in api_files: for api_file in api_files:
api_file_c = dotnet.find_file(api_file, dotnet.name) api_file_c = dotnet.find_file(api_file, dotnet.name)