mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' into jfleisher/devIntellitest

Browse source
This commit is contained in:
jofleish 2022-07-18 15:22:16 -04:00
commit 4e7c3bc7c4
130 changed files with 6682 additions and 4687 deletions
Download patch file Download diff file Expand all files Collapse all files

49
scripts/jsdoctest.yml Normal file
View file

@ -0,0 +1,49 @@
variables:
Major: '4'
Minor: '9'
Patch: '2'
NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
stages:
- stage: Build
jobs:
- job: UbuntuDoc
displayName: "Ubuntu Doc build"
pool:
vmImage: "Ubuntu-latest"
steps:
# TODO setup emscripten with no-install, then run
- script: npm --prefix=src/api/js ci
- script: npm --prefix=src/api/js run build:ts
- script: sudo apt-get install ocaml opam libgmp-dev
- script: opam init -y
- script: eval `opam config env`; opam install zarith ocamlfind -y
- script: eval `opam config env`; python scripts/mk_make.py --ml
- script: sudo apt-get install doxygen
- script: sudo apt-get install graphviz
- script: |
set -e
cd build
eval `opam config env`
make -j3
make -j3 examples
make -j3 test-z3
cd ..
- script: |
set -e
eval `opam config env`
cd doc
python mk_api_doc.py --mld --z3py-package-path=../build/python/z3 --js
mkdir api/html/ml
ocamldoc -html -d api/html/ml -sort -hide Z3 -I $( ocamlfind query zarith ) -I ../build/api/ml ../build/api/ml/z3enums.mli ../build/api/ml/z3.mli
cd ..
- script: zip -r z3doc.zip doc/api
- script: cp z3doc.zip $(Build.ArtifactStagingDirectory)/.
- task: PublishPipelineArtifact@0
inputs:
artifactName: 'UbuntuDoc'
targetPath: $(Build.ArtifactStagingDirectory)

2
scripts/mk_project.py
View file

@ -8,7 +8,7 @@
from mk_util import *
def init_version():
set_version(4, 8, 18, 0)
set_version(4, 9, 2, 0)
# Z3 Project definition
def init_project_def():

2
scripts/mk_util.py
View file

@ -1831,7 +1831,7 @@ class JavaDLLComponent(Component):
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
os.path.join('api', 'java', 'Native'))
else:
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) $(SLINK_EXTRA_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
os.path.join('api', 'java', 'Native'))
out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
deps = ''

4
scripts/nightly.yaml
View file

@ -1,8 +1,8 @@
variables:
Major: '4'
Minor: '8'
Patch: '18'
Minor: '9'
Patch: '2'
NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
stages:

65
scripts/release.yml
View file

