diff --git a/build-steps.log b/build-steps.log deleted file mode 100644 index 80b413183..000000000 --- a/build-steps.log +++ /dev/null @@ -1,478 +0,0 @@ -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/xxhash_benchmark b/xxhash_benchmark deleted file mode 100755 index 2ffee767f..000000000 Binary files a/xxhash_benchmark and /dev/null differ diff --git a/xxhash_benchmark.cpp b/xxhash_benchmark.cpp deleted file mode 100644 index eaaf675d1..000000000 --- a/xxhash_benchmark.cpp +++ /dev/null @@ -1,216 +0,0 @@ -#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 deleted file mode 100755 index d754272b1..000000000 Binary files a/xxhash_extended_benchmark and /dev/null differ diff --git a/xxhash_extended_benchmark.cpp b/xxhash_extended_benchmark.cpp index 593f3ff65..2a7e27d0c 100644 --- a/xxhash_extended_benchmark.cpp +++ b/xxhash_extended_benchmark.cpp @@ -197,7 +197,7 @@ std::vector generate_test_data() { template double benchmark_hash(const std::vector& data, HashFunc hash_func, const std::string& name) { - const int iterations = 100; + const int iterations = 10000; auto start = std::chrono::high_resolution_clock::now(); volatile unsigned result = 0; diff --git a/xxhash_z3_performance_test b/xxhash_z3_performance_test deleted file mode 100755 index c3573475e..000000000 Binary files a/xxhash_z3_performance_test and /dev/null differ diff --git a/xxhash_z3_performance_test.cpp b/xxhash_z3_performance_test.cpp deleted file mode 100644 index c352edf3c..000000000 --- a/xxhash_z3_performance_test.cpp +++ /dev/null @@ -1,172 +0,0 @@ -#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 deleted file mode 100755 index 84a1e111e..000000000 Binary files a/xxhash_z3_performance_test_orig and /dev/null differ