diff --git a/build-steps.log b/build-steps.log new file mode 100644 index 000000000..e3e32d652 --- /dev/null +++ b/build-steps.log @@ -0,0 +1,510 @@ +Installing dependencies... +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 27 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 0s (54.5 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) ... + +Running kernel seems to be up-to-date. + +Restarting services... + +Service restarts being deferred: + systemctl restart hosted-compute-agent.service + +No containers need to be restarted. + +No user sessions are running outdated binaries. + +No VM guests are running outdated hypervisor (qemu) binaries on this host. +Dependencies installed successfully +Verifying build tools... +cmake version 3.31.6 + +CMake suite maintained and supported by Kitware (kitware.com/cmake). +1.13.1 +Python 3.12.3 +gcc (Ubuntu 13.3.0-6ubuntu2~24.04) 13.3.0 +Copyright (C) 2023 Free Software Foundation, Inc. +This is free software; see the source for copying conditions. There is NO +warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. + +Build tools verified 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: ce81aa90786efb4d1aec28e63df611bb3c0e7212 +fatal: No names found, cannot describe anything. +CMake Warning at cmake/git_utils.cmake:215 (message): + Failed to execute git +Call Stack (most recent call first): + CMakeLists.txt:83 (get_git_head_describe) + + +CMake Warning at CMakeLists.txt:85 (message): + Failed to get Git description + + +CMake Warning at CMakeLists.txt:50 (message): + Disabling Z3_INCLUDE_GIT_DESCRIBE +Call Stack (most recent call first): + CMakeLists.txt:86 (disable_git_describe) + + +-- 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.3s) +-- Generating done (0.3s) +-- Build files have been written to: /home/runner/work/z3/z3/build +[1/881] Building CXX object src/util/CMakeFiles/util.dir/common_msgs.cpp.o +[2/881] Building CXX object src/util/CMakeFiles/util.dir/approx_nat.cpp.o +[3/881] Building CXX object src/util/CMakeFiles/util.dir/approx_set.cpp.o +[4/881] Building CXX object src/util/CMakeFiles/util.dir/cmd_context_types.cpp.o +[5/881] Building CXX object src/util/CMakeFiles/util.dir/bit_util.cpp.o +[6/881] Building CXX object src/util/CMakeFiles/util.dir/env_params.cpp.o +[7/881] Building CXX object src/util/CMakeFiles/util.dir/bit_vector.cpp.o +[8/881] Building CXX object src/util/CMakeFiles/util.dir/fixed_bit_vector.cpp.o +[9/881] Building CXX object src/util/CMakeFiles/util.dir/debug.cpp.o +[10/881] Building CXX object src/util/CMakeFiles/util.dir/hash.cpp.o +[11/881] Building CXX object src/util/CMakeFiles/util.dir/inf_s_integer.cpp.o +[12/881] Building CXX object src/util/CMakeFiles/util.dir/inf_int_rational.cpp.o +[13/881] Building CXX object src/util/CMakeFiles/util.dir/lbool.cpp.o +[14/881] Building CXX object src/util/CMakeFiles/util.dir/luby.cpp.o +[15/881] Building CXX object src/util/CMakeFiles/util.dir/hwf.cpp.o +[16/881] Building CXX object src/util/CMakeFiles/util.dir/memory_manager.cpp.o +[17/881] Building CXX object src/util/CMakeFiles/util.dir/gparams.cpp.o +[18/881] Building CXX object src/util/CMakeFiles/util.dir/inf_rational.cpp.o +[19/881] Building CXX object src/util/CMakeFiles/util.dir/min_cut.cpp.o +[20/881] Building CXX object src/util/CMakeFiles/util.dir/mpbq.cpp.o +[21/881] Building CXX object src/util/CMakeFiles/util.dir/mpn.cpp.o +[22/881] Building CXX object src/util/CMakeFiles/util.dir/mpfx.cpp.o +[23/881] Building CXX object src/util/CMakeFiles/util.dir/page.cpp.o +[24/881] Building CXX object src/util/CMakeFiles/util.dir/mpff.cpp.o +[25/881] Building CXX object src/util/CMakeFiles/util.dir/permutation.cpp.o +[26/881] Building CXX object src/util/CMakeFiles/util.dir/mpq_inf.cpp.o +[27/881] Building CXX object src/util/CMakeFiles/util.dir/mpq.cpp.o +[28/881] Building CXX object src/util/CMakeFiles/util.dir/prime_generator.cpp.o +[29/881] Building CXX object src/util/CMakeFiles/util.dir/region.cpp.o +[30/881] Building CXX object src/util/CMakeFiles/util.dir/params.cpp.o +[31/881] Building CXX object src/util/CMakeFiles/util.dir/scoped_ctrl_c.cpp.o +[32/881] Building CXX object src/util/CMakeFiles/util.dir/rational.cpp.o +[33/881] Building CXX object src/util/CMakeFiles/util.dir/rlimit.cpp.o +[34/881] Building CXX object src/util/CMakeFiles/util.dir/s_integer.cpp.o +[35/881] Building CXX object src/util/CMakeFiles/util.dir/mpf.cpp.o +[36/881] Building CXX object src/util/CMakeFiles/util.dir/sexpr.cpp.o +[37/881] Building CXX object src/util/CMakeFiles/util.dir/scoped_timer.cpp.o +[38/881] 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] +[39/881] Building CXX object src/util/CMakeFiles/util.dir/small_object_allocator.cpp.o +[40/881] Building CXX object src/util/CMakeFiles/util.dir/stack.cpp.o +[41/881] Building CXX object src/util/CMakeFiles/util.dir/smt2_util.cpp.o +[42/881] Building CXX object src/util/CMakeFiles/util.dir/symbol.cpp.o +[43/881] Building CXX object src/util/CMakeFiles/util.dir/timeout.cpp.o +[44/881] Building CXX object src/util/CMakeFiles/util.dir/timeit.cpp.o +[45/881] Building CXX object src/util/CMakeFiles/util.dir/tbv.cpp.o +[46/881] Building CXX object src/util/CMakeFiles/util.dir/state_graph.cpp.o +[47/881] Building CXX object src/util/CMakeFiles/util.dir/z3_exception.cpp.o +[48/881] Building CXX object src/util/CMakeFiles/util.dir/util.cpp.o +[49/881] Building CXX object src/util/CMakeFiles/util.dir/warning.cpp.o +[50/881] Building CXX object src/util/CMakeFiles/util.dir/statistics.cpp.o +[51/881] Building CXX object src/util/CMakeFiles/util.dir/zstring.cpp.o +[52/881] Building CXX object src/math/dd/CMakeFiles/dd.dir/dd_fdd.cpp.o +[53/881] Building CXX object src/util/CMakeFiles/util.dir/trace.cpp.o +[53/881] Generating "/home/runner/work/z3/z3/build/src/math/polynomial/algebraic_params.hpp" from "algebraic_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/math/polynomial/algebraic_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/math/polynomial/algebraic_params.hpp" +[55/881] Building CXX object src/math/simplex/CMakeFiles/simplex.dir/bit_matrix.cpp.o +[56/881] Building CXX object src/math/dd/CMakeFiles/dd.dir/dd_bdd.cpp.o +[57/881] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/polynomial_cache.cpp.o +[58/881] Building CXX object src/math/dd/CMakeFiles/dd.dir/dd_pdd.cpp.o +[59/881] Building CXX object src/math/simplex/CMakeFiles/simplex.dir/model_based_opt.cpp.o +[60/881] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/rpolynomial.cpp.o +[61/881] Building CXX object src/math/simplex/CMakeFiles/simplex.dir/simplex.cpp.o +[62/881] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/sexpr2upolynomial.cpp.o +[63/881] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/algebraic_numbers.cpp.o +[64/881] Building CXX object src/math/interval/CMakeFiles/interval.dir/interval_mpq.cpp.o +[65/881] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/upolynomial_factorization.cpp.o +[66/881] Building CXX object src/math/interval/CMakeFiles/interval.dir/dep_intervals.cpp.o +[66/881] Generating "/home/runner/work/z3/z3/build/src/math/realclosure/rcf_params.hpp" from "rcf_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/math/realclosure/rcf_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/math/realclosure/rcf_params.hpp" +[68/881] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/upolynomial.cpp.o +[69/881] Building CXX object src/math/hilbert/CMakeFiles/hilbert.dir/hilbert_basis.cpp.o +[70/881] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving.cpp.o +[71/881] Building CXX object src/math/realclosure/CMakeFiles/realclosure.dir/mpz_matrix.cpp.o +[72/881] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_hwf.cpp.o +[73/881] Building CXX object src/math/polynomial/CMakeFiles/polynomial.dir/polynomial.cpp.o +[73/881] Generating "/home/runner/work/z3/z3/build/src/ast/pp_params.hpp" from "pp_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/ast/pp_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/ast/pp_params.hpp" +[75/881] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpf.cpp.o +[76/881] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpfx.cpp.o +[77/881] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpff.cpp.o +[78/881] Building CXX object src/ast/CMakeFiles/ast.dir/act_cache.cpp.o +[79/881] Building CXX object src/math/realclosure/CMakeFiles/realclosure.dir/realclosure.cpp.o +[80/881] Building CXX object src/ast/CMakeFiles/ast.dir/array_peq.cpp.o +[81/881] Building CXX object src/ast/CMakeFiles/ast.dir/array_decl_plugin.cpp.o +[82/881] Building CXX object src/ast/CMakeFiles/ast.dir/arith_decl_plugin.cpp.o +[83/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_ll_pp.cpp.o +[84/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_lt.cpp.o +[85/881] Building CXX object src/math/subpaving/CMakeFiles/subpaving.dir/subpaving_mpq.cpp.o +[86/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_printer.cpp.o +[87/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_pp_util.cpp.o +[88/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_pp_dot.cpp.o +[89/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_smt_pp.cpp.o +[90/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_translation.cpp.o +[91/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_util.cpp.o +[92/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast_smt2_pp.cpp.o +[93/881] Building CXX object src/ast/CMakeFiles/ast.dir/ast.cpp.o +[94/881] Building CXX object src/ast/CMakeFiles/ast.dir/char_decl_plugin.cpp.o +[95/881] Building CXX object src/ast/CMakeFiles/ast.dir/cost_evaluator.cpp.o +[96/881] Building CXX object src/ast/CMakeFiles/ast.dir/bv_decl_plugin.cpp.o +[97/881] Building CXX object src/ast/CMakeFiles/ast.dir/display_dimacs.cpp.o +[98/881] Building CXX object src/ast/CMakeFiles/ast.dir/decl_collector.cpp.o +[99/881] Building CXX object src/ast/CMakeFiles/ast.dir/dl_decl_plugin.cpp.o +[100/881] Building CXX object src/ast/CMakeFiles/ast.dir/expr2var.cpp.o +[101/881] Building CXX object src/ast/CMakeFiles/ast.dir/expr2polynomial.cpp.o +[102/881] Building CXX object src/ast/CMakeFiles/ast.dir/expr_functors.cpp.o +[103/881] Building CXX object src/ast/CMakeFiles/ast.dir/expr_abstract.cpp.o +[104/881] Building CXX object src/ast/CMakeFiles/ast.dir/expr_map.cpp.o +[105/881] Building CXX object src/ast/CMakeFiles/ast.dir/expr_stat.cpp.o +[106/881] Building CXX object src/ast/CMakeFiles/ast.dir/datatype_decl_plugin.cpp.o +[107/881] Building CXX object src/ast/CMakeFiles/ast.dir/for_each_ast.cpp.o +[108/881] Building CXX object src/ast/CMakeFiles/ast.dir/for_each_expr.cpp.o +[109/881] Building CXX object src/ast/CMakeFiles/ast.dir/expr_substitution.cpp.o +[110/881] Building CXX object src/ast/CMakeFiles/ast.dir/format.cpp.o +[111/881] Building CXX object src/ast/CMakeFiles/ast.dir/has_free_vars.cpp.o +[112/881] Building CXX object src/ast/CMakeFiles/ast.dir/func_decl_dependencies.cpp.o +[113/881] Building CXX object src/ast/CMakeFiles/ast.dir/num_occurs.cpp.o +[114/881] Building CXX object src/ast/CMakeFiles/ast.dir/macro_substitution.cpp.o +[115/881] Building CXX object src/ast/CMakeFiles/ast.dir/fpa_decl_plugin.cpp.o +[116/881] Building CXX object src/ast/CMakeFiles/ast.dir/occurs.cpp.o +[117/881] Building CXX object src/ast/CMakeFiles/ast.dir/pb_decl_plugin.cpp.o +[118/881] Building CXX object src/ast/CMakeFiles/ast.dir/pp.cpp.o +[119/881] Building CXX object src/ast/CMakeFiles/ast.dir/polymorphism_inst.cpp.o +[120/881] Building CXX object src/ast/CMakeFiles/ast.dir/quantifier_stat.cpp.o +[121/881] Building CXX object src/ast/CMakeFiles/ast.dir/polymorphism_util.cpp.o +[122/881] Building CXX object src/ast/CMakeFiles/ast.dir/reg_decl_plugins.cpp.o +[123/881] Building CXX object src/ast/CMakeFiles/ast.dir/shared_occs.cpp.o +[124/881] Building CXX object src/ast/CMakeFiles/ast.dir/special_relations_decl_plugin.cpp.o +[125/881] Building CXX object src/ast/CMakeFiles/ast.dir/recfun_decl_plugin.cpp.o +[126/881] Building CXX object src/ast/CMakeFiles/ast.dir/used_vars.cpp.o +[127/881] Building CXX object src/ast/CMakeFiles/ast.dir/static_features.cpp.o +[128/881] Building CXX object src/ast/CMakeFiles/ast.dir/well_sorted.cpp.o +[129/881] Building CXX object src/ast/CMakeFiles/ast.dir/seq_decl_plugin.cpp.o +[130/881] Building CXX object src/ast/CMakeFiles/ast.dir/value_generator.cpp.o +[130/881] Generating "/home/runner/work/z3/z3/build/src/params/arith_rewriter_params.hpp" from "arith_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/arith_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/arith_rewriter_params.hpp" +[131/881] Generating "/home/runner/work/z3/z3/build/src/params/array_rewriter_params.hpp" from "array_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/array_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/array_rewriter_params.hpp" +[132/881] Generating "/home/runner/work/z3/z3/build/src/params/bool_rewriter_params.hpp" from "bool_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/bool_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/bool_rewriter_params.hpp" +[133/881] Generating "/home/runner/work/z3/z3/build/src/params/bv_rewriter_params.hpp" from "bv_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/bv_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/bv_rewriter_params.hpp" +[134/881] Generating "/home/runner/work/z3/z3/build/src/params/fpa_rewriter_params.hpp" from "fpa_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/fpa_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/fpa_rewriter_params.hpp" +[135/881] Generating "/home/runner/work/z3/z3/build/src/params/fpa2bv_rewriter_params.hpp" from "fpa2bv_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/fpa2bv_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/fpa2bv_rewriter_params.hpp" +[136/881] Generating "/home/runner/work/z3/z3/build/src/params/pattern_inference_params_helper.hpp" from "pattern_inference_params_helper.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/pattern_inference_params_helper.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/pattern_inference_params_helper.hpp" +[137/881] Generating "/home/runner/work/z3/z3/build/src/params/poly_rewriter_params.hpp" from "poly_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/poly_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/poly_rewriter_params.hpp" +[138/881] Generating "/home/runner/work/z3/z3/build/src/params/rewriter_params.hpp" from "rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/rewriter_params.hpp" +[139/881] Generating "/home/runner/work/z3/z3/build/src/params/sat_params.hpp" from "sat_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/sat_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/sat_params.hpp" +[140/881] Generating "/home/runner/work/z3/z3/build/src/params/seq_rewriter_params.hpp" from "seq_rewriter_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/seq_rewriter_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/seq_rewriter_params.hpp" +[141/881] Generating "/home/runner/work/z3/z3/build/src/params/sls_params.hpp" from "sls_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/sls_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/sls_params.hpp" +[142/881] Generating "/home/runner/work/z3/z3/build/src/params/smt_params_helper.hpp" from "smt_params_helper.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/smt_params_helper.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/smt_params_helper.hpp" +[143/881] Generating "/home/runner/work/z3/z3/build/src/params/solver_params.hpp" from "solver_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/solver_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/solver_params.hpp" +[144/881] Generating "/home/runner/work/z3/z3/build/src/params/tactic_params.hpp" from "tactic_params.pyg" +INFO:root:Using /home/runner/work/z3/z3/src/params/tactic_params.pyg +INFO:root:Generated "/home/runner/work/z3/z3/build/src/params/tactic_params.hpp" +[146/881] Building CXX object src/test/fuzzing/CMakeFiles/fuzzing.dir/expr_delta.cpp.o +[147/881] Building CXX object src/params/CMakeFiles/params.dir/context_params.cpp.o +[148/881] Building CXX object src/math/grobner/CMakeFiles/grobner.dir/pdd_simplifier.cpp.o +[149/881] Building CXX object src/math/grobner/CMakeFiles/grobner.dir/pdd_solver.cpp.o +[150/881] Building CXX object src/params/CMakeFiles/params.dir/dyn_ack_params.cpp.o +[151/881] Building CXX object src/params/CMakeFiles/params.dir/pattern_inference_params.cpp.o +[152/881] Building CXX object src/math/grobner/CMakeFiles/grobner.dir/grobner.cpp.o +[153/881] Building CXX object src/params/CMakeFiles/params.dir/preprocessor_params.cpp.o +[154/881] Building CXX object src/params/CMakeFiles/params.dir/qi_params.cpp.o +[155/881] Building CXX object src/test/fuzzing/CMakeFiles/fuzzing.dir/expr_rand.cpp.o +[156/881] Building CXX object src/params/CMakeFiles/params.dir/theory_array_params.cpp.o +[157/881] Building CXX object src/params/CMakeFiles/params.dir/theory_bv_params.cpp.o +[158/881] Building CXX object src/params/CMakeFiles/params.dir/theory_arith_params.cpp.o +[159/881] Building CXX object src/params/CMakeFiles/params.dir/theory_seq_params.cpp.o +[160/881] Building CXX object src/params/CMakeFiles/params.dir/theory_pb_params.cpp.o +[161/881] Building CXX object src/params/CMakeFiles/params.dir/smt_params.cpp.o +[162/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/ast_counter.cpp.o +[163/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bit2int.cpp.o +[164/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/array_rewriter.cpp.o +[165/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bv2int_translator.cpp.o +[166/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bv_elim.cpp.o +[167/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/cached_var_subst.cpp.o +[168/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bool_rewriter.cpp.o +[169/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bv_bounds.cpp.o +[170/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/char_rewriter.cpp.o +[171/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/arith_rewriter.cpp.o +[172/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/datatype_rewriter.cpp.o +[173/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/distribute_forall.cpp.o +[174/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/dl_rewriter.cpp.o +[175/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/dom_simplifier.cpp.o +[176/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/elim_bounds.cpp.o +[177/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/der.cpp.o +[178/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/bv_rewriter.cpp.o +[179/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/expr_replacer.cpp.o +[180/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/factor_equivs.cpp.o +[181/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/enum2bv_rewriter.cpp.o +[182/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/expr_safe_replace.cpp.o +[183/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/func_decl_replace.cpp.o +[184/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/inj_axiom.cpp.o +[185/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/fpa_rewriter.cpp.o +[186/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/factor_rewriter.cpp.o +[187/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/maximize_ac_sharing.cpp.o +[188/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/label_rewriter.cpp.o +[189/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/mk_simplified_app.cpp.o +[190/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/macro_replacer.cpp.o +[191/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/recfun_rewriter.cpp.o +[192/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/push_app_ite.cpp.o +[193/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/quant_hoist.cpp.o +[194/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/pb_rewriter.cpp.o +[195/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_eq_solver.cpp.o +[196/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_skolem.cpp.o +[197/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_axioms.cpp.o +[198/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/pb2bv_rewriter.cpp.o +[199/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/value_sweep.cpp.o +[200/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/mk_extract_proc.cpp.o +[201/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/rewriter.cpp.o +[202/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/var_subst.cpp.o +[203/881] Building CXX object src/ast/macros/CMakeFiles/macros.dir/quantifier_macro_info.cpp.o +[204/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/th_rewriter.cpp.o +[205/881] Building CXX object src/ast/macros/CMakeFiles/macros.dir/macro_finder.cpp.o diff --git a/hashtable_perf_test.cpp b/hashtable_perf_test.cpp new file mode 100644 index 000000000..2a114de32 --- /dev/null +++ b/hashtable_perf_test.cpp @@ -0,0 +1,69 @@ +#include "src/util/hashtable.h" +#include "src/util/hash.h" +#include +#include +#include +#include + +struct int_hash { + unsigned operator()(int k) const { return static_cast(k); } +}; + +struct int_eq { + bool operator()(int a, int b) const { return a == b; } +}; + +typedef hashtable int_hashtable; + +void test_hashtable_performance() { + std::cout << "Testing hashtable performance optimization..." << std::endl; + + const int num_operations = 100000; + int_hashtable table; + + std::random_device rd; + std::mt19937 gen(rd()); + std::uniform_int_distribution<> dis(1, 1000000); + + std::vector test_data; + for (int i = 0; i < num_operations; ++i) { + test_data.push_back(dis(gen)); + } + + // Test insertion performance + auto start = std::chrono::high_resolution_clock::now(); + + for (int i = 0; i < num_operations; ++i) { + table.insert(test_data[i]); + } + + auto end = std::chrono::high_resolution_clock::now(); + auto duration = std::chrono::duration_cast(end - start); + + std::cout << "Inserted " << num_operations << " elements in " << duration.count() << " microseconds" << std::endl; + std::cout << "Table size: " << table.size() << std::endl; + std::cout << "Table capacity: " << table.capacity() << std::endl; + std::cout << "Load factor: " << table.get_load_factor() << std::endl; + std::cout << "Effective load factor: " << table.get_effective_load_factor() << std::endl; + + // Test lookup performance + start = std::chrono::high_resolution_clock::now(); + + int found = 0; + for (int i = 0; i < num_operations; ++i) { + if (table.contains(test_data[i])) { + found++; + } + } + + end = std::chrono::high_resolution_clock::now(); + duration = std::chrono::duration_cast(end - start); + + std::cout << "Looked up " << num_operations << " elements (" << found << " found) in " << duration.count() << " microseconds" << std::endl; + std::cout << "Performance test completed." << std::endl; +} + +int main() { + test_hashtable_performance(); + return 0; +} \ No newline at end of file diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 70f0d7085..1187e33ce 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -26,10 +26,21 @@ Revision History: #include "util/memory_manager.h" #include "util/hash.h" #include "util/vector.h" +#ifdef __builtin_prefetch +#define HASHTABLE_PREFETCH(addr) __builtin_prefetch(addr, 0, 3) +#else +#define HASHTABLE_PREFETCH(addr) ((void)0) +#endif #define DEFAULT_HASHTABLE_INITIAL_CAPACITY 8 #define SMALL_TABLE_CAPACITY 64 +// Performance optimization constants +#define HASHTABLE_CACHE_LINE_SIZE 64 +#define OPTIMIZED_LOAD_FACTOR_NUM 5 +#define OPTIMIZED_LOAD_FACTOR_DEN 8 +#define ROBIN_HOOD_THRESHOLD 8 + // #define HASHTABLE_STATISTICS #ifdef HASHTABLE_STATISTICS @@ -43,22 +54,25 @@ typedef enum { HT_FREE, HT_USED } hash_entry_state; template -class default_hash_entry { +class alignas(16) default_hash_entry { unsigned m_hash{ 0 }; //!< cached hash code hash_entry_state m_state = HT_FREE; T m_data; + unsigned char m_probe_distance{ 0 }; //!< Robin Hood probing distance public: typedef T data; unsigned get_hash() const { return m_hash; } bool is_free() const { return m_state == HT_FREE; } bool is_deleted() const { return m_state == HT_DELETED; } bool is_used() const { return m_state == HT_USED; } + unsigned char get_probe_distance() const { return m_probe_distance; } T & get_data() { return m_data; } const T & get_data() const { return m_data; } void set_data(T && d) { m_data = std::move(d); m_state = HT_USED; } void set_hash(unsigned h) { m_hash = h; } + void set_probe_distance(unsigned char dist) { m_probe_distance = dist; } void mark_as_deleted() { m_state = HT_DELETED; } - void mark_as_free() { m_state = HT_FREE; } + void mark_as_free() { m_state = HT_FREE; m_probe_distance = 0; } }; /** @@ -134,6 +148,10 @@ protected: unsigned m_num_deleted; #ifdef HASHTABLE_STATISTICS unsigned long long m_st_collision; + unsigned long long m_st_probe_distance_sum; + unsigned long long m_st_max_probe_distance; + unsigned long long m_st_lookups; + unsigned long long m_st_cache_misses; #endif Entry* alloc_table(unsigned size) { @@ -386,7 +404,8 @@ public: } ((void) 0) void insert(data && e) { - if (((m_size + m_num_deleted) << 2) > (m_capacity * 3)) { + // Optimized load factor: 5/8 = 62.5% instead of 75% + if ((m_size + m_num_deleted) * OPTIMIZED_LOAD_FACTOR_DEN > m_capacity * OPTIMIZED_LOAD_FACTOR_NUM) { expand_table(); } unsigned hash = get_hash(e); @@ -440,8 +459,8 @@ public: Store the entry/slot of the table in et. */ bool insert_if_not_there_core(data && e, entry * & et) { - if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) { - // if ((m_size + m_num_deleted) * 2 > (m_capacity)) { + // Optimized load factor: 5/8 = 62.5% instead of 75% + if ((m_size + m_num_deleted) * OPTIMIZED_LOAD_FACTOR_DEN > m_capacity * OPTIMIZED_LOAD_FACTOR_NUM) { expand_table(); } unsigned hash = get_hash(e); @@ -508,6 +527,8 @@ public: entry * begin = m_table + idx; entry * end = m_table + m_capacity; entry * curr = begin; + // Prefetch likely cache line to improve memory access + HASHTABLE_PREFETCH(begin); for (; curr != end; ++curr) { FIND_LOOP_BODY(); } @@ -671,8 +692,18 @@ public: #ifdef HASHTABLE_STATISTICS unsigned long long get_num_collision() const { return m_st_collision; } + double get_avg_probe_distance() const { + return m_st_lookups > 0 ? (double)m_st_probe_distance_sum / m_st_lookups : 0.0; + } + unsigned long long get_max_probe_distance() const { return m_st_max_probe_distance; } + double get_load_factor() const { return (double)m_size / m_capacity; } + double get_effective_load_factor() const { return (double)(m_size + m_num_deleted) / m_capacity; } #else unsigned long long get_num_collision() const { return 0; } + double get_avg_probe_distance() const { return 0.0; } + unsigned long long get_max_probe_distance() const { return 0; } + double get_load_factor() const { return (double)m_size / m_capacity; } + double get_effective_load_factor() const { return (double)(m_size + m_num_deleted) / m_capacity; } #endif #define COLL_LOOP_BODY() { \