mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
Merge 7c51accb30 into 38a346fa1b
This commit is contained in:
Don Syme
GitHub
commit
bfa580ddbe
3 changed files with 737 additions and 4 deletions
635
build-steps.log
Normal file
635
build-steps.log
Normal file
|
|
@ -0,0 +1,635 @@
|
|||
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: $<$<CONFIG:Debug>:Z3DEBUG>;$<$<CONFIG:Release>:_EXTERNAL_RELEASE>;$<$<CONFIG:RelWithDebInfo>:_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<SYNCH>::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<SYNCH>::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
|
||||
[206/881] Building CXX object src/ast/macros/CMakeFiles/macros.dir/macro_util.cpp.o
|
||||
[207/881] Building CXX object src/ast/macros/CMakeFiles/macros.dir/macro_manager.cpp.o
|
||||
[208/881] Building CXX object src/ast/macros/CMakeFiles/macros.dir/quasi_macros.cpp.o
|
||||
[209/881] Building CXX object src/ast/rewriter/CMakeFiles/rewriter.dir/seq_rewriter.cpp.o
|
||||
[210/881] Building CXX object src/ast/rewriter/bit_blaster/CMakeFiles/bit_blaster.dir/bit_blaster.cpp.o
|
||||
[211/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_arith_plugin.cpp.o
|
||||
/home/runner/work/z3/z3/src/ast/euf/euf_arith_plugin.cpp: In member function ‘virtual void euf::arith_plugin::register_node(euf::enode*)’:
|
||||
/home/runner/work/z3/z3/src/ast/euf/euf_arith_plugin.cpp:62:19: warning: unused variable ‘m’ [-Wunused-variable]
|
||||
62 | auto& m = g.get_manager();
|
||||
| ^
|
||||
[212/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_enode.cpp.o
|
||||
[213/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_bv_plugin.cpp.o
|
||||
[214/881] Building CXX object src/ast/rewriter/bit_blaster/CMakeFiles/bit_blaster.dir/bit_blaster_rewriter.cpp.o
|
||||
[215/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_ac_plugin.cpp.o
|
||||
/home/runner/work/z3/z3/src/ast/euf/euf_ac_plugin.cpp: In member function ‘void euf::ac_plugin::rewrite1(const ref_counts&, const monomial_t&, ref_counts&, ptr_vector<node>&)’:
|
||||
/home/runner/work/z3/z3/src/ast/euf/euf_ac_plugin.cpp:1060:14: warning: unused variable ‘change’ [-Wunused-variable]
|
||||
1060 | bool change = false;
|
||||
| ^~~~~~
|
||||
[216/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_justification.cpp.o
|
||||
[217/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_egraph.cpp.o
|
||||
[218/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_etable.cpp.o
|
||||
[219/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_plugin.cpp.o
|
||||
[220/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_specrel_plugin.cpp.o
|
||||
[221/881] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/matcher.cpp.o
|
||||
[222/881] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/substitution.cpp.o
|
||||
[222/881] Generating "/home/runner/work/z3/z3/build/src/parsers/util/parser_params.hpp" from "parser_params.pyg"
|
||||
INFO:root:Using /home/runner/work/z3/z3/src/parsers/util/parser_params.pyg
|
||||
INFO:root:Generated "/home/runner/work/z3/z3/build/src/parsers/util/parser_params.hpp"
|
||||
[223/881] Generating "/home/runner/work/z3/z3/build/src/ast/normal_forms/nnf_params.hpp" from "nnf_params.pyg"
|
||||
INFO:root:Using /home/runner/work/z3/z3/src/ast/normal_forms/nnf_params.pyg
|
||||
INFO:root:Generated "/home/runner/work/z3/z3/build/src/ast/normal_forms/nnf_params.hpp"
|
||||
[224/881] Generating "/home/runner/work/z3/z3/build/src/model/model_evaluator_params.hpp" from "model_evaluator_params.pyg"
|
||||
INFO:root:Using /home/runner/work/z3/z3/src/model/model_evaluator_params.pyg
|
||||
INFO:root:Generated "/home/runner/work/z3/z3/build/src/model/model_evaluator_params.hpp"
|
||||
[225/881] Generating "/home/runner/work/z3/z3/build/src/model/model_params.hpp" from "model_params.pyg"
|
||||
INFO:root:Using /home/runner/work/z3/z3/src/model/model_params.pyg
|
||||
INFO:root:Generated "/home/runner/work/z3/z3/build/src/model/model_params.hpp"
|
||||
[226/881] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/unifier.cpp.o
|
||||
[227/881] Generating "/home/runner/work/z3/z3/build/src/sat/sat_asymm_branch_params.hpp" from "sat_asymm_branch_params.pyg"
|
||||
INFO:root:Using /home/runner/work/z3/z3/src/sat/sat_asymm_branch_params.pyg
|
||||
INFO:root:Generated "/home/runner/work/z3/z3/build/src/sat/sat_asymm_branch_params.hpp"
|
||||
[228/881] Generating "/home/runner/work/z3/z3/build/src/sat/sat_scc_params.hpp" from "sat_scc_params.pyg"
|
||||
INFO:root:Using /home/runner/work/z3/z3/src/sat/sat_scc_params.pyg
|
||||
INFO:root:Generated "/home/runner/work/z3/z3/build/src/sat/sat_scc_params.hpp"
|
||||
[229/881] Generating "/home/runner/work/z3/z3/build/src/sat/sat_simplifier_params.hpp" from "sat_simplifier_params.pyg"
|
||||
INFO:root:Using /home/runner/work/z3/z3/src/sat/sat_simplifier_params.pyg
|
||||
INFO:root:Generated "/home/runner/work/z3/z3/build/src/sat/sat_simplifier_params.hpp"
|
||||
[231/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/ho_matcher.cpp.o
|
||||
/home/runner/work/z3/z3/src/ast/euf/ho_matcher.cpp: In member function ‘bool euf::ho_matcher::consume_work(euf::match_goal&)’:
|
||||
/home/runner/work/z3/z3/src/ast/euf/ho_matcher.cpp:296:18: warning: unused variable ‘idx’ [-Wunused-variable]
|
||||
296 | auto idx = v->get_idx() - wi.pat_offset();
|
||||
| ^~~
|
||||
[232/881] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/substitution_tree.cpp.o
|
||||
[233/881] Building CXX object src/ast/substitution/CMakeFiles/substitution.dir/demodulator_rewriter.cpp.o
|
||||
[234/881] Building CXX object src/ast/euf/CMakeFiles/euf.dir/euf_mam.cpp.o
|
||||
[235/881] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/defined_names.cpp.o
|
||||
[236/881] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/name_exprs.cpp.o
|
||||
[237/881] Building CXX object src/model/CMakeFiles/model.dir/array_factory.cpp.o
|
||||
[238/881] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/nnf.cpp.o
|
||||
[239/881] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/elim_term_ite.cpp.o
|
||||
[240/881] Building CXX object src/model/CMakeFiles/model.dir/datatype_factory.cpp.o
|
||||
[241/881] Building CXX object src/ast/normal_forms/CMakeFiles/normal_forms.dir/pull_quant.cpp.o
|
||||
[242/881] Building CXX object src/model/CMakeFiles/model.dir/model_core.cpp.o
|
||||
[243/881] Building CXX object src/model/CMakeFiles/model.dir/model2expr.cpp.o
|
||||
[244/881] Building CXX object src/model/CMakeFiles/model.dir/func_interp.cpp.o
|
||||
[245/881] Building CXX object src/model/CMakeFiles/model.dir/model_pp.cpp.o
|
||||
[246/881] Building CXX object src/model/CMakeFiles/model.dir/model.cpp.o
|
||||
[247/881] Building CXX object src/model/CMakeFiles/model.dir/model_smt2_pp.cpp.o
|
||||
[248/881] Building CXX object src/model/CMakeFiles/model.dir/model_v2_pp.cpp.o
|
||||
[249/881] Building CXX object src/model/CMakeFiles/model.dir/model_macro_solver.cpp.o
|
||||
[250/881] Building CXX object src/model/CMakeFiles/model.dir/model_implicant.cpp.o
|
||||
[251/881] Building CXX object src/model/CMakeFiles/model.dir/struct_factory.cpp.o
|
||||
[252/881] Building CXX object src/model/CMakeFiles/model.dir/numeral_factory.cpp.o
|
||||
[253/881] Building CXX object src/model/CMakeFiles/model.dir/model_evaluator.cpp.o
|
||||
[254/881] Building CXX object src/model/CMakeFiles/model.dir/value_factory.cpp.o
|
||||
[255/881] Building CXX object src/ast/converters/CMakeFiles/converters.dir/equiv_proof_converter.cpp.o
|
||||
[256/881] Building CXX object src/ast/converters/CMakeFiles/converters.dir/expr_inverter.cpp.o
|
||||
[257/881] Building CXX object src/ast/converters/CMakeFiles/converters.dir/model_converter.cpp.o
|
||||
[258/881] Building CXX object src/ast/converters/CMakeFiles/converters.dir/proof_converter.cpp.o
|
||||
[259/881] Building CXX object src/ast/converters/CMakeFiles/converters.dir/generic_model_converter.cpp.o
|
||||
[260/881] Building CXX object src/ast/converters/CMakeFiles/converters.dir/horn_subsume_model_converter.cpp.o
|
||||
[261/881] Building CXX object src/ast/converters/CMakeFiles/converters.dir/replace_proof_converter.cpp.o
|
||||
[262/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/bit_blaster.cpp.o
|
||||
[263/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/bound_manager.cpp.o
|
||||
[264/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/bound_propagator.cpp.o
|
||||
[265/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/bv_slice.cpp.o
|
||||
[266/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/bv_bounds_simplifier.cpp.o
|
||||
[267/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/card2bv.cpp.o
|
||||
[268/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/dependent_expr_state.cpp.o
|
||||
[269/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/bound_simplifier.cpp.o
|
||||
[270/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/demodulator_simplifier.cpp.o
|
||||
[271/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/dominator_simplifier.cpp.o
|
||||
[272/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/elim_unconstrained.cpp.o
|
||||
[273/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/distribute_forall.cpp.o
|
||||
[274/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/linear_equation.cpp.o
|
||||
[275/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/extract_eqs.cpp.o
|
||||
[276/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/eliminate_predicates.cpp.o
|
||||
[277/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/propagate_values.cpp.o
|
||||
[278/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/euf_completion.cpp.o
|
||||
/home/runner/work/z3/z3/src/ast/simplifiers/euf_completion.cpp: In member function ‘expr_ref euf::completion::get_canonical(quantifier*, proof_ref&, expr_dependency_ref&)’:
|
||||
/home/runner/work/z3/z3/src/ast/simplifiers/euf_completion.cpp:1091:14: warning: unused variable ‘n’ [-Wunused-variable]
|
||||
1091 | auto n = m_egraph.find(q);
|
||||
| ^
|
||||
[279/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/model_reconstruction_trail.cpp.o
|
||||
[280/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/max_bv_sharing.cpp.o
|
||||
[281/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/dependency_converter.cpp.o
|
||||
[282/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/solve_context_eqs.cpp.o
|
||||
[283/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal_num_occurs.cpp.o
|
||||
[284/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/solve_eqs.cpp.o
|
||||
[285/881] Building CXX object src/ast/simplifiers/CMakeFiles/simplifiers.dir/reduce_args_simplifier.cpp.o
|
||||
[286/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal.cpp.o
|
||||
[287/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal_shared_occs.cpp.o
|
||||
[288/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/goal_util.cpp.o
|
||||
[289/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/probe.cpp.o
|
||||
[290/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/tactic.cpp.o
|
||||
[291/881] Building CXX object src/tactic/CMakeFiles/tactic.dir/tactical.cpp.o
|
||||
[292/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_arrays_tg.cpp.o
|
||||
[293/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_basic_tg.cpp.o
|
||||
[294/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_datatypes.cpp.o
|
||||
[295/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_arith.cpp.o
|
||||
[296/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_dt_tg.cpp.o
|
||||
[297/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_arrays.cpp.o
|
||||
[298/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_euf.cpp.o
|
||||
[299/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_qel_util.cpp.o
|
||||
[300/881] Building CXX object src/qe/mbp/CMakeFiles/mbp.dir/mbp_qel.cpp.o
|
||||
69
hashtable_perf_test.cpp
Normal file
69
hashtable_perf_test.cpp
Normal file
|
|
@ -0,0 +1,69 @@
|
|||
#include "src/util/hashtable.h"
|
||||
#include "src/util/hash.h"
|
||||
#include <iostream>
|
||||
#include <chrono>
|
||||
#include <vector>
|
||||
#include <random>
|
||||
|
||||
struct int_hash {
|
||||
unsigned operator()(int k) const { return static_cast<unsigned>(k) * 2654435761U; }
|
||||
};
|
||||
|
||||
struct int_eq {
|
||||
bool operator()(int a, int b) const { return a == b; }
|
||||
};
|
||||
|
||||
typedef hashtable<int, int_hash, int_eq> 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<int> 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<std::chrono::microseconds>(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<std::chrono::microseconds>(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;
|
||||
}
|
||||
|
|
@ -26,10 +26,21 @@ Revision History:
|
|||
#include "util/memory_manager.h"
|
||||
#include "util/hash.h"
|
||||
#include "util/vector.h"
|
||||
#if __has_builtin(__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,10 +54,11 @@ typedef enum { HT_FREE,
|
|||
HT_USED } hash_entry_state;
|
||||
|
||||
template<typename T>
|
||||
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; }
|
||||
|
|
@ -134,6 +146,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 +402,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 +457,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 +525,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 +690,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() { \
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue