From 3ebec56880ec7e1b55993ea80ef44a71d2dbf3d8 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Thu, 14 Dec 2023 00:36:41 +0700 Subject: [PATCH 1/8] tptr.h: Include `` once rather than twice. (#7051) --- src/util/tptr.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/tptr.h b/src/util/tptr.h index 50e9417feea..37b6f64fe72 100644 --- a/src/util/tptr.h +++ b/src/util/tptr.h @@ -21,7 +21,6 @@ Revision History: #include #include "util/machine.h" -#include #define TAG_SHIFT PTR_ALIGNMENT #define ALIGNMENT_VALUE (1 << PTR_ALIGNMENT) From 8293be859f0b8eb4c2b818f245c912864e79bde0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Dec 2023 02:05:33 +0000 Subject: [PATCH 2/8] Disable Python compilation cache during build (#7052) * Disable Python compilation cache during build * Fix var name --- scripts/mk_util.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0728c2cb727..90271321bb4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2994,9 +2994,16 @@ def cp_z3py_to_build(): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) + # We do not want a second copy of the compiled files in the system-wide cache, + # so we disable it temporarily. This is an issue with recent versions of MacOS + # where XCode's Python has a cache, but the build scripts don't have access to + # it (e.g. during OPAM package installation). + pycache_prefix_before = sys.pycache_prefix + sys.pycache_prefix = None # Compile Z3Py files if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") + sys.pycache_prefix = pycache_prefix_before if is_verbose: print("Generated python bytecode") # Copy sources to build From 995b40865b868511f8e627b7728c07b9d35520c9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 18:44:11 -0800 Subject: [PATCH 3/8] remove readme reference, add arm64 build to nightly Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 7 +----- scripts/nightly.yaml | 46 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 47 insertions(+), 6 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index d3f4027738b..58251c6f8d7 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -88,7 +88,7 @@ def mk_targets(source_root): def mk_icon(source_root): mk_dir("out/content") shutil.copy(f"{source_root}/resources/icon.jpg", "out/content/icon.jpg") - shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") +# shutil.copy(f"{source_root}/src/api/dotnet/README.md", "out/content/README.md") @@ -109,7 +109,6 @@ def create_nuget_spec(version, repo, branch, commit, symbols, arch): © Microsoft Corporation. All rights reserved. smt constraint solver theorem prover content/icon.jpg - content/README.md https://github.com/Z3Prover/z3 MIT @@ -119,10 +118,6 @@ def create_nuget_spec(version, repo, branch, commit, symbols, arch): - - - - """.format(version, repo, branch, commit, arch) print(contents) sym = "sym." if symbols else "" diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 2b1b4ca3d3c..ad7f19a9c96 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -233,6 +233,47 @@ stages: symbolServerType: TeamServices detailedLog: true +- job: "WindowsArm64" + displayName: "Windows" + pool: + vmImage: "windows-latest" + variables: + arch: "amd64_arm64" + steps: + - script: md build + - script: | + cd build + call "C:\Program Files\Microsoft Visual Studio\2022\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch) + cmake $(bindings) -G "NMake Makefiles" ../ + nmake + cd .. + - task: CopyFiles@2 + inputs: + sourceFolder: build + contents: '*.zip' + targetFolder: $(Build.ArtifactStagingDirectory) + - task: PublishPipelineArtifact@1 + inputs: + targetPath: $(Build.ArtifactStagingDirectory) + artifactName: 'WindowsArm64' + - task: CopyFiles@2 + displayName: 'Collect Symbols' + inputs: + sourceFolder: build + contents: '**/*.pdb' + targetFolder: '$(Build.ArtifactStagingDirectory)/symbols' + # Publish symbol archive to match nuget package + # Index your source code and publish symbols to a file share or Azure Artifacts symbol server + - task: PublishSymbols@2 + inputs: + symbolsFolder: '$(Build.ArtifactStagingDirectory)/symbols' + searchPattern: '**/*.pdb' + indexSources: false # Github not supported + publishSymbols: true + symbolServerType: TeamServices + detailedLog: true + + - stage: Package jobs: - job: NuGet64 @@ -534,6 +575,11 @@ stages: inputs: artifactName: 'Windows32' targetPath: tmp + - task: DownloadPipelineArtifact@2 + displayName: "Download windowsArm64" + inputs: + artifactName: 'WindowsArm64' + targetPath: tmp - task: DownloadPipelineArtifact@2 displayName: "Download windows64" inputs: From c20b8cb9788bc445600c637e763c9c37e0fb6c57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 18:46:20 -0800 Subject: [PATCH 4/8] nightly Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index ad7f19a9c96..4de95339c93 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -233,13 +233,13 @@ stages: symbolServerType: TeamServices detailedLog: true -- job: "WindowsArm64" - displayName: "Windows" - pool: - vmImage: "windows-latest" - variables: - arch: "amd64_arm64" - steps: + - job: "WindowsArm64" + displayName: "Windows" + pool: + vmImage: "windows-latest" + variables: + arch: "amd64_arm64" + steps: - script: md build - script: | cd build From b40e3015efe5092e072a85cc41770e3a946e06ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 19:25:18 -0800 Subject: [PATCH 5/8] fix #7053 --- src/opt/opt_solver.cpp | 4 ++-- src/smt/theory_arith_pp.h | 6 ++++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index ee91b06a491..955025fd96c 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -52,7 +52,7 @@ namespace opt { if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { m_params.m_relevancy_lvl = 0; } - m_params.m_arith_auto_config_simplex = false; + m_params.m_arith_auto_config_simplex = true; m_params.m_threads = 1; // need to interact with the solver that created model so can't have threads // m_params.m_auto_config = false; } @@ -67,7 +67,7 @@ namespace opt { m_dump_benchmarks = p.dump_benchmarks(); m_params.updt_params(_p); m_context.updt_params(_p); - m_params.m_arith_auto_config_simplex = false; + m_params.m_arith_auto_config_simplex = true; } solver* opt_solver::translate(ast_manager& m, params_ref const& p) { diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index b0d43bc00ac..edc640d86aa 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -83,9 +83,11 @@ namespace smt { template void theory_arith::display_row(std::ostream & out, row const & r, bool compact) const { - + if (static_cast(r.get_base_var()) >= m_columns.size()) + return; column const & c = m_columns[r.get_base_var()]; - out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : "; + if (c.size() > 0) + out << "(v" << r.get_base_var() << " r" << c[0].m_row_id << ") : "; bool first = true; for (auto const& e : r) { if (!e.is_dead()) { From f7d9a5ba935163ddefd3e1883878556d713d6fee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 19:32:00 -0800 Subject: [PATCH 6/8] Revert "Disable Python compilation cache during build (#7052)" (#7054) This reverts commit 8293be859f0b8eb4c2b818f245c912864e79bde0. --- scripts/mk_util.py | 7 ------- 1 file changed, 7 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 90271321bb4..0728c2cb727 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2994,16 +2994,9 @@ def cp_z3py_to_build(): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) - # We do not want a second copy of the compiled files in the system-wide cache, - # so we disable it temporarily. This is an issue with recent versions of MacOS - # where XCode's Python has a cache, but the build scripts don't have access to - # it (e.g. during OPAM package installation). - pycache_prefix_before = sys.pycache_prefix - sys.pycache_prefix = None # Compile Z3Py files if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") - sys.pycache_prefix = pycache_prefix_before if is_verbose: print("Generated python bytecode") # Copy sources to build From 7c2e4f2f9c546ee0b8ed241c7ea85a903b2b7c38 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Dec 2023 20:43:17 -0800 Subject: [PATCH 7/8] fiddle with what gets added to win-arm64 Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 4de95339c93..0f533765409 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -234,11 +234,12 @@ stages: detailedLog: true - job: "WindowsArm64" - displayName: "Windows" + displayName: "WindowsArm64" pool: vmImage: "windows-latest" variables: arch: "amd64_arm64" + bindings: "-DCMAKE_BUILD_TYPE=RelWithDebInfo" steps: - script: md build - script: | @@ -250,7 +251,7 @@ stages: - task: CopyFiles@2 inputs: sourceFolder: build - contents: '*.zip' + contents: '*z3*.*' targetFolder: $(Build.ArtifactStagingDirectory) - task: PublishPipelineArtifact@1 inputs: From a2b490baa6f092be60d9797e7ddbeabe37b2671f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Dec 2023 15:26:52 +0000 Subject: [PATCH 8/8] Disable Python compilation cache during build (#7057) * Disable Python compilation cache during build * More pythonic check for none --- scripts/mk_util.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0728c2cb727..014b0e40f83 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2994,9 +2994,19 @@ def cp_z3py_to_build(): for f in files: if f.endswith('.pyc'): rmf(os.path.join(root, f)) + # We do not want a second copy of the compiled files in the system-wide cache, + # so we disable it temporarily. This is an issue with recent versions of MacOS + # where XCode's Python has a cache, but the build scripts don't have access to + # it (e.g. during OPAM package installation). + have_cache = hasattr(sys, 'pycache_prefix') and sys.pycache_prefix is not None + if have_cache: + pycache_prefix_before = sys.pycache_prefix + sys.pycache_prefix = None # Compile Z3Py files if compileall.compile_dir(z3py_src, force=1) != 1: raise MKException("failed to compile Z3Py sources") + if have_cache: + sys.pycache_prefix = pycache_prefix_before if is_verbose: print("Generated python bytecode") # Copy sources to build