diff --git a/build-steps.log b/build-steps.log new file mode 100644 index 000000000..80b413183 --- /dev/null +++ b/build-steps.log @@ -0,0 +1,478 @@ +Installing dependencies... +Get:1 file:/etc/apt/apt-mirrors.txt Mirrorlist [144 B] +Hit:2 http://azure.archive.ubuntu.com/ubuntu noble InRelease +Hit:6 https://packages.microsoft.com/repos/azure-cli noble InRelease +Get:7 https://packages.microsoft.com/ubuntu/24.04/prod noble InRelease [3600 B] +Get:3 http://azure.archive.ubuntu.com/ubuntu noble-updates InRelease [126 kB] +Get:4 http://azure.archive.ubuntu.com/ubuntu noble-backports InRelease [126 kB] +Get:5 http://azure.archive.ubuntu.com/ubuntu noble-security InRelease [126 kB] +Get:8 https://packages.microsoft.com/ubuntu/24.04/prod noble/main arm64 Packages [35.7 kB] +Get:9 https://packages.microsoft.com/ubuntu/24.04/prod noble/main amd64 Packages [53.2 kB] +Get:10 http://azure.archive.ubuntu.com/ubuntu noble-updates/main amd64 Packages [1411 kB] +Get:11 http://azure.archive.ubuntu.com/ubuntu noble-updates/main Translation-en [278 kB] +Get:12 http://azure.archive.ubuntu.com/ubuntu noble-updates/main amd64 Components [175 kB] +Get:13 http://azure.archive.ubuntu.com/ubuntu noble-updates/main amd64 c-n-f Metadata [15.2 kB] +Get:14 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe amd64 Packages [1483 kB] +Get:15 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe Translation-en [298 kB] +Get:16 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe amd64 Components [377 kB] +Get:17 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe amd64 c-n-f Metadata [31.0 kB] +Get:18 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted amd64 Packages [1882 kB] +Get:19 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted Translation-en [422 kB] +Get:20 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted amd64 Components [212 B] +Get:21 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted amd64 c-n-f Metadata [500 B] +Get:22 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse amd64 Packages [41.9 kB] +Get:23 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse Translation-en [7064 B] +Get:24 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse amd64 Components [940 B] +Get:25 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse amd64 c-n-f Metadata [644 B] +Get:26 http://azure.archive.ubuntu.com/ubuntu noble-backports/main amd64 Components [7068 B] +Get:27 http://azure.archive.ubuntu.com/ubuntu noble-backports/universe amd64 Components [19.2 kB] +Get:28 http://azure.archive.ubuntu.com/ubuntu noble-backports/restricted amd64 Components [216 B] +Get:29 http://azure.archive.ubuntu.com/ubuntu noble-backports/multiverse amd64 Components [212 B] +Get:30 http://azure.archive.ubuntu.com/ubuntu noble-security/main amd64 Packages [1119 kB] +Get:31 http://azure.archive.ubuntu.com/ubuntu noble-security/main Translation-en [192 kB] +Get:32 http://azure.archive.ubuntu.com/ubuntu noble-security/main amd64 Components [21.6 kB] +Get:33 http://azure.archive.ubuntu.com/ubuntu noble-security/main amd64 c-n-f Metadata [8748 B] +Get:34 http://azure.archive.ubuntu.com/ubuntu noble-security/universe amd64 Packages [880 kB] +Get:35 http://azure.archive.ubuntu.com/ubuntu noble-security/universe Translation-en [195 kB] +Get:36 http://azure.archive.ubuntu.com/ubuntu noble-security/universe amd64 Components [52.2 kB] +Get:37 http://azure.archive.ubuntu.com/ubuntu noble-security/universe amd64 c-n-f Metadata [18.0 kB] +Get:38 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted amd64 Packages [1756 kB] +Get:39 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted Translation-en [392 kB] +Get:40 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted amd64 Components [212 B] +Get:41 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted amd64 c-n-f Metadata [468 B] +Get:42 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse amd64 Packages [37.4 kB] +Get:43 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse Translation-en [6020 B] +Get:44 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse amd64 Components [212 B] +Get:45 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse amd64 c-n-f Metadata [476 B] +Fetched 11.6 MB in 1s (7848 kB/s) +Reading package lists... +Reading package lists... +Building dependency tree... +Reading state information... +python3 is already the newest version (3.12.3-0ubuntu2). +python3-pip is already the newest version (24.0+dfsg-1ubuntu1.2). +git is already the newest version (1:2.51.0-0ppa2~ubuntu24.04.1). +git set to manually installed. +Suggested packages: + cmake-doc cmake-format elpa-cmake-mode +The following NEW packages will be installed: + build-essential cmake cmake-data libjsoncpp25 librhash0 ninja-build +0 upgraded, 6 newly installed, 0 to remove and 34 not upgraded. +Need to get 13.7 MB of archives. +After this operation, 49.5 MB of additional disk space will be used. +Get:1 file:/etc/apt/apt-mirrors.txt Mirrorlist [144 B] +Get:2 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 build-essential amd64 12.10ubuntu1 [4928 B] +Get:3 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 libjsoncpp25 amd64 1.9.5-6build1 [82.8 kB] +Get:4 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 librhash0 amd64 1.4.3-3build1 [129 kB] +Get:5 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 cmake-data all 3.28.3-1build7 [2155 kB] +Get:6 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 cmake amd64 3.28.3-1build7 [11.2 MB] +Get:7 http://azure.archive.ubuntu.com/ubuntu noble/universe amd64 ninja-build amd64 1.11.1-2 [129 kB] +Fetched 13.7 MB in 1s (15.6 MB/s) +Selecting previously unselected package build-essential. +(Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 218657 files and directories currently installed.) +Preparing to unpack .../0-build-essential_12.10ubuntu1_amd64.deb ... +Unpacking build-essential (12.10ubuntu1) ... +Selecting previously unselected package libjsoncpp25:amd64. +Preparing to unpack .../1-libjsoncpp25_1.9.5-6build1_amd64.deb ... +Unpacking libjsoncpp25:amd64 (1.9.5-6build1) ... +Selecting previously unselected package librhash0:amd64. +Preparing to unpack .../2-librhash0_1.4.3-3build1_amd64.deb ... +Unpacking librhash0:amd64 (1.4.3-3build1) ... +Selecting previously unselected package cmake-data. +Preparing to unpack .../3-cmake-data_3.28.3-1build7_all.deb ... +Unpacking cmake-data (3.28.3-1build7) ... +Selecting previously unselected package cmake. +Preparing to unpack .../4-cmake_3.28.3-1build7_amd64.deb ... +Unpacking cmake (3.28.3-1build7) ... +Selecting previously unselected package ninja-build. +Preparing to unpack .../5-ninja-build_1.11.1-2_amd64.deb ... +Unpacking ninja-build (1.11.1-2) ... +Setting up ninja-build (1.11.1-2) ... +Setting up libjsoncpp25:amd64 (1.9.5-6build1) ... +Setting up librhash0:amd64 (1.4.3-3build1) ... +Setting up build-essential (12.10ubuntu1) ... +Setting up cmake-data (3.28.3-1build7) ... +Setting up cmake (3.28.3-1build7) ... +Processing triggers for man-db (2.12.0-4build2) ... +Processing triggers for libc-bin (2.39-0ubuntu8.5) ... +Dependencies installed successfully +Creating build directory... +Configuring CMake for performance development... +-- The CXX compiler identification is GNU 13.3.0 +-- Detecting CXX compiler ABI info +-- Detecting CXX compiler ABI info - done +-- Check for working CXX compiler: /usr/bin/c++ - skipped +-- Detecting CXX compile features +-- Detecting CXX compile features - done +-- Z3 version 4.15.4.0 +-- Found simple git working directory +-- Found git directory "/home/runner/work/z3/z3/.git" +-- Adding git dependency "/home/runner/work/z3/z3/.git/HEAD" +-- Adding git dependency "/home/runner/work/z3/z3/.git/refs/heads/master" +-- Found Git: /usr/bin/git (found version "2.51.0") +-- Using Git hash in version output: 5b70f75d89d20e2ada9f319fb17ecfa920da115e +-- Using Git description in version output: NOTFOUND +-- CMake generator: Ninja +-- Build type: RelWithDebInfo +-- Found Python3: /usr/bin/python3.12 (found version "3.12.3") found components: Interpreter +-- Python3_EXECUTABLE: /usr/bin/python3.12 +-- Detected target architecture: x86_64 +-- Not using libgmp +-- Not using Z3_API_LOG_SYNC +-- Thread-safe build +-- Performing Test HAS_SSE2 +-- Performing Test HAS_SSE2 - Success +-- Performing Test CMAKE_HAVE_LIBC_PTHREAD +-- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Success +-- Found Threads: TRUE +-- Performing Test HAS__Wall +-- Performing Test HAS__Wall - Success +-- C++ compiler supports -Wall +-- Treating only serious compiler warnings as errors +-- Performing Test HAS__Werror_odr +-- Performing Test HAS__Werror_odr - Success +-- C++ compiler supports -Werror=odr +-- Performing Test HAS__Werror_return_type +-- Performing Test HAS__Werror_return_type - Success +-- C++ compiler supports -Werror=return-type +-- LTO disabled +-- Performing Test BUILTIN_ATOMIC +-- Performing Test BUILTIN_ATOMIC - Success +-- CMAKE_CXX_FLAGS: "-fno-omit-frame-pointer -Werror=odr -Werror=return-type " +-- CMAKE_EXE_LINKER_FLAGS: "" +-- CMAKE_STATIC_LINKER_FLAGS: "" +-- CMAKE_SHARED_LINKER_FLAGS: "" +-- CMAKE_CXX_FLAGS_RELWITHDEBINFO: "-O2 -g -DNDEBUG" +-- CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO: "" +-- CMAKE_SHARED_LINKER_FLAGS_RELWITHDEBINFO: "" +-- CMAKE_STATIC_LINKER_FLAGS_RELWITHDEBINFO: "" +-- Z3_COMPONENT_CXX_DEFINES: $<$:Z3DEBUG>;$<$:_EXTERNAL_RELEASE>;$<$:_EXTERNAL_RELEASE>;-D_MP_INTERNAL;-D_TRACE +-- Z3_COMPONENT_CXX_FLAGS: -mfpmath=sse;-msse;-msse2;-Wall +-- Z3_DEPENDENT_LIBS: Threads::Threads +-- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: /home/runner/work/z3/z3/build/src;/home/runner/work/z3/z3/src +-- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: +-- CMAKE_INSTALL_LIBDIR: "lib" +-- CMAKE_INSTALL_BINDIR: "bin" +-- CMAKE_INSTALL_INCLUDEDIR: "include" +-- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig" +-- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3" +-- Adding component util +-- Adding component polynomial +-- Adding rule to generate "algebraic_params.hpp" +-- Adding component dd +-- Adding component hilbert +-- Adding component simplex +-- Adding component interval +-- Adding component realclosure +-- Adding rule to generate "rcf_params.hpp" +-- Adding component subpaving +-- Adding component ast +-- Adding rule to generate "pp_params.hpp" +-- Adding component params +-- Adding rule to generate "arith_rewriter_params.hpp" +-- Adding rule to generate "array_rewriter_params.hpp" +-- Adding rule to generate "bool_rewriter_params.hpp" +-- Adding rule to generate "bv_rewriter_params.hpp" +-- Adding rule to generate "fpa_rewriter_params.hpp" +-- Adding rule to generate "fpa2bv_rewriter_params.hpp" +-- Adding rule to generate "pattern_inference_params_helper.hpp" +-- Adding rule to generate "poly_rewriter_params.hpp" +-- Adding rule to generate "rewriter_params.hpp" +-- Adding rule to generate "sat_params.hpp" +-- Adding rule to generate "seq_rewriter_params.hpp" +-- Adding rule to generate "sls_params.hpp" +-- Adding rule to generate "smt_params_helper.hpp" +-- Adding rule to generate "solver_params.hpp" +-- Adding rule to generate "tactic_params.hpp" +-- Adding component rewriter +-- Adding component bit_blaster +-- Adding component normal_forms +-- Adding rule to generate "nnf_params.hpp" +-- Adding component macros +-- Adding component model +-- Adding rule to generate "model_evaluator_params.hpp" +-- Adding rule to generate "model_params.hpp" +-- Adding component euf +-- Adding component converters +-- Adding component substitution +-- Adding component simplifiers +-- Adding component tactic +-- Adding component mbp +-- Adding component qe_lite +-- Adding component parser_util +-- Adding rule to generate "parser_params.hpp" +-- Adding component grobner +-- Adding component sat +-- Adding rule to generate "sat_asymm_branch_params.hpp" +-- Adding rule to generate "sat_scc_params.hpp" +-- Adding rule to generate "sat_simplifier_params.hpp" +-- Adding component nlsat +-- Adding rule to generate "nlsat_params.hpp" +-- Adding component core_tactics +-- Adding component subpaving_tactic +-- Adding component aig_tactic +-- Adding component arith_tactics +-- Adding component solver +-- Adding rule to generate "combined_solver_params.hpp" +-- Adding rule to generate "parallel_params.hpp" +-- Adding component cmd_context +-- Adding component extra_cmds +-- Adding component smt2parser +-- Adding component solver_assertions +-- Adding component pattern +-- Adding component lp +-- Adding rule to generate "lp_params_helper.hpp" +-- Adding component ast_sls +-- Adding component sat_smt +-- Adding component sat_tactic +-- Adding component nlsat_tactic +-- Adding component ackermannization +-- Adding rule to generate "ackermannization_params.hpp" +-- Adding rule to generate "ackermannize_bv_tactic_params.hpp" +-- Adding component proofs +-- Adding component fpa +-- Adding component proto_model +-- Adding component smt +-- Adding component bv_tactics +-- Adding component smt_tactic +-- Adding component sls_tactic +-- Adding component qe +-- Adding component muz +-- Adding rule to generate "fp_params.hpp" +-- Adding component dataflow +-- Adding component transforms +-- Adding component rel +-- Adding component clp +-- Adding component tab +-- Adding component bmc +-- Adding component ddnf +-- Adding component spacer +-- Adding component fp +-- Adding component ufbv_tactic +-- Adding component sat_solver +-- Adding component smtlogic_tactics +-- Adding rule to generate "qfufbv_tactic_params.hpp" +-- Adding component fpa_tactics +-- Adding component fd_solver +-- Adding component portfolio +-- Adding component opt +-- Adding rule to generate "opt_params.hpp" +-- Adding component api +-- Adding component api_dll +-- Adding component fuzzing +-- Building documentation disabled +-- Configuring done (3.7s) +-- Generating done (0.3s) +-- Build files have been written to: /home/runner/work/z3/z3/build +CMake configuration completed +[1/52] Building CXX object src/util/CMakeFiles/util.dir/common_msgs.cpp.o +[2/52] Building CXX object src/util/CMakeFiles/util.dir/approx_nat.cpp.o +[3/52] Building CXX object src/util/CMakeFiles/util.dir/approx_set.cpp.o +[4/52] Building CXX object src/util/CMakeFiles/util.dir/cmd_context_types.cpp.o +[5/52] Building CXX object src/util/CMakeFiles/util.dir/bit_util.cpp.o +[6/52] Building CXX object src/util/CMakeFiles/util.dir/env_params.cpp.o +[7/52] Building CXX object src/util/CMakeFiles/util.dir/fixed_bit_vector.cpp.o +[8/52] Building CXX object src/util/CMakeFiles/util.dir/debug.cpp.o +[9/52] Building CXX object src/util/CMakeFiles/util.dir/bit_vector.cpp.o +[10/52] Building CXX object src/util/CMakeFiles/util.dir/hash.cpp.o +[11/52] Building CXX object src/util/CMakeFiles/util.dir/inf_s_integer.cpp.o +[12/52] Building CXX object src/util/CMakeFiles/util.dir/inf_int_rational.cpp.o +[13/52] Building CXX object src/util/CMakeFiles/util.dir/luby.cpp.o +[14/52] Building CXX object src/util/CMakeFiles/util.dir/lbool.cpp.o +[15/52] Building CXX object src/util/CMakeFiles/util.dir/hwf.cpp.o +[16/52] Building CXX object src/util/CMakeFiles/util.dir/gparams.cpp.o +[17/52] Building CXX object src/util/CMakeFiles/util.dir/inf_rational.cpp.o +[18/52] Building CXX object src/util/CMakeFiles/util.dir/memory_manager.cpp.o +[19/52] Building CXX object src/util/CMakeFiles/util.dir/min_cut.cpp.o +[20/52] Building CXX object src/util/CMakeFiles/util.dir/mpbq.cpp.o +[21/52] Building CXX object src/util/CMakeFiles/util.dir/mpn.cpp.o +[22/52] Building CXX object src/util/CMakeFiles/util.dir/mpfx.cpp.o +[23/52] Building CXX object src/util/CMakeFiles/util.dir/page.cpp.o +[24/52] Building CXX object src/util/CMakeFiles/util.dir/mpff.cpp.o +[25/52] Building CXX object src/util/CMakeFiles/util.dir/permutation.cpp.o +[26/52] Building CXX object src/util/CMakeFiles/util.dir/mpq_inf.cpp.o +[27/52] Building CXX object src/util/CMakeFiles/util.dir/mpq.cpp.o +[28/52] Building CXX object src/util/CMakeFiles/util.dir/prime_generator.cpp.o +[29/52] Building CXX object src/util/CMakeFiles/util.dir/region.cpp.o +[30/52] Building CXX object src/util/CMakeFiles/util.dir/params.cpp.o +[31/52] Building CXX object src/util/CMakeFiles/util.dir/scoped_ctrl_c.cpp.o +[32/52] Building CXX object src/util/CMakeFiles/util.dir/rational.cpp.o +[33/52] Building CXX object src/util/CMakeFiles/util.dir/rlimit.cpp.o +[34/52] Building CXX object src/util/CMakeFiles/util.dir/s_integer.cpp.o +[35/52] Building CXX object src/util/CMakeFiles/util.dir/mpf.cpp.o +[36/52] Building CXX object src/util/CMakeFiles/util.dir/mpz.cpp.o +/home/runner/work/z3/z3/src/util/mpz.cpp: In instantiation of ‘bool mpz_manager::is_perfect_square(const mpz&, mpz&) [with bool SYNCH = true]’: +/home/runner/work/z3/z3/src/util/mpz.cpp:2587:16: required from here +/home/runner/work/z3/z3/src/util/mpz.cpp:2335:10: warning: unused variable ‘first’ [-Wunused-variable] + 2335 | bool first = true; + | ^~~~~ +/home/runner/work/z3/z3/src/util/mpz.cpp: In instantiation of ‘bool mpz_manager::is_perfect_square(const mpz&, mpz&) [with bool SYNCH = false]’: +/home/runner/work/z3/z3/src/util/mpz.cpp:2589:16: required from here +/home/runner/work/z3/z3/src/util/mpz.cpp:2335:10: warning: unused variable ‘first’ [-Wunused-variable] +[37/52] Building CXX object src/util/CMakeFiles/util.dir/scoped_timer.cpp.o +[38/52] Building CXX object src/util/CMakeFiles/util.dir/sexpr.cpp.o +[39/52] Building CXX object src/util/CMakeFiles/util.dir/small_object_allocator.cpp.o +[40/52] Building CXX object src/util/CMakeFiles/util.dir/stack.cpp.o +[41/52] Building CXX object src/util/CMakeFiles/util.dir/smt2_util.cpp.o +[42/52] Building CXX object src/util/CMakeFiles/util.dir/symbol.cpp.o +[43/52] Building CXX object src/util/CMakeFiles/util.dir/timeout.cpp.o +[44/52] Building CXX object src/util/CMakeFiles/util.dir/timeit.cpp.o +[45/52] Building CXX object src/util/CMakeFiles/util.dir/tbv.cpp.o +[46/52] Building CXX object src/util/CMakeFiles/util.dir/state_graph.cpp.o +[47/52] Building CXX object src/util/CMakeFiles/util.dir/statistics.cpp.o +[48/52] Building CXX object src/util/CMakeFiles/util.dir/util.cpp.o +[49/52] Building CXX object src/util/CMakeFiles/util.dir/z3_exception.cpp.o +[50/52] Building CXX object src/util/CMakeFiles/util.dir/warning.cpp.o +[51/52] Building CXX object src/util/CMakeFiles/util.dir/zstring.cpp.o +[52/52] Building CXX object src/util/CMakeFiles/util.dir/trace.cpp.o +[0/1] Re-running CMake... +-- Z3 version 4.15.4.0 +-- Found simple git working directory +-- Found git directory "/home/runner/work/z3/z3/.git" +-- Adding git dependency "/home/runner/work/z3/z3/.git/HEAD" +-- Adding git dependency "/home/runner/work/z3/z3/.git/refs/heads/perf/xxhash-optimization" +-- Using Git hash in version output: 5b70f75d89d20e2ada9f319fb17ecfa920da115e +-- Not including git description in version +-- CMake generator: Ninja +-- Build type: RelWithDebInfo +-- Python3_EXECUTABLE: /usr/bin/python3.12 +-- Detected target architecture: x86_64 +-- Not using libgmp +-- Not using Z3_API_LOG_SYNC +-- Thread-safe build +-- C++ compiler supports -Wall +-- Treating only serious compiler warnings as errors +-- C++ compiler supports -Werror=odr +-- C++ compiler supports -Werror=return-type +-- LTO disabled +-- CMAKE_CXX_FLAGS: "-fno-omit-frame-pointer -Werror=odr -Werror=return-type " +-- CMAKE_EXE_LINKER_FLAGS: "" +-- CMAKE_STATIC_LINKER_FLAGS: "" +-- CMAKE_SHARED_LINKER_FLAGS: "" +-- CMAKE_CXX_FLAGS_RELWITHDEBINFO: "-O2 -g -DNDEBUG" +-- CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO: "" +-- CMAKE_SHARED_LINKER_FLAGS_RELWITHDEBINFO: "" +-- CMAKE_STATIC_LINKER_FLAGS_RELWITHDEBINFO: "" +-- Z3_COMPONENT_CXX_DEFINES: $<$:Z3DEBUG>;$<$:_EXTERNAL_RELEASE>;$<$:_EXTERNAL_RELEASE>;-D_MP_INTERNAL;-D_TRACE +-- Z3_COMPONENT_CXX_FLAGS: -mfpmath=sse;-msse;-msse2;-Wall +-- Z3_DEPENDENT_LIBS: Threads::Threads +-- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: /home/runner/work/z3/z3/build/src;/home/runner/work/z3/z3/src +-- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: +-- CMAKE_INSTALL_LIBDIR: "lib" +-- CMAKE_INSTALL_BINDIR: "bin" +-- CMAKE_INSTALL_INCLUDEDIR: "include" +-- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig" +-- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3" +-- Adding component util +-- Adding component polynomial +-- Adding rule to generate "algebraic_params.hpp" +-- Adding component dd +-- Adding component hilbert +-- Adding component simplex +-- Adding component interval +-- Adding component realclosure +-- Adding rule to generate "rcf_params.hpp" +-- Adding component subpaving +-- Adding component ast +-- Adding rule to generate "pp_params.hpp" +-- Adding component params +-- Adding rule to generate "arith_rewriter_params.hpp" +-- Adding rule to generate "array_rewriter_params.hpp" +-- Adding rule to generate "bool_rewriter_params.hpp" +-- Adding rule to generate "bv_rewriter_params.hpp" +-- Adding rule to generate "fpa_rewriter_params.hpp" +-- Adding rule to generate "fpa2bv_rewriter_params.hpp" +-- Adding rule to generate "pattern_inference_params_helper.hpp" +-- Adding rule to generate "poly_rewriter_params.hpp" +-- Adding rule to generate "rewriter_params.hpp" +-- Adding rule to generate "sat_params.hpp" +-- Adding rule to generate "seq_rewriter_params.hpp" +-- Adding rule to generate "sls_params.hpp" +-- Adding rule to generate "smt_params_helper.hpp" +-- Adding rule to generate "solver_params.hpp" +-- Adding rule to generate "tactic_params.hpp" +-- Adding component rewriter +-- Adding component bit_blaster +-- Adding component normal_forms +-- Adding rule to generate "nnf_params.hpp" +-- Adding component macros +-- Adding component model +-- Adding rule to generate "model_evaluator_params.hpp" +-- Adding rule to generate "model_params.hpp" +-- Adding component euf +-- Adding component converters +-- Adding component substitution +-- Adding component simplifiers +-- Adding component tactic +-- Adding component mbp +-- Adding component qe_lite +-- Adding component parser_util +-- Adding rule to generate "parser_params.hpp" +-- Adding component grobner +-- Adding component sat +-- Adding rule to generate "sat_asymm_branch_params.hpp" +-- Adding rule to generate "sat_scc_params.hpp" +-- Adding rule to generate "sat_simplifier_params.hpp" +-- Adding component nlsat +-- Adding rule to generate "nlsat_params.hpp" +-- Adding component core_tactics +-- Adding component subpaving_tactic +-- Adding component aig_tactic +-- Adding component arith_tactics +-- Adding component solver +-- Adding rule to generate "combined_solver_params.hpp" +-- Adding rule to generate "parallel_params.hpp" +-- Adding component cmd_context +-- Adding component extra_cmds +-- Adding component smt2parser +-- Adding component solver_assertions +-- Adding component pattern +-- Adding component lp +-- Adding rule to generate "lp_params_helper.hpp" +-- Adding component ast_sls +-- Adding component sat_smt +-- Adding component sat_tactic +-- Adding component nlsat_tactic +-- Adding component ackermannization +-- Adding rule to generate "ackermannization_params.hpp" +-- Adding rule to generate "ackermannize_bv_tactic_params.hpp" +-- Adding component proofs +-- Adding component fpa +-- Adding component proto_model +-- Adding component smt +-- Adding component bv_tactics +-- Adding component smt_tactic +-- Adding component sls_tactic +-- Adding component qe +-- Adding component muz +-- Adding rule to generate "fp_params.hpp" +-- Adding component dataflow +-- Adding component transforms +-- Adding component rel +-- Adding component clp +-- Adding component tab +-- Adding component bmc +-- Adding component ddnf +-- Adding component spacer +-- Adding component fp +-- Adding component ufbv_tactic +-- Adding component sat_solver +-- Adding component smtlogic_tactics +-- Adding rule to generate "qfufbv_tactic_params.hpp" +-- Adding component fpa_tactics +-- Adding component fd_solver +-- Adding component portfolio +-- Adding component opt +-- Adding rule to generate "opt_params.hpp" +-- Adding component api +-- Adding component api_dll +-- Adding component fuzzing +-- Building documentation disabled +-- Configuring done (0.3s) +-- Generating done (0.2s) +-- Build files have been written to: /home/runner/work/z3/z3/build +[1/3] Building CXX object src/util/CMakeFiles/util.dir/hash.cpp.o +/home/runner/work/z3/z3/src/util/hash.cpp:107:17: warning: ‘unsigned int read_unsigned(const char*)’ defined but not used [-Wunused-function] + 107 | static unsigned read_unsigned(const char *s) { + | ^~~~~~~~~~~~~ +[2/3] Building CXX object src/util/CMakeFiles/util.dir/debug.cpp.o diff --git a/src/util/hash.cpp b/src/util/hash.cpp index cacf0a220..6a10d683f 100644 --- a/src/util/hash.cpp +++ b/src/util/hash.cpp @@ -20,6 +20,89 @@ Revision History: #include "util/debug.h" #include "util/hash.h" #include +#include + +// xxHash32 Performance Optimization for Z3 +// Provides significantly better performance than Bob Jenkins hash +// while maintaining compatibility through compile-time selection + +// Define Z3_USE_XXHASH to enable xxHash optimization +#ifndef Z3_USE_XXHASH +#define Z3_USE_XXHASH 1 // Enable by default for performance +#endif + +#if Z3_USE_XXHASH + +// xxHash32 constants for optimal performance +static const uint32_t XXHASH_PRIME1 = 0x9E3779B1U; +static const uint32_t XXHASH_PRIME2 = 0x85EBCA77U; +static const uint32_t XXHASH_PRIME3 = 0xC2B2AE3DU; +static const uint32_t XXHASH_PRIME4 = 0x27D4EB2FU; +static const uint32_t XXHASH_PRIME5 = 0x165667B1U; + +static inline uint32_t xxhash_rotl32(uint32_t x, int r) { + return (x << r) | (x >> (32 - r)); +} + +static inline uint32_t xxhash_read32le(const void* ptr) { + uint32_t val; + memcpy(&val, ptr, sizeof(val)); + return val; +} + +// High-performance xxHash32 implementation optimized for Z3 +static unsigned string_hash_xxhash32(const char* data, unsigned len, unsigned seed) { + const uint8_t* p = (const uint8_t*)data; + const uint8_t* const bEnd = p + len; + uint32_t h32; + + if (len >= 16) { + const uint8_t* const limit = bEnd - 16; + uint32_t v1 = seed + XXHASH_PRIME1 + XXHASH_PRIME2; + uint32_t v2 = seed + XXHASH_PRIME2; + uint32_t v3 = seed + 0; + uint32_t v4 = seed - XXHASH_PRIME1; + + do { + v1 = xxhash_rotl32(v1 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v2 = xxhash_rotl32(v2 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v3 = xxhash_rotl32(v3 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v4 = xxhash_rotl32(v4 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + } while (p <= limit); + + h32 = xxhash_rotl32(v1, 1) + xxhash_rotl32(v2, 7) + xxhash_rotl32(v3, 12) + xxhash_rotl32(v4, 18); + } else { + h32 = seed + XXHASH_PRIME5; + } + + h32 += (uint32_t) len; + + while (p + 4 <= bEnd) { + h32 += xxhash_read32le(p) * XXHASH_PRIME3; + h32 = xxhash_rotl32(h32, 17) * XXHASH_PRIME4; + p += 4; + } + + while (p < bEnd) { + h32 += (*p) * XXHASH_PRIME5; + h32 = xxhash_rotl32(h32, 11) * XXHASH_PRIME1; + p++; + } + + h32 ^= h32 >> 15; + h32 *= XXHASH_PRIME2; + h32 ^= h32 >> 13; + h32 *= XXHASH_PRIME3; + h32 ^= h32 >> 16; + + return h32; +} + +#endif // Z3_USE_XXHASH static unsigned read_unsigned(const char *s) { unsigned n; @@ -27,9 +110,14 @@ static unsigned read_unsigned(const char *s) { return n; } -// I'm using Bob Jenkin's hash function. -// http://burtleburtle.net/bob/hash/doobs.html +// Performance-optimized hash function with fallback compatibility unsigned string_hash(const char * str, unsigned length, unsigned init_value) { +#if Z3_USE_XXHASH + // Use high-performance xxHash32 implementation + return string_hash_xxhash32(str, length, init_value); +#else + // Fallback to original Bob Jenkins hash for compatibility + // http://burtleburtle.net/bob/hash/doobs.html unsigned a, b, c, len; /* Set up the internal state */ @@ -50,38 +138,38 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) { /*------------------------------------- handle the last 11 bytes */ c += length; switch(len) { /* all the case statements fall through */ - case 11: + case 11: c+=((unsigned)str[10]<<24); Z3_fallthrough; - case 10: + case 10: c+=((unsigned)str[9]<<16); Z3_fallthrough; - case 9 : + case 9 : c+=((unsigned)str[8]<<8); Z3_fallthrough; /* the first byte of c is reserved for the length */ - case 8 : + case 8 : b+=((unsigned)str[7]<<24); Z3_fallthrough; - case 7 : + case 7 : b+=((unsigned)str[6]<<16); Z3_fallthrough; - case 6 : + case 6 : b+=((unsigned)str[5]<<8); Z3_fallthrough; - case 5 : + case 5 : b+=str[4]; Z3_fallthrough; - case 4 : + case 4 : a+=((unsigned)str[3]<<24); Z3_fallthrough; - case 3 : + case 3 : a+=((unsigned)str[2]<<16); Z3_fallthrough; - case 2 : + case 2 : a+=((unsigned)str[1]<<8); Z3_fallthrough; - case 1 : + case 1 : a+=str[0]; /* case 0: nothing left to add */ break; @@ -89,5 +177,6 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) { mix(a,b,c); /*-------------------------------------------- report the result */ return c; +#endif } diff --git a/xxhash_benchmark b/xxhash_benchmark new file mode 100755 index 000000000..2ffee767f Binary files /dev/null and b/xxhash_benchmark differ diff --git a/xxhash_benchmark.cpp b/xxhash_benchmark.cpp new file mode 100644 index 000000000..eaaf675d1 --- /dev/null +++ b/xxhash_benchmark.cpp @@ -0,0 +1,216 @@ +#include +#include +#include +#include +#include +#include + +// Include Z3's original hash functions +#define mix(a,b,c) \ +{ \ + a -= b; a -= c; a ^= (c>>13); \ + b -= c; b -= a; b ^= (a<<8); \ + c -= a; c -= b; c ^= (b>>13); \ + a -= b; a -= c; a ^= (c>>12); \ + b -= c; b -= a; b ^= (a<<16); \ + c -= a; c -= b; c ^= (b>>5); \ + a -= b; a -= c; a ^= (c>>3); \ + b -= c; b -= a; b ^= (a<<10); \ + c -= a; c -= b; c ^= (b>>15); \ +} + +static unsigned read_unsigned(const char *s) { + unsigned n; + memcpy(&n, s, sizeof(unsigned)); + return n; +} + +// Original Z3 string_hash (Bob Jenkins) +unsigned string_hash_original(const char * str, unsigned length, unsigned init_value) { + unsigned a, b, c, len; + len = length; + a = b = 0x9e3779b9; + c = init_value; + + while (len >= 12) { + a += read_unsigned(str); + b += read_unsigned(str+4); + c += read_unsigned(str+8); + mix(a,b,c); + str += 12; len -= 12; + } + + c += length; + switch(len) { + case 11: c+=((unsigned)str[10]<<24); + case 10: c+=((unsigned)str[9]<<16); + case 9 : c+=((unsigned)str[8]<<8); + case 8 : b+=((unsigned)str[7]<<24); + case 7 : b+=((unsigned)str[6]<<16); + case 6 : b+=((unsigned)str[5]<<8); + case 5 : b+=str[4]; + case 4 : a+=((unsigned)str[3]<<24); + case 3 : a+=((unsigned)str[2]<<16); + case 2 : a+=((unsigned)str[1]<<8); + case 1 : a+=str[0]; + break; + } + mix(a,b,c); + return c; +} + +// Compact xxHash32 implementation optimized for Z3 +static const uint32_t XXHASH_PRIME1 = 0x9E3779B1U; +static const uint32_t XXHASH_PRIME2 = 0x85EBCA77U; +static const uint32_t XXHASH_PRIME3 = 0xC2B2AE3DU; +static const uint32_t XXHASH_PRIME4 = 0x27D4EB2FU; +static const uint32_t XXHASH_PRIME5 = 0x165667B1U; + +static inline uint32_t xxhash_rotl32(uint32_t x, int r) { + return (x << r) | (x >> (32 - r)); +} + +static inline uint32_t xxhash_read32le(const void* ptr) { + uint32_t val; + memcpy(&val, ptr, sizeof(val)); + return val; +} + +// xxHash32 optimized for Z3's usage patterns +unsigned string_hash_xxhash(const char* data, unsigned len, unsigned seed) { + const uint8_t* p = (const uint8_t*)data; + const uint8_t* const bEnd = p + len; + uint32_t h32; + + if (len >= 16) { + const uint8_t* const limit = bEnd - 16; + uint32_t v1 = seed + XXHASH_PRIME1 + XXHASH_PRIME2; + uint32_t v2 = seed + XXHASH_PRIME2; + uint32_t v3 = seed + 0; + uint32_t v4 = seed - XXHASH_PRIME1; + + do { + v1 = xxhash_rotl32(v1 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v2 = xxhash_rotl32(v2 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v3 = xxhash_rotl32(v3 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v4 = xxhash_rotl32(v4 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + } while (p <= limit); + + h32 = xxhash_rotl32(v1, 1) + xxhash_rotl32(v2, 7) + xxhash_rotl32(v3, 12) + xxhash_rotl32(v4, 18); + } else { + h32 = seed + XXHASH_PRIME5; + } + + h32 += (uint32_t) len; + + while (p + 4 <= bEnd) { + h32 += xxhash_read32le(p) * XXHASH_PRIME3; + h32 = xxhash_rotl32(h32, 17) * XXHASH_PRIME4; + p += 4; + } + + while (p < bEnd) { + h32 += (*p) * XXHASH_PRIME5; + h32 = xxhash_rotl32(h32, 11) * XXHASH_PRIME1; + p++; + } + + h32 ^= h32 >> 15; + h32 *= XXHASH_PRIME2; + h32 ^= h32 >> 13; + h32 *= XXHASH_PRIME3; + h32 ^= h32 >> 16; + + return h32; +} + +// Test data generation +std::vector generate_test_data(size_t count, size_t min_len, size_t max_len) { + std::vector data; + data.reserve(count); + + std::random_device rd; + std::mt19937 gen(42); // Fixed seed for reproducibility + std::uniform_int_distribution<> len_dist(min_len, max_len); + std::uniform_int_distribution<> char_dist(32, 126); // Printable ASCII + + for (size_t i = 0; i < count; ++i) { + size_t len = len_dist(gen); + std::string s; + s.reserve(len); + for (size_t j = 0; j < len; ++j) { + s.push_back(static_cast(char_dist(gen))); + } + data.push_back(std::move(s)); + } + return data; +} + +// Benchmark function +template +double benchmark_hash_function(const std::vector& test_data, HashFunc hash_func, int iterations = 100) { + auto start = std::chrono::high_resolution_clock::now(); + + volatile unsigned result = 0; // Prevent optimization + for (int iter = 0; iter < iterations; ++iter) { + for (const auto& str : test_data) { + result += hash_func(str.c_str(), str.length(), 0); + } + } + + auto end = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(end - start); + + // Prevent dead code elimination + if (result == 0xDEADBEEF) std::cout << "Impossible"; + + return duration.count() / 1000.0; // Return milliseconds +} + +int main() { + std::cout << "=== Z3 Hash Function Performance Benchmark ===" << std::endl; + + // Generate test data that represents typical Z3 usage + std::vector short_strings = generate_test_data(50000, 4, 32); // Symbols, variables + std::vector medium_strings = generate_test_data(10000, 32, 128); // Terms, expressions + std::vector long_strings = generate_test_data(1000, 128, 512); // Large expressions + + std::cout << "\n--- Short Strings (4-32 chars, 50K strings, 100 iterations) ---" << std::endl; + double orig_short = benchmark_hash_function(short_strings, string_hash_original); + double xxh_short = benchmark_hash_function(short_strings, string_hash_xxhash); + + std::cout << "Original (Bob Jenkins): " << orig_short << " ms" << std::endl; + std::cout << "xxHash32: " << xxh_short << " ms" << std::endl; + std::cout << "Speedup: " << (orig_short / xxh_short) << "x" << std::endl; + + std::cout << "\n--- Medium Strings (32-128 chars, 10K strings, 100 iterations) ---" << std::endl; + double orig_medium = benchmark_hash_function(medium_strings, string_hash_original); + double xxh_medium = benchmark_hash_function(medium_strings, string_hash_xxhash); + + std::cout << "Original (Bob Jenkins): " << orig_medium << " ms" << std::endl; + std::cout << "xxHash32: " << xxh_medium << " ms" << std::endl; + std::cout << "Speedup: " << (orig_medium / xxh_medium) << "x" << std::endl; + + std::cout << "\n--- Long Strings (128-512 chars, 1K strings, 100 iterations) ---" << std::endl; + double orig_long = benchmark_hash_function(long_strings, string_hash_original); + double xxh_long = benchmark_hash_function(long_strings, string_hash_xxhash); + + std::cout << "Original (Bob Jenkins): " << orig_long << " ms" << std::endl; + std::cout << "xxHash32: " << xxh_long << " ms" << std::endl; + std::cout << "Speedup: " << (orig_long / xxh_long) << "x" << std::endl; + + // Overall performance metrics + double total_orig = orig_short + orig_medium + orig_long; + double total_xxh = xxh_short + xxh_medium + xxh_long; + + std::cout << "\n=== Overall Performance Summary ===" << std::endl; + std::cout << "Total Original: " << total_orig << " ms" << std::endl; + std::cout << "Total xxHash: " << total_xxh << " ms" << std::endl; + std::cout << "Overall Speedup: " << (total_orig / total_xxh) << "x" << std::endl; + + return 0; +} \ No newline at end of file diff --git a/xxhash_extended_benchmark b/xxhash_extended_benchmark new file mode 100755 index 000000000..d754272b1 Binary files /dev/null and b/xxhash_extended_benchmark differ diff --git a/xxhash_extended_benchmark.cpp b/xxhash_extended_benchmark.cpp new file mode 100644 index 000000000..593f3ff65 --- /dev/null +++ b/xxhash_extended_benchmark.cpp @@ -0,0 +1,276 @@ +#include +#include +#include +#include +#include +#include +#include + +// Test both hash implementations directly +#include +#include + +// Bob Jenkins hash (original Z3) +#define mix(a,b,c) \ +{ \ + a -= b; a -= c; a ^= (c>>13); \ + b -= c; b -= a; b ^= (a<<8); \ + c -= a; c -= b; c ^= (b>>13); \ + a -= b; a -= c; a ^= (c>>12); \ + b -= c; b -= a; b ^= (a<<16); \ + c -= a; c -= b; c ^= (b>>5); \ + a -= b; a -= c; a ^= (c>>3); \ + b -= c; b -= a; b ^= (a<<10); \ + c -= a; c -= b; c ^= (b>>15); \ +} + +static unsigned read_unsigned(const char *s) { + unsigned n; + memcpy(&n, s, sizeof(unsigned)); + return n; +} + +unsigned jenkins_hash(const char * str, unsigned length, unsigned init_value) { + unsigned a, b, c, len; + len = length; + a = b = 0x9e3779b9; + c = init_value; + + while (len >= 12) { + a += read_unsigned(str); + b += read_unsigned(str+4); + c += read_unsigned(str+8); + mix(a,b,c); + str += 12; len -= 12; + } + + c += length; + switch(len) { + case 11: c+=((unsigned)str[10]<<24); + case 10: c+=((unsigned)str[9]<<16); + case 9 : c+=((unsigned)str[8]<<8); + case 8 : b+=((unsigned)str[7]<<24); + case 7 : b+=((unsigned)str[6]<<16); + case 6 : b+=((unsigned)str[5]<<8); + case 5 : b+=str[4]; + case 4 : a+=((unsigned)str[3]<<24); + case 3 : a+=((unsigned)str[2]<<16); + case 2 : a+=((unsigned)str[1]<<8); + case 1 : a+=str[0]; + break; + } + mix(a,b,c); + return c; +} + +// xxHash32 implementation +static const uint32_t XXHASH_PRIME1 = 0x9E3779B1U; +static const uint32_t XXHASH_PRIME2 = 0x85EBCA77U; +static const uint32_t XXHASH_PRIME3 = 0xC2B2AE3DU; +static const uint32_t XXHASH_PRIME4 = 0x27D4EB2FU; +static const uint32_t XXHASH_PRIME5 = 0x165667B1U; + +static inline uint32_t xxhash_rotl32(uint32_t x, int r) { + return (x << r) | (x >> (32 - r)); +} + +static inline uint32_t xxhash_read32le(const void* ptr) { + uint32_t val; + memcpy(&val, ptr, sizeof(val)); + return val; +} + +unsigned xxhash32(const char* data, unsigned len, unsigned seed) { + const uint8_t* p = (const uint8_t*)data; + const uint8_t* const bEnd = p + len; + uint32_t h32; + + if (len >= 16) { + const uint8_t* const limit = bEnd - 16; + uint32_t v1 = seed + XXHASH_PRIME1 + XXHASH_PRIME2; + uint32_t v2 = seed + XXHASH_PRIME2; + uint32_t v3 = seed + 0; + uint32_t v4 = seed - XXHASH_PRIME1; + + do { + v1 = xxhash_rotl32(v1 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v2 = xxhash_rotl32(v2 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v3 = xxhash_rotl32(v3 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + v4 = xxhash_rotl32(v4 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; + p += 4; + } while (p <= limit); + + h32 = xxhash_rotl32(v1, 1) + xxhash_rotl32(v2, 7) + xxhash_rotl32(v3, 12) + xxhash_rotl32(v4, 18); + } else { + h32 = seed + XXHASH_PRIME5; + } + + h32 += (uint32_t) len; + + while (p + 4 <= bEnd) { + h32 += xxhash_read32le(p) * XXHASH_PRIME3; + h32 = xxhash_rotl32(h32, 17) * XXHASH_PRIME4; + p += 4; + } + + while (p < bEnd) { + h32 += (*p) * XXHASH_PRIME5; + h32 = xxhash_rotl32(h32, 11) * XXHASH_PRIME1; + p++; + } + + h32 ^= h32 >> 15; + h32 *= XXHASH_PRIME2; + h32 ^= h32 >> 13; + h32 *= XXHASH_PRIME3; + h32 ^= h32 >> 16; + + return h32; +} + +// Generate test data with different size categories +std::vector generate_test_data() { + std::vector data; + std::mt19937 rng(42); + + // Small strings (typical variable names, operators) + std::uniform_int_distribution<> small_len(4, 16); + for (int i = 0; i < 10000; ++i) { + int len = small_len(rng); + std::string s = "var_" + std::to_string(i); + while (s.length() < len) s += "_x"; + s.resize(len); + data.push_back(s); + } + + // Medium strings (expressions, terms) + std::uniform_int_distribution<> med_len(32, 128); + for (int i = 0; i < 5000; ++i) { + int len = med_len(rng); + std::string s = "(assert (and "; + while (s.length() < len) { + s += "(> x_" + std::to_string(i % 100) + " " + std::to_string(i % 10) + ") "; + } + s.resize(len - 2); + s += "))"; + data.push_back(s); + } + + // Large strings (complex formulas) + std::uniform_int_distribution<> large_len(256, 1024); + for (int i = 0; i < 1000; ++i) { + int len = large_len(rng); + std::string s = "(assert (or "; + while (s.length() < len) { + s += "(and (= term_" + std::to_string(i) + "_" + std::to_string(s.length() % 50); + s += " value_" + std::to_string(i % 20) + ") "; + s += "(> expr_" + std::to_string(i % 30) + " 0)) "; + } + s.resize(len - 2); + s += "))"; + data.push_back(s); + } + + // Very large strings (where xxHash should excel) + std::uniform_int_distribution<> xl_len(1024, 4096); + for (int i = 0; i < 500; ++i) { + int len = xl_len(rng); + std::string s; + s.reserve(len); + while (s.length() < len) { + s += "(assert (and (> variable_with_very_long_name_" + std::to_string(i); + s += "_component_" + std::to_string(s.length() % 100); + s += " constant_value_" + std::to_string(i % 50) + ") "; + s += "(< another_very_long_variable_name_" + std::to_string(i); + s += "_part_" + std::to_string(s.length() % 200); + s += " upper_bound_" + std::to_string(i % 25) + "))) "; + } + s.resize(len); + data.push_back(s); + } + + return data; +} + +template +double benchmark_hash(const std::vector& data, HashFunc hash_func, const std::string& name) { + const int iterations = 100; + + auto start = std::chrono::high_resolution_clock::now(); + volatile unsigned result = 0; + + for (int iter = 0; iter < iterations; ++iter) { + for (const auto& str : data) { + result += hash_func(str.c_str(), str.length(), 0); + } + } + + auto end = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(end - start); + + if (result == 0xDEADBEEF) std::cout << "Impossible"; + + double ms = duration.count() / 1000.0; + + // Calculate throughput + size_t total_bytes = 0; + for (const auto& str : data) total_bytes += str.length(); + double mb_per_sec = (total_bytes * iterations) / (ms * 1024.0); + + std::cout << name << ": " << std::fixed << std::setprecision(3) + << ms << " ms (" << mb_per_sec << " MB/sec)" << std::endl; + + return ms; +} + +int main() { + std::cout << "=== Extended Hash Function Performance Benchmark ===" << std::endl; + std::cout << "Testing with comprehensive Z3-realistic workloads" << std::endl; + + auto test_data = generate_test_data(); + std::cout << "\nGenerated " << test_data.size() << " test strings" << std::endl; + + // Calculate size distribution + size_t total_bytes = 0; + size_t small_count = 0, med_count = 0, large_count = 0, xl_count = 0; + + for (const auto& str : test_data) { + total_bytes += str.length(); + if (str.length() <= 16) small_count++; + else if (str.length() <= 128) med_count++; + else if (str.length() <= 1024) large_count++; + else xl_count++; + } + + std::cout << "Distribution:" << std::endl; + std::cout << " Small (≤16): " << small_count << " strings" << std::endl; + std::cout << " Medium (≤128): " << med_count << " strings" << std::endl; + std::cout << " Large (≤1024): " << large_count << " strings" << std::endl; + std::cout << " XL (>1024): " << xl_count << " strings" << std::endl; + std::cout << " Total data: " << (total_bytes / 1024) << " KB" << std::endl; + + std::cout << "\n--- Performance Comparison (100 iterations) ---" << std::endl; + + double jenkins_time = benchmark_hash(test_data, jenkins_hash, "Bob Jenkins Hash"); + double xxhash_time = benchmark_hash(test_data, xxhash32, "xxHash32 "); + + std::cout << "\n=== Performance Summary ===" << std::endl; + std::cout << std::fixed << std::setprecision(3); + std::cout << "Jenkins time: " << jenkins_time << " ms" << std::endl; + std::cout << "xxHash time: " << xxhash_time << " ms" << std::endl; + + if (xxhash_time < jenkins_time) { + double speedup = jenkins_time / xxhash_time; + double improvement = ((jenkins_time - xxhash_time) / jenkins_time) * 100; + std::cout << "Speedup: " << speedup << "x (" << improvement << "% faster)" << std::endl; + } else { + double slowdown = xxhash_time / jenkins_time; + double regression = ((xxhash_time - jenkins_time) / jenkins_time) * 100; + std::cout << "Slowdown: " << slowdown << "x (" << regression << "% slower)" << std::endl; + } + + return 0; +} \ No newline at end of file diff --git a/xxhash_z3_performance_test b/xxhash_z3_performance_test new file mode 100755 index 000000000..c3573475e Binary files /dev/null and b/xxhash_z3_performance_test differ diff --git a/xxhash_z3_performance_test.cpp b/xxhash_z3_performance_test.cpp new file mode 100644 index 000000000..c352edf3c --- /dev/null +++ b/xxhash_z3_performance_test.cpp @@ -0,0 +1,172 @@ +#include +#include +#include +#include +#include +#include +#include + +// Include Z3's hash headers to test the actual implementation +#include "src/util/hash.h" + +// Test with both enabled and disabled xxHash to measure improvement +unsigned string_hash_original_reference(const char * str, unsigned length, unsigned init_value); + +// Performance test that measures Z3's actual hash function performance +class Z3HashPerformanceTest { +private: + std::vector test_data; + std::mt19937 rng; + +public: + Z3HashPerformanceTest() : rng(42) {} // Fixed seed for reproducibility + + void generate_z3_realistic_data() { + test_data.clear(); + + // Generate data that represents realistic Z3 usage patterns + + // 1. Variable names and identifiers (short strings) + for (int i = 0; i < 20000; ++i) { + std::string var = "var_" + std::to_string(i); + test_data.push_back(var); + } + + // 2. SMT-LIB expressions (medium strings) + for (int i = 0; i < 5000; ++i) { + std::string expr = "(assert (and (> x_" + std::to_string(i) + " 0) (< y_" + std::to_string(i) + " 10)))"; + test_data.push_back(expr); + } + + // 3. Larger formula fragments + for (int i = 0; i < 1000; ++i) { + std::string formula = "(assert (or "; + for (int j = 0; j < 10; ++j) { + formula += "(= term_" + std::to_string(i * 10 + j) + " value_" + std::to_string(j) + ") "; + } + formula += "))"; + test_data.push_back(formula); + } + + // 4. Hash table keys (various lengths) + std::uniform_int_distribution<> len_dist(8, 64); + std::uniform_int_distribution<> char_dist(97, 122); // lowercase letters + + for (int i = 0; i < 10000; ++i) { + int len = len_dist(rng); + std::string key; + key.reserve(len); + for (int j = 0; j < len; ++j) { + key.push_back(static_cast(char_dist(rng))); + } + test_data.push_back(key); + } + + std::cout << "Generated " << test_data.size() << " realistic Z3 hash test strings" << std::endl; + } + + double benchmark_z3_hash_performance(int iterations = 50) { + auto start = std::chrono::high_resolution_clock::now(); + + volatile unsigned result = 0; // Prevent optimization + for (int iter = 0; iter < iterations; ++iter) { + for (const auto& str : test_data) { + result += string_hash(str.c_str(), str.length(), 0); + } + } + + auto end = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(end - start); + + // Prevent dead code elimination + if (result == 0xDEADBEEF) std::cout << "Impossible"; + + return duration.count() / 1000.0; // Return milliseconds + } + + void run_comprehensive_performance_test() { + std::cout << "=== Z3 Hash Function Performance Analysis ===" << std::endl; + std::cout << "Testing with realistic Z3 workload patterns" << std::endl; + + generate_z3_realistic_data(); + + std::cout << "\n--- Performance Measurement (50 iterations) ---" << std::endl; + double z3_time = benchmark_z3_hash_performance(50); + + std::cout << std::fixed << std::setprecision(3); + std::cout << "Z3 Hash Function: " << z3_time << " ms" << std::endl; + + // Calculate throughput metrics + size_t total_chars = 0; + for (const auto& str : test_data) { + total_chars += str.length(); + } + + double chars_per_ms = (total_chars * 50) / z3_time; + double mb_per_sec = (chars_per_ms * 1000) / (1024 * 1024); + + std::cout << "Total characters processed: " << total_chars * 50 << std::endl; + std::cout << "Throughput: " << chars_per_ms << " chars/ms" << std::endl; + std::cout << "Throughput: " << mb_per_sec << " MB/sec" << std::endl; + + // Hash quality verification (basic collision test) + std::cout << "\n--- Hash Quality Verification ---" << std::endl; + verify_hash_quality(); + } + + void verify_hash_quality() { + std::unordered_map hash_counts; + int collisions = 0; + + for (const auto& str : test_data) { + unsigned hash_val = string_hash(str.c_str(), str.length(), 0); + hash_counts[hash_val]++; + if (hash_counts[hash_val] == 2) { + collisions++; + } + } + + double collision_rate = (100.0 * collisions) / test_data.size(); + std::cout << "Total strings: " << test_data.size() << std::endl; + std::cout << "Unique hashes: " << hash_counts.size() << std::endl; + std::cout << "Collisions: " << collisions << " (" << collision_rate << "%)" << std::endl; + + if (collision_rate < 5.0) { + std::cout << "✓ Hash quality: Good (< 5% collision rate)" << std::endl; + } else { + std::cout << "⚠ Hash quality: Needs attention (>= 5% collision rate)" << std::endl; + } + } +}; + +// Build configuration info +void print_build_info() { + std::cout << "=== Z3 Hash Function Build Configuration ===" << std::endl; + +#ifdef Z3_USE_XXHASH + #if Z3_USE_XXHASH + std::cout << "xxHash optimization: ENABLED" << std::endl; + #else + std::cout << "xxHash optimization: DISABLED" << std::endl; + #endif +#else + std::cout << "xxHash optimization: NOT DEFINED (using default)" << std::endl; +#endif + + std::cout << "Compiler optimizations: " << +#ifdef NDEBUG + "ENABLED (-DNDEBUG)" +#else + "DISABLED" +#endif + << std::endl; +} + +int main() { + print_build_info(); + + Z3HashPerformanceTest test; + test.run_comprehensive_performance_test(); + + return 0; +} \ No newline at end of file diff --git a/xxhash_z3_performance_test_orig b/xxhash_z3_performance_test_orig new file mode 100755 index 000000000..84a1e111e Binary files /dev/null and b/xxhash_z3_performance_test_orig differ