From 07b9eeecd2695a2d09d458ad8ab9bf6a1caec603 Mon Sep 17 00:00:00 2001 From: Eric Kilmer Date: Tue, 26 Apr 2022 22:24:59 -0400 Subject: [PATCH] [z3] Update to 4.8.16 (#24407) * [z3] Update to 4.8.16 * Use Python3 instead of Python2 Python2 is EOL and the build script works with Python3, so we should prefer Python3 * Update version --- ports/z3/fix-32-bit-build.patch | 132 --------------------------- ports/z3/portfile.cmake | 11 +-- ports/z3/remove-flag-overrides.patch | 2 +- ports/z3/vcpkg.json | 2 +- versions/baseline.json | 2 +- versions/z-/z3.json | 5 + 6 files changed, 13 insertions(+), 141 deletions(-) delete mode 100644 ports/z3/fix-32-bit-build.patch diff --git a/ports/z3/fix-32-bit-build.patch b/ports/z3/fix-32-bit-build.patch deleted file mode 100644 index 56b9f4c776..0000000000 --- a/ports/z3/fix-32-bit-build.patch +++ /dev/null @@ -1,132 +0,0 @@ -From 3828130791bf8e60038b46b0d6602cb7e43fb344 Mon Sep 17 00:00:00 2001 -From: Nikolaj Bjorner -Date: Thu, 24 Mar 2022 14:05:05 -1000 -Subject: [PATCH] fix #5922 use 0u to help type inference - -Signed-off-by: Nikolaj Bjorner ---- - src/api/c++/z3++.h | 30 +++++++++++++++--------------- - 1 file changed, 15 insertions(+), 15 deletions(-) - -diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h -index b00a33ad71..4d60de4338 100644 ---- a/src/api/c++/z3++.h -+++ b/src/api/c++/z3++.h -@@ -2333,7 +2333,7 @@ namespace z3 { - - inline expr pble(expr_vector const& es, int const* coeffs, int bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0u].ctx(); - array _es(es); - Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound); - ctx.check_error(); -@@ -2341,7 +2341,7 @@ namespace z3 { - } - inline expr pbge(expr_vector const& es, int const* coeffs, int bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0u].ctx(); - array _es(es); - Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound); - ctx.check_error(); -@@ -2349,7 +2349,7 @@ namespace z3 { - } - inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0u].ctx(); - array _es(es); - Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound); - ctx.check_error(); -@@ -2357,7 +2357,7 @@ namespace z3 { - } - inline expr atmost(expr_vector const& es, unsigned bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0u].ctx(); - array _es(es); - Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound); - ctx.check_error(); -@@ -2365,7 +2365,7 @@ namespace z3 { - } - inline expr atleast(expr_vector const& es, unsigned bound) { - assert(es.size() > 0); -- context& ctx = es[0].ctx(); -+ context& ctx = es[0u].ctx(); - array _es(es); - Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound); - ctx.check_error(); -@@ -2373,7 +2373,7 @@ namespace z3 { - } - inline expr sum(expr_vector const& args) { - assert(args.size() > 0); -- context& ctx = args[0].ctx(); -+ context& ctx = args[0u].ctx(); - array _args(args); - Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr()); - ctx.check_error(); -@@ -2382,7 +2382,7 @@ namespace z3 { - - inline expr distinct(expr_vector const& args) { - assert(args.size() > 0); -- context& ctx = args[0].ctx(); -+ context& ctx = args[0u].ctx(); - array _args(args); - Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr()); - ctx.check_error(); -@@ -2411,14 +2411,14 @@ namespace z3 { - Z3_ast r; - assert(args.size() > 0); - if (args.size() == 1) { -- return args[0]; -+ return args[0u]; - } -- context& ctx = args[0].ctx(); -+ context& ctx = args[0u].ctx(); - array _args(args); -- if (Z3_is_seq_sort(ctx, args[0].get_sort())) { -+ if (Z3_is_seq_sort(ctx, args[0u].get_sort())) { - r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr()); - } -- else if (Z3_is_re_sort(ctx, args[0].get_sort())) { -+ else if (Z3_is_re_sort(ctx, args[0u].get_sort())) { - r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr()); - } - else { -@@ -2448,7 +2448,7 @@ namespace z3 { - inline expr mk_xor(expr_vector const& args) { - if (args.empty()) - return args.ctx().bool_val(false); -- expr r = args[0]; -+ expr r = args[0u]; - for (unsigned i = 1; i < args.size(); ++i) - r = r ^ args[i]; - return r; -@@ -2771,7 +2771,7 @@ namespace z3 { - assert(!m_end && !m_empty); - m_cube = m_solver.cube(m_vars, m_cutoff); - m_cutoff = 0xFFFFFFFF; -- if (m_cube.size() == 1 && m_cube[0].is_false()) { -+ if (m_cube.size() == 1 && m_cube[0u].is_false()) { - m_cube = z3::expr_vector(m_solver.ctx()); - m_end = true; - } -@@ -3005,7 +3005,7 @@ namespace z3 { - } - array buffer(n); - for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i]; -- return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr())); -+ return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr())); - } - - inline tactic par_and_then(tactic const & t1, tactic const & t2) { -@@ -3804,7 +3804,7 @@ namespace z3 { - } - inline expr re_intersect(expr_vector const& args) { - assert(args.size() > 0); -- context& ctx = args[0].ctx(); -+ context& ctx = args[0u].ctx(); - array _args(args); - Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr()); - ctx.check_error(); diff --git a/ports/z3/portfile.cmake b/ports/z3/portfile.cmake index 7156b7186c..0e8dc4b0ba 100644 --- a/ports/z3/portfile.cmake +++ b/ports/z3/portfile.cmake @@ -1,17 +1,16 @@ -vcpkg_find_acquire_program(PYTHON2) -get_filename_component(PYTHON2_DIR "${PYTHON2}" DIRECTORY) -vcpkg_add_to_path("${PYTHON2_DIR}") +vcpkg_find_acquire_program(PYTHON3) +get_filename_component(PYTHON3_DIR "${PYTHON3}" DIRECTORY) +vcpkg_add_to_path("${PYTHON3_DIR}") vcpkg_from_github( OUT_SOURCE_PATH SOURCE_PATH REPO Z3Prover/z3 - REF z3-4.8.15 - SHA512 7b08dec5b035a38edc90c4c491f508fd9ed227357de94400169db53d4c59382bd6a81ae6615771023a06534a3aa92668844f0ebfcc2a3b5ef4bba957426a0c6c + REF z3-4.8.16 + SHA512 385f6e1ee075b9eadb5aad338657a81f518eef382b99ce623448a630b79f5d414ebccfd1bb5e959626f0b82ef54a5f20326814ae988b5688d51578de6fb69615 HEAD_REF master PATCHES fix-install-path.patch remove-flag-overrides.patch - fix-32-bit-build.patch ) if (VCPKG_LIBRARY_LINKAGE STREQUAL "static") diff --git a/ports/z3/remove-flag-overrides.patch b/ports/z3/remove-flag-overrides.patch index df6a4a16ef..ddba89dd60 100644 --- a/ports/z3/remove-flag-overrides.patch +++ b/ports/z3/remove-flag-overrides.patch @@ -7,6 +7,6 @@ index 477410ba8..fcca03917 100644 cmake_minimum_required(VERSION 3.4) -set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") - project(Z3 VERSION 4.8.15.0 LANGUAGES CXX) + project(Z3 VERSION 4.8.16.0 LANGUAGES CXX) ################################################################################ diff --git a/ports/z3/vcpkg.json b/ports/z3/vcpkg.json index 50ec3e9ea7..f5f59bfbd1 100644 --- a/ports/z3/vcpkg.json +++ b/ports/z3/vcpkg.json @@ -1,6 +1,6 @@ { "name": "z3", - "version": "4.8.15", + "version": "4.8.16", "description": "Z3 is a theorem prover from Microsoft Research", "homepage": "https://github.com/Z3Prover/z3", "license": "MIT", diff --git a/versions/baseline.json b/versions/baseline.json index 9bd8490478..d1817f82b5 100644 --- a/versions/baseline.json +++ b/versions/baseline.json @@ -7665,7 +7665,7 @@ "port-version": 0 }, "z3": { - "baseline": "4.8.15", + "baseline": "4.8.16", "port-version": 0 }, "z85": { diff --git a/versions/z-/z3.json b/versions/z-/z3.json index 26bf54ad69..ae108bc454 100644 --- a/versions/z-/z3.json +++ b/versions/z-/z3.json @@ -1,5 +1,10 @@ { "versions": [ + { + "git-tree": "a1217f07ef4a8f918f5b61a01057a4ee70f92422", + "version": "4.8.16", + "port-version": 0 + }, { "git-tree": "ca14e43533889ce4abf89af387b73d015e133c4a", "version": "4.8.15",