@ -6,7 +6,7 @@
trigger: none
variables:
ReleaseVersion: '4.8.18'
ReleaseVersion: '4.9.2'
stages:
@ -44,25 +44,18 @@ stages:
targetPath: $(Build.ArtifactStagingDirectory)
- job: MacBuildArm64
displayName: "macOS Build"
displayName: "macOS ARM64 Build"
pool:
vmImage: "macOS-latest"
steps:
- task: PythonScript@0
displayName: Build
- script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0
- script: git clone https://github.com/z3prover/z3test z3test
- script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
- task: PublishPipelineArtifact@1
inputs:
scriptSource: 'filepath'
scriptPath: scripts/mk_unix_dist.py
arguments: --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --nojava --arch=arm64 --os=osx-11.0
- task: CopyFiles@2
inputs:
sourceFolder: dist
contents: '*.zip'
targetFolder: $(Build.ArtifactStagingDirectory)
- task: PublishPipelineArtifact@0
inputs:
artifactName: 'macOSBuildArm64'
artifactName: 'MacArm64'
targetPath: $(Build.ArtifactStagingDirectory)
- job: UbuntuBuild
@ -130,22 +123,14 @@ stages:
targetPath: $(Build.ArtifactStagingDirectory)
- job: LinuxBuilds
strategy:
matrix:
manyLinux:
name: ManyLinux
image: "quay.io/pypa/manylinux2010_x86_64:latest"
python: "/opt/python/cp37-cp37m/bin/python"
muslLinux:
name: MuslLinux
image: "quay.io/pypa/musllinux_1_1_x86_64:latest"
python: "/opt/python/cp310-cp310/bin/python"
displayName: "$(name) build"
displayName: "ManyLinux build"
variables:
name: ManyLinux
image: "quay.io/pypa/manylinux2010_x86_64:latest"
python: "/opt/python/cp37-cp37m/bin/python"
pool:
vmImage: "ubuntu-latest"
container: $(image)
variables:
python: $(python)
container: "quay.io/pypa/manylinux2010_x86_64:latest"
steps:
- task: PythonScript@0
displayName: Build
@ -170,7 +155,7 @@ stages:
targetFolder: $(Build.ArtifactStagingDirectory)
- task: PublishPipelineArtifact@0
inputs:
artifactName: '$(name)Build'
artifactName: 'ManyLinuxBuild'
targetPath: $(Build.ArtifactStagingDirectory)
- template: build-win-signed.yml
@ -405,16 +390,16 @@ stages:
inputs:
artifact: 'macOSBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download macOS Arm64 Build'
inputs:
artifact: 'MacArm64'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download ManyLinux Build'
inputs:
artifact: 'ManyLinuxBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download MuslLinux Build'
inputs:
artifact: 'MuslLinuxBuild'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download Win32 Build'
inputs:
@ -425,19 +410,17 @@ stages:
inputs:
artifact: 'WindowsBuild-x64'
path: $(Agent.TempDirectory)
- script: cd $(Agent.TempDirectory); mkdir osx-bin; cd osx-bin; unzip ../*osx*.zip
- script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*x64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip
- script: cd $(Agent.TempDirectory); mkdir libc-bin; cd libc-bin; unzip ../*glibc*.zip
- script: cd $(Agent.TempDirectory); mkdir musl-bin; cd musl-bin; unzip ../*-linux.zip
- script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip
- script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip
- script: python3 -m pip install --user -U setuptools wheel
- script: cd src/api/python; python3 setup.py sdist
# take a look at this PREMIUM HACK I came up with to get around the fact that the azure variable syntax overloads the bash syntax for subshells
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/osx-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/libc-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/musl-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
- task: PublishPipelineArtifact@0
@ -473,7 +456,7 @@ stages:
- task: DownloadPipelineArtifact@2
displayName: 'Download macOSArm64 Build'
inputs:
artifact: 'macOSBuildArm64'
artifact: 'MacArm64'
path: $(Agent.TempDirectory)
- task: DownloadPipelineArtifact@2
displayName: 'Download Win32 Build'
@ -513,7 +496,7 @@ stages:
releaseNotes: '$(ReleaseVersion) release'
assets: '$(Agent.TempDirectory)/*.*'
isDraft: true
isPreRelease: false
isPreRelease: true
# Enable on release (after fixing Nuget key)
- job: NuGetPublish

13
scripts/update_api.py
View file

@ -91,7 +91,7 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint',
# Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int64', UINT64 : 'int64', DOUBLE : 'float',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'int' }
@ -254,8 +254,10 @@ def param2pystr(p):
def param2ml(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL or param_type(p) == INT64 or param_type(p) == UINT64:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return "int"
elif param_type(p) == INT64 or param_type(p) == UINT64:
return "int64"
elif param_type(p) == STRING:
return "string"
else:
@ -689,6 +691,7 @@ def mk_java(java_src, java_dir, package_name):
java_native.write('}\n')
java_wrapper = open(java_wrapperf, 'w')
pkg_str = package_name.replace('.', '_')
java_wrapper.write("// Automatically generated file\n")
with open(java_src + "/NativeStatic.txt") as ins:
for line in ins:
java_wrapper.write(line)
@ -1251,9 +1254,9 @@ def ml_unwrap(t, ts, s):
elif t == UINT:
return '(' + ts + ') Unsigned_int_val(' + s + ')'
elif t == INT64:
return '(' + ts + ') Long_val(' + s + ')'
return '(' + ts + ') Int64_val(' + s + ')'
elif t == UINT64:
return '(' + ts + ') Unsigned_long_val(' + s + ')'
return '(' + ts + ') Int64_val(' + s + ')'
elif t == DOUBLE:
return '(' + ts + ') Double_val(' + s + ')'
elif ml_has_plus_type(ts):
@ -1270,7 +1273,7 @@ def ml_set_wrap(t, d, n):
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL:
return d + ' = Val_int(' + n + ');'
elif t == INT64 or t == UINT64:
return d + ' = Val_long(' + n + ');'
return d + ' = caml_copy_int64(' + n + ');'
elif t == DOUBLE:
return d + '= caml_copy_double(' + n + ');'
elif t == STRING: