From e2d725ee95a414b5e6302e4b226fd1cab37470a2 Mon Sep 17 00:00:00 2001 From: Don Syme Date: Thu, 18 Sep 2025 00:16:41 +0100 Subject: [PATCH] remove files, increase num iterations on benchmark --- build-steps.log | 478 -------------------------------- xxhash_benchmark | Bin 23176 -> 0 bytes xxhash_benchmark.cpp | 216 --------------- xxhash_extended_benchmark | Bin 44696 -> 0 bytes xxhash_extended_benchmark.cpp | 2 +- xxhash_z3_performance_test | Bin 58088 -> 0 bytes xxhash_z3_performance_test.cpp | 172 ------------ xxhash_z3_performance_test_orig | Bin 58088 -> 0 bytes 8 files changed, 1 insertion(+), 867 deletions(-) delete mode 100644 build-steps.log delete mode 100755 xxhash_benchmark delete mode 100644 xxhash_benchmark.cpp delete mode 100755 xxhash_extended_benchmark delete mode 100755 xxhash_z3_performance_test delete mode 100644 xxhash_z3_performance_test.cpp delete mode 100755 xxhash_z3_performance_test_orig diff --git a/build-steps.log b/build-steps.log deleted file mode 100644 index 80b413183..000000000 --- a/build-steps.log +++ /dev/null @@ -1,478 +0,0 @@ -Installing dependencies... -Get:1 file:/etc/apt/apt-mirrors.txt Mirrorlist [144 B] -Hit:2 http://azure.archive.ubuntu.com/ubuntu noble InRelease -Hit:6 https://packages.microsoft.com/repos/azure-cli noble InRelease -Get:7 https://packages.microsoft.com/ubuntu/24.04/prod noble InRelease [3600 B] -Get:3 http://azure.archive.ubuntu.com/ubuntu noble-updates InRelease [126 kB] -Get:4 http://azure.archive.ubuntu.com/ubuntu noble-backports InRelease [126 kB] -Get:5 http://azure.archive.ubuntu.com/ubuntu noble-security InRelease [126 kB] -Get:8 https://packages.microsoft.com/ubuntu/24.04/prod noble/main arm64 Packages [35.7 kB] -Get:9 https://packages.microsoft.com/ubuntu/24.04/prod noble/main amd64 Packages [53.2 kB] -Get:10 http://azure.archive.ubuntu.com/ubuntu noble-updates/main amd64 Packages [1411 kB] -Get:11 http://azure.archive.ubuntu.com/ubuntu noble-updates/main Translation-en [278 kB] -Get:12 http://azure.archive.ubuntu.com/ubuntu noble-updates/main amd64 Components [175 kB] -Get:13 http://azure.archive.ubuntu.com/ubuntu noble-updates/main amd64 c-n-f Metadata [15.2 kB] -Get:14 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe amd64 Packages [1483 kB] -Get:15 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe Translation-en [298 kB] -Get:16 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe amd64 Components [377 kB] -Get:17 http://azure.archive.ubuntu.com/ubuntu noble-updates/universe amd64 c-n-f Metadata [31.0 kB] -Get:18 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted amd64 Packages [1882 kB] -Get:19 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted Translation-en [422 kB] -Get:20 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted amd64 Components [212 B] -Get:21 http://azure.archive.ubuntu.com/ubuntu noble-updates/restricted amd64 c-n-f Metadata [500 B] -Get:22 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse amd64 Packages [41.9 kB] -Get:23 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse Translation-en [7064 B] -Get:24 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse amd64 Components [940 B] -Get:25 http://azure.archive.ubuntu.com/ubuntu noble-updates/multiverse amd64 c-n-f Metadata [644 B] -Get:26 http://azure.archive.ubuntu.com/ubuntu noble-backports/main amd64 Components [7068 B] -Get:27 http://azure.archive.ubuntu.com/ubuntu noble-backports/universe amd64 Components [19.2 kB] -Get:28 http://azure.archive.ubuntu.com/ubuntu noble-backports/restricted amd64 Components [216 B] -Get:29 http://azure.archive.ubuntu.com/ubuntu noble-backports/multiverse amd64 Components [212 B] -Get:30 http://azure.archive.ubuntu.com/ubuntu noble-security/main amd64 Packages [1119 kB] -Get:31 http://azure.archive.ubuntu.com/ubuntu noble-security/main Translation-en [192 kB] -Get:32 http://azure.archive.ubuntu.com/ubuntu noble-security/main amd64 Components [21.6 kB] -Get:33 http://azure.archive.ubuntu.com/ubuntu noble-security/main amd64 c-n-f Metadata [8748 B] -Get:34 http://azure.archive.ubuntu.com/ubuntu noble-security/universe amd64 Packages [880 kB] -Get:35 http://azure.archive.ubuntu.com/ubuntu noble-security/universe Translation-en [195 kB] -Get:36 http://azure.archive.ubuntu.com/ubuntu noble-security/universe amd64 Components [52.2 kB] -Get:37 http://azure.archive.ubuntu.com/ubuntu noble-security/universe amd64 c-n-f Metadata [18.0 kB] -Get:38 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted amd64 Packages [1756 kB] -Get:39 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted Translation-en [392 kB] -Get:40 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted amd64 Components [212 B] -Get:41 http://azure.archive.ubuntu.com/ubuntu noble-security/restricted amd64 c-n-f Metadata [468 B] -Get:42 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse amd64 Packages [37.4 kB] -Get:43 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse Translation-en [6020 B] -Get:44 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse amd64 Components [212 B] -Get:45 http://azure.archive.ubuntu.com/ubuntu noble-security/multiverse amd64 c-n-f Metadata [476 B] -Fetched 11.6 MB in 1s (7848 kB/s) -Reading package lists... -Reading package lists... -Building dependency tree... -Reading state information... -python3 is already the newest version (3.12.3-0ubuntu2). -python3-pip is already the newest version (24.0+dfsg-1ubuntu1.2). -git is already the newest version (1:2.51.0-0ppa2~ubuntu24.04.1). -git set to manually installed. -Suggested packages: - cmake-doc cmake-format elpa-cmake-mode -The following NEW packages will be installed: - build-essential cmake cmake-data libjsoncpp25 librhash0 ninja-build -0 upgraded, 6 newly installed, 0 to remove and 34 not upgraded. -Need to get 13.7 MB of archives. -After this operation, 49.5 MB of additional disk space will be used. -Get:1 file:/etc/apt/apt-mirrors.txt Mirrorlist [144 B] -Get:2 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 build-essential amd64 12.10ubuntu1 [4928 B] -Get:3 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 libjsoncpp25 amd64 1.9.5-6build1 [82.8 kB] -Get:4 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 librhash0 amd64 1.4.3-3build1 [129 kB] -Get:5 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 cmake-data all 3.28.3-1build7 [2155 kB] -Get:6 http://azure.archive.ubuntu.com/ubuntu noble/main amd64 cmake amd64 3.28.3-1build7 [11.2 MB] -Get:7 http://azure.archive.ubuntu.com/ubuntu noble/universe amd64 ninja-build amd64 1.11.1-2 [129 kB] -Fetched 13.7 MB in 1s (15.6 MB/s) -Selecting previously unselected package build-essential. -(Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 218657 files and directories currently installed.) -Preparing to unpack .../0-build-essential_12.10ubuntu1_amd64.deb ... -Unpacking build-essential (12.10ubuntu1) ... -Selecting previously unselected package libjsoncpp25:amd64. -Preparing to unpack .../1-libjsoncpp25_1.9.5-6build1_amd64.deb ... -Unpacking libjsoncpp25:amd64 (1.9.5-6build1) ... -Selecting previously unselected package librhash0:amd64. -Preparing to unpack .../2-librhash0_1.4.3-3build1_amd64.deb ... -Unpacking librhash0:amd64 (1.4.3-3build1) ... -Selecting previously unselected package cmake-data. -Preparing to unpack .../3-cmake-data_3.28.3-1build7_all.deb ... -Unpacking cmake-data (3.28.3-1build7) ... -Selecting previously unselected package cmake. -Preparing to unpack .../4-cmake_3.28.3-1build7_amd64.deb ... -Unpacking cmake (3.28.3-1build7) ... -Selecting previously unselected package ninja-build. -Preparing to unpack .../5-ninja-build_1.11.1-2_amd64.deb ... -Unpacking ninja-build (1.11.1-2) ... -Setting up ninja-build (1.11.1-2) ... -Setting up libjsoncpp25:amd64 (1.9.5-6build1) ... -Setting up librhash0:amd64 (1.4.3-3build1) ... -Setting up build-essential (12.10ubuntu1) ... -Setting up cmake-data (3.28.3-1build7) ... -Setting up cmake (3.28.3-1build7) ... -Processing triggers for man-db (2.12.0-4build2) ... -Processing triggers for libc-bin (2.39-0ubuntu8.5) ... -Dependencies installed successfully -Creating build directory... -Configuring CMake for performance development... --- The CXX compiler identification is GNU 13.3.0 --- Detecting CXX compiler ABI info --- Detecting CXX compiler ABI info - done --- Check for working CXX compiler: /usr/bin/c++ - skipped --- Detecting CXX compile features --- Detecting CXX compile features - done --- Z3 version 4.15.4.0 --- Found simple git working directory --- Found git directory "/home/runner/work/z3/z3/.git" --- Adding git dependency "/home/runner/work/z3/z3/.git/HEAD" --- Adding git dependency "/home/runner/work/z3/z3/.git/refs/heads/master" --- Found Git: /usr/bin/git (found version "2.51.0") --- Using Git hash in version output: 5b70f75d89d20e2ada9f319fb17ecfa920da115e --- Using Git description in version output: NOTFOUND --- CMake generator: Ninja --- Build type: RelWithDebInfo --- Found Python3: /usr/bin/python3.12 (found version "3.12.3") found components: Interpreter --- Python3_EXECUTABLE: /usr/bin/python3.12 --- Detected target architecture: x86_64 --- Not using libgmp --- Not using Z3_API_LOG_SYNC --- Thread-safe build --- Performing Test HAS_SSE2 --- Performing Test HAS_SSE2 - Success --- Performing Test CMAKE_HAVE_LIBC_PTHREAD --- Performing Test CMAKE_HAVE_LIBC_PTHREAD - Success --- Found Threads: TRUE --- Performing Test HAS__Wall --- Performing Test HAS__Wall - Success --- C++ compiler supports -Wall --- Treating only serious compiler warnings as errors --- Performing Test HAS__Werror_odr --- Performing Test HAS__Werror_odr - Success --- C++ compiler supports -Werror=odr --- Performing Test HAS__Werror_return_type --- Performing Test HAS__Werror_return_type - Success --- C++ compiler supports -Werror=return-type --- LTO disabled --- Performing Test BUILTIN_ATOMIC --- Performing Test BUILTIN_ATOMIC - Success --- CMAKE_CXX_FLAGS: "-fno-omit-frame-pointer -Werror=odr -Werror=return-type " --- CMAKE_EXE_LINKER_FLAGS: "" --- CMAKE_STATIC_LINKER_FLAGS: "" --- CMAKE_SHARED_LINKER_FLAGS: "" --- CMAKE_CXX_FLAGS_RELWITHDEBINFO: "-O2 -g -DNDEBUG" --- CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO: "" --- CMAKE_SHARED_LINKER_FLAGS_RELWITHDEBINFO: "" --- CMAKE_STATIC_LINKER_FLAGS_RELWITHDEBINFO: "" --- Z3_COMPONENT_CXX_DEFINES: $<$:Z3DEBUG>;$<$:_EXTERNAL_RELEASE>;$<$:_EXTERNAL_RELEASE>;-D_MP_INTERNAL;-D_TRACE --- Z3_COMPONENT_CXX_FLAGS: -mfpmath=sse;-msse;-msse2;-Wall --- Z3_DEPENDENT_LIBS: Threads::Threads --- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: /home/runner/work/z3/z3/build/src;/home/runner/work/z3/z3/src --- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: --- CMAKE_INSTALL_LIBDIR: "lib" --- CMAKE_INSTALL_BINDIR: "bin" --- CMAKE_INSTALL_INCLUDEDIR: "include" --- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig" --- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3" --- Adding component util --- Adding component polynomial --- Adding rule to generate "algebraic_params.hpp" --- Adding component dd --- Adding component hilbert --- Adding component simplex --- Adding component interval --- Adding component realclosure --- Adding rule to generate "rcf_params.hpp" --- Adding component subpaving --- Adding component ast --- Adding rule to generate "pp_params.hpp" --- Adding component params --- Adding rule to generate "arith_rewriter_params.hpp" --- Adding rule to generate "array_rewriter_params.hpp" --- Adding rule to generate "bool_rewriter_params.hpp" --- Adding rule to generate "bv_rewriter_params.hpp" --- Adding rule to generate "fpa_rewriter_params.hpp" --- Adding rule to generate "fpa2bv_rewriter_params.hpp" --- Adding rule to generate "pattern_inference_params_helper.hpp" --- Adding rule to generate "poly_rewriter_params.hpp" --- Adding rule to generate "rewriter_params.hpp" --- Adding rule to generate "sat_params.hpp" --- Adding rule to generate "seq_rewriter_params.hpp" --- Adding rule to generate "sls_params.hpp" --- Adding rule to generate "smt_params_helper.hpp" --- Adding rule to generate "solver_params.hpp" --- Adding rule to generate "tactic_params.hpp" --- Adding component rewriter --- Adding component bit_blaster --- Adding component normal_forms --- Adding rule to generate "nnf_params.hpp" --- Adding component macros --- Adding component model --- Adding rule to generate "model_evaluator_params.hpp" --- Adding rule to generate "model_params.hpp" --- Adding component euf --- Adding component converters --- Adding component substitution --- Adding component simplifiers --- Adding component tactic --- Adding component mbp --- Adding component qe_lite --- Adding component parser_util --- Adding rule to generate "parser_params.hpp" --- Adding component grobner --- Adding component sat --- Adding rule to generate "sat_asymm_branch_params.hpp" --- Adding rule to generate "sat_scc_params.hpp" --- Adding rule to generate "sat_simplifier_params.hpp" --- Adding component nlsat --- Adding rule to generate "nlsat_params.hpp" --- Adding component core_tactics --- Adding component subpaving_tactic --- Adding component aig_tactic --- Adding component arith_tactics --- Adding component solver --- Adding rule to generate "combined_solver_params.hpp" --- Adding rule to generate "parallel_params.hpp" --- Adding component cmd_context --- Adding component extra_cmds --- Adding component smt2parser --- Adding component solver_assertions --- Adding component pattern --- Adding component lp --- Adding rule to generate "lp_params_helper.hpp" --- Adding component ast_sls --- Adding component sat_smt --- Adding component sat_tactic --- Adding component nlsat_tactic --- Adding component ackermannization --- Adding rule to generate "ackermannization_params.hpp" --- Adding rule to generate "ackermannize_bv_tactic_params.hpp" --- Adding component proofs --- Adding component fpa --- Adding component proto_model --- Adding component smt --- Adding component bv_tactics --- Adding component smt_tactic --- Adding component sls_tactic --- Adding component qe --- Adding component muz --- Adding rule to generate "fp_params.hpp" --- Adding component dataflow --- Adding component transforms --- Adding component rel --- Adding component clp --- Adding component tab --- Adding component bmc --- Adding component ddnf --- Adding component spacer --- Adding component fp --- Adding component ufbv_tactic --- Adding component sat_solver --- Adding component smtlogic_tactics --- Adding rule to generate "qfufbv_tactic_params.hpp" --- Adding component fpa_tactics --- Adding component fd_solver --- Adding component portfolio --- Adding component opt --- Adding rule to generate "opt_params.hpp" --- Adding component api --- Adding component api_dll --- Adding component fuzzing --- Building documentation disabled --- Configuring done (3.7s) --- Generating done (0.3s) --- Build files have been written to: /home/runner/work/z3/z3/build -CMake configuration completed -[1/52] Building CXX object src/util/CMakeFiles/util.dir/common_msgs.cpp.o -[2/52] Building CXX object src/util/CMakeFiles/util.dir/approx_nat.cpp.o -[3/52] Building CXX object src/util/CMakeFiles/util.dir/approx_set.cpp.o -[4/52] Building CXX object src/util/CMakeFiles/util.dir/cmd_context_types.cpp.o -[5/52] Building CXX object src/util/CMakeFiles/util.dir/bit_util.cpp.o -[6/52] Building CXX object src/util/CMakeFiles/util.dir/env_params.cpp.o -[7/52] Building CXX object src/util/CMakeFiles/util.dir/fixed_bit_vector.cpp.o -[8/52] Building CXX object src/util/CMakeFiles/util.dir/debug.cpp.o -[9/52] Building CXX object src/util/CMakeFiles/util.dir/bit_vector.cpp.o -[10/52] Building CXX object src/util/CMakeFiles/util.dir/hash.cpp.o -[11/52] Building CXX object src/util/CMakeFiles/util.dir/inf_s_integer.cpp.o -[12/52] Building CXX object src/util/CMakeFiles/util.dir/inf_int_rational.cpp.o -[13/52] Building CXX object src/util/CMakeFiles/util.dir/luby.cpp.o -[14/52] Building CXX object src/util/CMakeFiles/util.dir/lbool.cpp.o -[15/52] Building CXX object src/util/CMakeFiles/util.dir/hwf.cpp.o -[16/52] Building CXX object src/util/CMakeFiles/util.dir/gparams.cpp.o -[17/52] Building CXX object src/util/CMakeFiles/util.dir/inf_rational.cpp.o -[18/52] Building CXX object src/util/CMakeFiles/util.dir/memory_manager.cpp.o -[19/52] Building CXX object src/util/CMakeFiles/util.dir/min_cut.cpp.o -[20/52] Building CXX object src/util/CMakeFiles/util.dir/mpbq.cpp.o -[21/52] Building CXX object src/util/CMakeFiles/util.dir/mpn.cpp.o -[22/52] Building CXX object src/util/CMakeFiles/util.dir/mpfx.cpp.o -[23/52] Building CXX object src/util/CMakeFiles/util.dir/page.cpp.o -[24/52] Building CXX object src/util/CMakeFiles/util.dir/mpff.cpp.o -[25/52] Building CXX object src/util/CMakeFiles/util.dir/permutation.cpp.o -[26/52] Building CXX object src/util/CMakeFiles/util.dir/mpq_inf.cpp.o -[27/52] Building CXX object src/util/CMakeFiles/util.dir/mpq.cpp.o -[28/52] Building CXX object src/util/CMakeFiles/util.dir/prime_generator.cpp.o -[29/52] Building CXX object src/util/CMakeFiles/util.dir/region.cpp.o -[30/52] Building CXX object src/util/CMakeFiles/util.dir/params.cpp.o -[31/52] Building CXX object src/util/CMakeFiles/util.dir/scoped_ctrl_c.cpp.o -[32/52] Building CXX object src/util/CMakeFiles/util.dir/rational.cpp.o -[33/52] Building CXX object src/util/CMakeFiles/util.dir/rlimit.cpp.o -[34/52] Building CXX object src/util/CMakeFiles/util.dir/s_integer.cpp.o -[35/52] Building CXX object src/util/CMakeFiles/util.dir/mpf.cpp.o -[36/52] Building CXX object src/util/CMakeFiles/util.dir/mpz.cpp.o -/home/runner/work/z3/z3/src/util/mpz.cpp: In instantiation of ‘bool mpz_manager::is_perfect_square(const mpz&, mpz&) [with bool SYNCH = true]’: -/home/runner/work/z3/z3/src/util/mpz.cpp:2587:16: required from here -/home/runner/work/z3/z3/src/util/mpz.cpp:2335:10: warning: unused variable ‘first’ [-Wunused-variable] - 2335 | bool first = true; - | ^~~~~ -/home/runner/work/z3/z3/src/util/mpz.cpp: In instantiation of ‘bool mpz_manager::is_perfect_square(const mpz&, mpz&) [with bool SYNCH = false]’: -/home/runner/work/z3/z3/src/util/mpz.cpp:2589:16: required from here -/home/runner/work/z3/z3/src/util/mpz.cpp:2335:10: warning: unused variable ‘first’ [-Wunused-variable] -[37/52] Building CXX object src/util/CMakeFiles/util.dir/scoped_timer.cpp.o -[38/52] Building CXX object src/util/CMakeFiles/util.dir/sexpr.cpp.o -[39/52] Building CXX object src/util/CMakeFiles/util.dir/small_object_allocator.cpp.o -[40/52] Building CXX object src/util/CMakeFiles/util.dir/stack.cpp.o -[41/52] Building CXX object src/util/CMakeFiles/util.dir/smt2_util.cpp.o -[42/52] Building CXX object src/util/CMakeFiles/util.dir/symbol.cpp.o -[43/52] Building CXX object src/util/CMakeFiles/util.dir/timeout.cpp.o -[44/52] Building CXX object src/util/CMakeFiles/util.dir/timeit.cpp.o -[45/52] Building CXX object src/util/CMakeFiles/util.dir/tbv.cpp.o -[46/52] Building CXX object src/util/CMakeFiles/util.dir/state_graph.cpp.o -[47/52] Building CXX object src/util/CMakeFiles/util.dir/statistics.cpp.o -[48/52] Building CXX object src/util/CMakeFiles/util.dir/util.cpp.o -[49/52] Building CXX object src/util/CMakeFiles/util.dir/z3_exception.cpp.o -[50/52] Building CXX object src/util/CMakeFiles/util.dir/warning.cpp.o -[51/52] Building CXX object src/util/CMakeFiles/util.dir/zstring.cpp.o -[52/52] Building CXX object src/util/CMakeFiles/util.dir/trace.cpp.o -[0/1] Re-running CMake... --- Z3 version 4.15.4.0 --- Found simple git working directory --- Found git directory "/home/runner/work/z3/z3/.git" --- Adding git dependency "/home/runner/work/z3/z3/.git/HEAD" --- Adding git dependency "/home/runner/work/z3/z3/.git/refs/heads/perf/xxhash-optimization" --- Using Git hash in version output: 5b70f75d89d20e2ada9f319fb17ecfa920da115e --- Not including git description in version --- CMake generator: Ninja --- Build type: RelWithDebInfo --- Python3_EXECUTABLE: /usr/bin/python3.12 --- Detected target architecture: x86_64 --- Not using libgmp --- Not using Z3_API_LOG_SYNC --- Thread-safe build --- C++ compiler supports -Wall --- Treating only serious compiler warnings as errors --- C++ compiler supports -Werror=odr --- C++ compiler supports -Werror=return-type --- LTO disabled --- CMAKE_CXX_FLAGS: "-fno-omit-frame-pointer -Werror=odr -Werror=return-type " --- CMAKE_EXE_LINKER_FLAGS: "" --- CMAKE_STATIC_LINKER_FLAGS: "" --- CMAKE_SHARED_LINKER_FLAGS: "" --- CMAKE_CXX_FLAGS_RELWITHDEBINFO: "-O2 -g -DNDEBUG" --- CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO: "" --- CMAKE_SHARED_LINKER_FLAGS_RELWITHDEBINFO: "" --- CMAKE_STATIC_LINKER_FLAGS_RELWITHDEBINFO: "" --- Z3_COMPONENT_CXX_DEFINES: $<$:Z3DEBUG>;$<$:_EXTERNAL_RELEASE>;$<$:_EXTERNAL_RELEASE>;-D_MP_INTERNAL;-D_TRACE --- Z3_COMPONENT_CXX_FLAGS: -mfpmath=sse;-msse;-msse2;-Wall --- Z3_DEPENDENT_LIBS: Threads::Threads --- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: /home/runner/work/z3/z3/build/src;/home/runner/work/z3/z3/src --- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: --- CMAKE_INSTALL_LIBDIR: "lib" --- CMAKE_INSTALL_BINDIR: "bin" --- CMAKE_INSTALL_INCLUDEDIR: "include" --- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig" --- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3" --- Adding component util --- Adding component polynomial --- Adding rule to generate "algebraic_params.hpp" --- Adding component dd --- Adding component hilbert --- Adding component simplex --- Adding component interval --- Adding component realclosure --- Adding rule to generate "rcf_params.hpp" --- Adding component subpaving --- Adding component ast --- Adding rule to generate "pp_params.hpp" --- Adding component params --- Adding rule to generate "arith_rewriter_params.hpp" --- Adding rule to generate "array_rewriter_params.hpp" --- Adding rule to generate "bool_rewriter_params.hpp" --- Adding rule to generate "bv_rewriter_params.hpp" --- Adding rule to generate "fpa_rewriter_params.hpp" --- Adding rule to generate "fpa2bv_rewriter_params.hpp" --- Adding rule to generate "pattern_inference_params_helper.hpp" --- Adding rule to generate "poly_rewriter_params.hpp" --- Adding rule to generate "rewriter_params.hpp" --- Adding rule to generate "sat_params.hpp" --- Adding rule to generate "seq_rewriter_params.hpp" --- Adding rule to generate "sls_params.hpp" --- Adding rule to generate "smt_params_helper.hpp" --- Adding rule to generate "solver_params.hpp" --- Adding rule to generate "tactic_params.hpp" --- Adding component rewriter --- Adding component bit_blaster --- Adding component normal_forms --- Adding rule to generate "nnf_params.hpp" --- Adding component macros --- Adding component model --- Adding rule to generate "model_evaluator_params.hpp" --- Adding rule to generate "model_params.hpp" --- Adding component euf --- Adding component converters --- Adding component substitution --- Adding component simplifiers --- Adding component tactic --- Adding component mbp --- Adding component qe_lite --- Adding component parser_util --- Adding rule to generate "parser_params.hpp" --- Adding component grobner --- Adding component sat --- Adding rule to generate "sat_asymm_branch_params.hpp" --- Adding rule to generate "sat_scc_params.hpp" --- Adding rule to generate "sat_simplifier_params.hpp" --- Adding component nlsat --- Adding rule to generate "nlsat_params.hpp" --- Adding component core_tactics --- Adding component subpaving_tactic --- Adding component aig_tactic --- Adding component arith_tactics --- Adding component solver --- Adding rule to generate "combined_solver_params.hpp" --- Adding rule to generate "parallel_params.hpp" --- Adding component cmd_context --- Adding component extra_cmds --- Adding component smt2parser --- Adding component solver_assertions --- Adding component pattern --- Adding component lp --- Adding rule to generate "lp_params_helper.hpp" --- Adding component ast_sls --- Adding component sat_smt --- Adding component sat_tactic --- Adding component nlsat_tactic --- Adding component ackermannization --- Adding rule to generate "ackermannization_params.hpp" --- Adding rule to generate "ackermannize_bv_tactic_params.hpp" --- Adding component proofs --- Adding component fpa --- Adding component proto_model --- Adding component smt --- Adding component bv_tactics --- Adding component smt_tactic --- Adding component sls_tactic --- Adding component qe --- Adding component muz --- Adding rule to generate "fp_params.hpp" --- Adding component dataflow --- Adding component transforms --- Adding component rel --- Adding component clp --- Adding component tab --- Adding component bmc --- Adding component ddnf --- Adding component spacer --- Adding component fp --- Adding component ufbv_tactic --- Adding component sat_solver --- Adding component smtlogic_tactics --- Adding rule to generate "qfufbv_tactic_params.hpp" --- Adding component fpa_tactics --- Adding component fd_solver --- Adding component portfolio --- Adding component opt --- Adding rule to generate "opt_params.hpp" --- Adding component api --- Adding component api_dll --- Adding component fuzzing --- Building documentation disabled --- Configuring done (0.3s) --- Generating done (0.2s) --- Build files have been written to: /home/runner/work/z3/z3/build -[1/3] Building CXX object src/util/CMakeFiles/util.dir/hash.cpp.o -/home/runner/work/z3/z3/src/util/hash.cpp:107:17: warning: ‘unsigned int read_unsigned(const char*)’ defined but not used [-Wunused-function] - 107 | static unsigned read_unsigned(const char *s) { - | ^~~~~~~~~~~~~ -[2/3] Building CXX object src/util/CMakeFiles/util.dir/debug.cpp.o diff --git a/xxhash_benchmark b/xxhash_benchmark deleted file mode 100755 index 2ffee767f4d2f166ff51bb6cde6ad5dd23cc0eb3..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 23176 zcmeHv3wTsjmhP!MOc5|uDB4kMslmcYsl-$gAf?i#paQ3`0+9s8_E8i`L8?ir()Ezg z!$>d*a;7Y$d!~ErZ+d#1Ztd~*v@PxJv61V=JO~ha#DJ~RJ_9XUWe@@?1VQTlYoEQV zPRgVoj`zEBzmHvCowe86YpuQZ+RwAkIeSBuYeAMyCy9_PeM2Jb@vo_rN}jNJDUSeD zN)^(@xSFJC(nY{?7)?#DQ~^@ea4>5$)N^_^AjuU{WDIzfN|po^77`@6@xtZ;HAO(l zsNy7-OHqzz!s;tkJ^@8~D!&pnUCMx4$pHugYUL=&IF}_$#_G{f&&w@~!f?CDT_k7X zawaY(pppAiK;chPL;nh{Hxp)0d)x$9Nr+}iJ-Pq(?IlKJEriPhKK7XWjW^2XlnX}7_ zLxEz|aI(vUKeefai= z40;o2W6>9kLr;vO=NmA5EIqm7@ZW|)j>X?T4!vOS0~b=U?rtuMJzR^^KmO zI~?@*!XamURjmh?syRV#$Q!)hTcu_au(_+jW2(yjC~xa&QkFqw){ zTYZ6$8&-PV7_ow$;5uaNqeS=W)>e0mHy8@|Jx#vwI`{o0OoB88P#~|TS=cy6xnMLb zQcKUdoptWI5_eVYY!X4Cb@qF>|RoDb;gxBesmI8`rp3d3>k=s&s0e)Ongc zK0he+tsZJPsPpf5B_xN!4fWSwPczqSLRZ&=pD-(7^(uYg{Q2&(;u2}0%Q!tTt7|8PmtU^jr6_p%o;2WE|#9* zw0R@{2ty`G+d2MihEJ6GIqqS2zI2e|$_5MgCrBS~eBJ(MU~iuEDaRWbKfHiN1C`0g z@N8)^$HSKIVTqR|nP^dgAl9E^-PcyA(hK?eQqU_oUC+m9K^OSJC8`{)J;a)WD1#b0 zTW70mQd~o)^^XX{8alt#U`ZnyIyZ&UjocoZHni&mF`rPLQyHgvk+~k4f5cQnDK#3p z+A>uBo8TMMMD>JAEmTv=)$K&Z`07xpi*J8hMu3IO41e$ z9StHC9@Ee#rKpnhxQ31foeEEB==_$6rES&Fsa=V%O+%k7h=5%h`lTBB9u5664ShgE zzg$DV5dDASfsYMWef~#R#r9}LV zl#)1{OeR-tVK{ZL#DO$U9V^k3#;HRko=xM_krF>ic_m zlvtU@spBM;rg7>piFs+9I!dB6jZ+6nOi$y~F%p-gaq19>tTb*Q{N(vmd8uP04ySSI z5QzgRJUQcmZ%EQA!!(D){FR*X4({f)_-h&Xz6^X<2EHQ$e=Y<6Wd{DU4E)C#_zyDh zM>6nD8TbPk`288UKLcNtf!~*b-;u&y%IUt5wee0kTaKk;>bO8f{0;bhs5gEo2reZ_X>rsS^u`AnJRUy?NGdl&Q(C2- zRNf1z_(5neOzS|ZT3_}%?RVIh$+1~4e_fL7b<1ky*w?4PVtM1y$G`%)205x4CM&91 zYgc?Fw76nT<`P#dY_5@&-SIZG)8|c)*iH?8M-6(EOF16@J(}zDZA3N^*@%LYwLKua zV(ZN<&(o4+J2C8tqvxPd@t+|L_N;|HWcBIK;Von^4H;~203*_Rkq2qN8-*3L4d_Uq z^_`uZV~)=wFT`erv7-hZpgGL?_|wqTch;C=CUqsO1T)q!j@>Th{rDq1qvy~AA-hbK zjjvUupn$~As7%CvALrks^3Ub`3srtI<pma=p&naylMBM-{Zc#~?zDiOOY+FGC6peh5nfQP{$G*Ev>Lq?6h6RK;ZWzafE0 zFT-Du@~cwuErP$05-&;fujTyzqVnIt`B$j?O-z5^D=24S{4JH03TWq2K2_=_Ucl=( zc`3-EFsIN0sNNsJ$RudbvI<6Rp@61%7%4FIXV~u%1uTlcdzKf_LtnwclgE*M6Vf-5Xy6U2M`-dJ`^W!Q&XW z67p!&4wTKW){mUZ{`+L*u-yLMa7|s6waeNs$L8LS^yFnzD_SCmJ^W6pISGGQ92ib#s1ff1a*vKFz*UpS>_AYH;ZK9kEG9%Yehu zZ&&u)yAv1Nt^E$m9*1SG((O?8bPwvSdz5ZVkKNLZMC)EKS@v57x)YNe)_%(#%U-+E zO>9Pob&sXT(hV(2Pxptp4l7dj6DyQvt4g`Xd?>fK$0y0{yC*?8_@Vnl0|eSfCK?`E zfnw-RQhaSI+SZd;-!7`3v`N;T_(t*&FP~w@lKk#Ng}S|nOz1vjWD$M$Aw7%aQPLhH zT|`L~$)zNU+;~m;u*VxzVBYTLvsAl-IhCU2Hv}?4z=FzpuCM zQid%jEhoC;7h8K2SP!Px;0-IhVA%(jL8En8c@1USMWxEMo>X3A4m*}@-KU(eK)Cx* zKKZIUZmyDgFP{?S_8z#yx9Af>cK+dShPy8Hb^Qu$0?mNX z{!1Oce!_i=MuZ%(1>M+MII!^1o0 zL+2IF*ixe_cE<^)ZSV86v6>v=D2LTf>xK(y~Srg zH}{v%_Q>tsIl2Mj>oWKTZXEjEU(2?Ap~G@)!8zG7BDW8obH;8#_dFe%W_T`7PVPo= zR^M?s7rD$gKqktz^N~Z!z}@#Uhx@vy5Y$9bf4&2hi!#t1H&Ruk{k5@&^d!8jM>!-3 zix;-K&y%B-aXI>nykROx=SSh%w!f`FKRp}1(y${kpT^AFKgCemzEgkqy%^mSA;Pep zc#~kX3M0y8ZJ42U(ApZhN@UwWxL?JT64Y-ZD=P@|GCQ+58bm3@ubt%XXyAPly4`@dW!OX5ivl!vNLX``A+F^DT8wN zph?yZ7{1qIcw(h; z?WaGnE3ex2hptZhkFwnckraD8cvM#Q$lY<1Hiy)B8;^onlS1Q{x_)E}$Bjp6cSdfX zWTw@lHoh6_nZ7f}yJRJ7#`KFBanz!cmcQ06jKnwfeYPP_-o20-pk(NLn&z$c_2wdY z;}uzX$tHQGK1Po@cu)XK3IUHtnWCzIQ*BW5U|Oey|6 z-3OwQG%a9@tPH?+SIgD`+1KS&@|t2(^iE~UJ~`PfZ#>h2bx!0hULKU8lGL@J=#-#f zEv?*RE|+&>p#aTLonxjIa*d(Gimcdt5DlBlqjgwxV>;eKE41h>W*58(O%Ainq#oPl zFxNnM7up?_%^05p>#M9E$(?UTu21|On9}t>Z}SZ%IZBowYuTCX+m%x&xolX|g&Vd% z0M;EQTqrkMuezcQSTXc50cY$Uv(AMH_XZgT)yTFtLeG*l_HE=AYrpjXtyj*SBpacB z==;q6?O2sdLkBRJb|8W>A`J$#=;fPRjE0UFkz#jX!FoB9f__8CQ$$oQB0`O}uW!zvHIz#ZdD!*~(X4HV_O<1#x zs?X>YvwEX;nA#mQR=RA-@S`MJ!b?s;L!Ntz#t+MifQF*yK z>bP~pr8sUHkz)@ORx211KNyiMpXv5HEd%X`M!;=&&;lihTMuA9Ztu}AiB8ckR;Czi zdxOUk7bERdcaEWR6TI8mZ|FFO0@@AF-CDW%0pqFeEJMc-2ui=*@SF99^Q)Bg`R5bA z2Zd^^$l3i~u1onK{^D>lx%1E&{~o7Who-(0P2J>tR}^)=E8Og|>~h9xj4mba(j6PR z8snL)z{~lvB7-RF<@PT4yT>Ghxl)d`8eP#vBeGHw&@yBV-KwE4yCTJDzisri%gI(!g9IeYAS*+9 zh`b8<9*x|t^1-VWcGN|&QI%dz=J*|s};u^dH& zMz7b8p$oM4qT1e$yyJ{sWyVMlzRZcS1nz!Uw!A})Kk+MYZJ}6idU#;#aX!8)uh9_i zR6fTHixK?OxCsInb#Pxt{S)^dRh_3ESWsnsPt$>%(Q3&Vy;m>WejC2Vsl1FHVUMoW zTMr~(ReDgXS2^2vn{)$^zRG1g8yU1GcUIZnkL-!}enj1tZl|`te7g1zPyW+RlWf_8 z8BIR@A<478on1Q*oxQHN@9cfKHo7Nn-&v&T+1uG{ z9-DO?CNb2?jW?iH-atk}yGHq!?T4s^{T(Z8)Qv83qs*piG>B|jIq0&)anF#8Wr3k% z4kjt5a>}VBU6x}`+uMeY|De$&HU%r59>ari@=xahL+42hA=^yAtRGnqR7cUSW0Oi< zF;}V4i9Hmf6QhgXrA%oAd&o1O5u9x5a|hIyk@Z98V@ z_+LP)l@rcbHP{BKEeWS?|BzW7kCYNQYL%51D5>QAx7*~h?J;z0gp}Hc?P?$XHu~_1 z$V*N%nfCK~L;K?xYAR3d!k}{$#&n(vzkrUcb8OB75k2`NSs1mC3_Yo-Z~1=@!a)cd zu(FV0Z+y{FRHV`)>o9GUqr{b_gbwNAehedu)Ao*`qaD_`EFU{#i;c3bcWAmuAJcx> z)*JT9Q5ej|Ak}`@j`4@v{tr;6+J1#(X=15B)UVe-!QT zziJB&mwR{q;l%V_T{TvbS2&|<;mPA{xI$&e*AMX_YG?O%Hsm>#fH9-VX?#Qd*%h6@ z2CWkqv?gc=t-WH>Rd`5?n+gx47!oQ=4qwc7?{!-4@>c~$N{lAE}O z7)5`<&43Pffcnq^`>8IpluzLIs?IJ$hYMq2mEpNMv(d5nb|VroMO6?@=~`g;P2EN3 zS1nZPbmtRh&@?`(###anzTH@*^em3vbNR>;<(|nX((NeH$GBA)skZE|((S3X{ML^0 zQO<@34`CyRFsIT_!%(3^$uVQoz@c>8+q?A6XwF2Zl9P|_X18?(6Ev3;x|IIJ&mrcB zPC!#&qrR0!{W<3n{{Vv=Q5})<98m|69dj@l*hdo2LxQy&2WvTwIhYJU{t3ucWH-v@ zfawdObr+qZ(w$2zK$6VX`>4rmj0Un{Ar^>-bK%Uy8A@C?@7CiJuq>g4?&%4OeOLBreWgEQXUs{bLa zL=|)p+nGr3&clCu*Uam%w@Q&27DQeo7H6!j6-!zoe*G#C`}&WcqIUl}Q4VNw$9kae z?KhqJzE|JW!2(m?=R@6npN0l>eV-mz_F&ti@AEf%`(8TR1=s^xSKs*!_CeX!9ogfI zvOJtoqjPs#8*-zt@i4P|2BK~91lY-o;4IscQ3R*L#4%%PCMPjJ%F%~NV=eCP<$w*j=ii97cLh(aKQr?JaEAS|37$u-jDjv1or0fe*ynz z@qY^cpWy#P{I}r$5dII~AHlx~e`hmZR15j&mCXCS_2EG9rkn8o8eS-D!h4kbox)TK ze=|~A67;R6x6({S^8zbPi@g3dctO%~lSwi)hosh4*%N9kE4|4yDoC|0UT;IBC4+2| zTBW)`7`lW~s8I>3BI1{p-0uy-B2!8StB$#I=bFA*W}@s&3nKpdurJ^@)p&!e0>NgF zzus$_=k?b&HhY3=OkhpdVE)XRGflOPfneBF8>W{*L#CqgnPsIWdL1-$gK1XDZ6@_C zQ6Scm5|a;auX;#($YO%5(8TmqdmDU_=Cq=+(wWxM3ZcsS=cr;v=*qCIm?=| z$ogj)lur&3uG0FUHqs0)tQ+Np%10|vjy5b(C~TlI;g*O6-PG)xe}ovln|1K*WO4vd z|86ol0$2!0@B3EZR;UfPe4T(JfO`O+09<|qn~C6)-%lp#J?cWN{b~RoLtASl{6p|z z8KcL&g&F*f*b68Ey%q2Yz&PMrfCsVjR0O`|r;^Dq;O5iG{|?GX1RjVUra0&(lIMYV9>%`{dmC8IvOu)Q@y~%DdO0uU|7-la;FG^0np|Mq zlw~g{Y|qZVS(jg6v=`{t;IU&7lHS6fd=>?uA+fvGvapb!M`%HSBIOj1{_K8f_!_f5$m$90q3MHUa+uO! z)gx4n7?tDUoJ9pio2VS^7m+{_e3G)fdSce%4AN~A<JQXlU` zzBdEr+=&Z>wE2P};mPQgdvv)w^Q9-U+jIl@QX)4O*I(pyWdBD#rRH1@j{sh7E0&~n zxos1q@9T0;=%pugpI>xD&p52$xDYOQ;DQG(c;JEuE_mSoh6mbc0fA7-AzxOoZ##%C zaQc=+i_^Cw6tL5%23njTT&x1Ak{*yF;C(X|#P=9eIgVu(3s^6(Aim3>wJ8OW{^|K- zfbgw6KQSfJyBQQXkOp}=J>a2m1Lk`Qv{s$Ybl7e z>(^9NI>-wy=y9Hru$!&7z>Dov7DWD6b6oJ@IVLL~vSTFdHZnZU3xfL&h6_8f^k?`l zc>0-)bgup@1L8aEOob)9zAHJb;cx|qEgZISxP`;VIo!%&7l#8J4stlmAwHsH!N{SB z!x9cFIn1>0PvPSG9>Iq%!frAZEn6A!ha)CySuws2n>jne(9#D=%Zp3OEu1VQ#)i~v za-yu+}29nikT=_`0g83sPVcvnbXDi!O7B(LD%66rJCDS3Q!h) z&gfs0M1SXGX+PJ~COQgFc$@KGp8B3k@Q-KzImSOlYM3oJ({QZv=Ck|dOC|ALzTo~k z=sFZOv;AMo=vSo13&DR2=-kDE#9$rh^nLK-RG|pszU}xp{MVp;Tmt?r+z;aZ*bcf8 zU%MC9sCvZp5C%XKeFdLEm%%@oEGkhs`EV%R3Ho#)tbswEuaO!g0^KiBSj*^YTzmaj z(w}vul-ZAd3Ho1wF1}wAi@_BL7RWCa2~Rk#_~r1)_n=Kqox| z7L~~Eg%Lf%>6zbWR|PnDMQ{w^#y0s2_= zdn+bRqvrc~!G9a*#BVaI6t-uA=sTc~Wq&>z*jV(t#-Yar9JTpf@p&(U*HbA1mL`IQ0H;^c)mKOFgdAZl$&@|RZ|6_enp87bx*cS?V@GUj_ zsK2y4;`hZN7P_(tFB_j}#pwd~9TH;ymx`Mu6& zS94ium8*GnX*sTCwmEdQ;!-+m_MGyHvf0*IK&(V5FSV81X3r_L5rz0lXP3>kl~&9y zFCiA9mY0;4&M7OIGmBJOE7-+aT3%LGI;*S-!MC)|O&{KuxUD5Eo*)hfpo0pk(xtIh ztoHh8PaB4MLnw?V?3p)<9h1=9++18AXljt?6Ld8OFNeYrJS(r4(x*AN!|bdDzc&Q; zu$hq z^*V@XFm~|3C|0+7!BTs5mAh)OgHD=oKegG%ahfW z?0^of0aWdw05V3`^Gc38i-X=(#p9f1vA8yMpu}hu?3@qv(UkMc93_E6J#aQeRh6TZ zTu7&Iz$`i~L37eVs*E@xLG9}QEgC?5lUnQA!#Mu@qeirDEVfplV71{daioS;4Rqjm zjSLDqkEJqwm;{c2$UNI3d!8{=Vzgp8)LVOeda=&FA7%&)97SgB>XSB64D{a2;g zN@v}Sethg)#5!Qr{flkr{Qd|#jt5Tm(_`8uxB7535Omgnt#%G|)s`jfjGggM#L@bR z4lMan^_D*9XOuctXBdvgIQM51A2stY9?PTY2(Zdpp&fkH#R(sJk@m;tV6{kJ?WsDW z%%@`hvGbWmomNvR4wd;*j{d^QI$tnkjB}&LIUB09EVZ^%XS7xP!N0R+!MB)etEw87 zV#J*NUz{`SXoz)gpClEB)-{JcD*?kn6*h_()`8w&i&X3nguTUR*~Klv08VKNuhWoL zMtnGU&ey<6IB{ntEmRphP03Pm!#Y2*P+>Tzrr>>t5EhoB5I53--X;$T@K{SzSSn^C zYB8e4s{=qO67tqd#bIwNP&VTg2Lo)TFZMR_WmRJXvv4RuJ^8YHNZ6R!RV9!Slg}9HVAfVVsRjDekh!dpS z1lqe4@)cZOK)!82tSsPmXH=l=6|HZ+o&J_J;)&_T%=Gg-rWBpwgDDkQe*M0zS?Y$VT$BkQduiX!LCFSjdb0XaU9k zGuT)l9oq11AhfqDzgR$KGb-I$S0zFxOG(nhvGQ_r+%US ze}n|Byot*R$lhTQ!hjj-rGLwiui^X10t$YiLf`^!&5&Qg -#include -#include -#include -#include -#include - -// Include Z3's original hash functions -#define mix(a,b,c) \ -{ \ - a -= b; a -= c; a ^= (c>>13); \ - b -= c; b -= a; b ^= (a<<8); \ - c -= a; c -= b; c ^= (b>>13); \ - a -= b; a -= c; a ^= (c>>12); \ - b -= c; b -= a; b ^= (a<<16); \ - c -= a; c -= b; c ^= (b>>5); \ - a -= b; a -= c; a ^= (c>>3); \ - b -= c; b -= a; b ^= (a<<10); \ - c -= a; c -= b; c ^= (b>>15); \ -} - -static unsigned read_unsigned(const char *s) { - unsigned n; - memcpy(&n, s, sizeof(unsigned)); - return n; -} - -// Original Z3 string_hash (Bob Jenkins) -unsigned string_hash_original(const char * str, unsigned length, unsigned init_value) { - unsigned a, b, c, len; - len = length; - a = b = 0x9e3779b9; - c = init_value; - - while (len >= 12) { - a += read_unsigned(str); - b += read_unsigned(str+4); - c += read_unsigned(str+8); - mix(a,b,c); - str += 12; len -= 12; - } - - c += length; - switch(len) { - case 11: c+=((unsigned)str[10]<<24); - case 10: c+=((unsigned)str[9]<<16); - case 9 : c+=((unsigned)str[8]<<8); - case 8 : b+=((unsigned)str[7]<<24); - case 7 : b+=((unsigned)str[6]<<16); - case 6 : b+=((unsigned)str[5]<<8); - case 5 : b+=str[4]; - case 4 : a+=((unsigned)str[3]<<24); - case 3 : a+=((unsigned)str[2]<<16); - case 2 : a+=((unsigned)str[1]<<8); - case 1 : a+=str[0]; - break; - } - mix(a,b,c); - return c; -} - -// Compact xxHash32 implementation optimized for Z3 -static const uint32_t XXHASH_PRIME1 = 0x9E3779B1U; -static const uint32_t XXHASH_PRIME2 = 0x85EBCA77U; -static const uint32_t XXHASH_PRIME3 = 0xC2B2AE3DU; -static const uint32_t XXHASH_PRIME4 = 0x27D4EB2FU; -static const uint32_t XXHASH_PRIME5 = 0x165667B1U; - -static inline uint32_t xxhash_rotl32(uint32_t x, int r) { - return (x << r) | (x >> (32 - r)); -} - -static inline uint32_t xxhash_read32le(const void* ptr) { - uint32_t val; - memcpy(&val, ptr, sizeof(val)); - return val; -} - -// xxHash32 optimized for Z3's usage patterns -unsigned string_hash_xxhash(const char* data, unsigned len, unsigned seed) { - const uint8_t* p = (const uint8_t*)data; - const uint8_t* const bEnd = p + len; - uint32_t h32; - - if (len >= 16) { - const uint8_t* const limit = bEnd - 16; - uint32_t v1 = seed + XXHASH_PRIME1 + XXHASH_PRIME2; - uint32_t v2 = seed + XXHASH_PRIME2; - uint32_t v3 = seed + 0; - uint32_t v4 = seed - XXHASH_PRIME1; - - do { - v1 = xxhash_rotl32(v1 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; - p += 4; - v2 = xxhash_rotl32(v2 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; - p += 4; - v3 = xxhash_rotl32(v3 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; - p += 4; - v4 = xxhash_rotl32(v4 + xxhash_read32le(p) * XXHASH_PRIME2, 13) * XXHASH_PRIME1; - p += 4; - } while (p <= limit); - - h32 = xxhash_rotl32(v1, 1) + xxhash_rotl32(v2, 7) + xxhash_rotl32(v3, 12) + xxhash_rotl32(v4, 18); - } else { - h32 = seed + XXHASH_PRIME5; - } - - h32 += (uint32_t) len; - - while (p + 4 <= bEnd) { - h32 += xxhash_read32le(p) * XXHASH_PRIME3; - h32 = xxhash_rotl32(h32, 17) * XXHASH_PRIME4; - p += 4; - } - - while (p < bEnd) { - h32 += (*p) * XXHASH_PRIME5; - h32 = xxhash_rotl32(h32, 11) * XXHASH_PRIME1; - p++; - } - - h32 ^= h32 >> 15; - h32 *= XXHASH_PRIME2; - h32 ^= h32 >> 13; - h32 *= XXHASH_PRIME3; - h32 ^= h32 >> 16; - - return h32; -} - -// Test data generation -std::vector generate_test_data(size_t count, size_t min_len, size_t max_len) { - std::vector data; - data.reserve(count); - - std::random_device rd; - std::mt19937 gen(42); // Fixed seed for reproducibility - std::uniform_int_distribution<> len_dist(min_len, max_len); - std::uniform_int_distribution<> char_dist(32, 126); // Printable ASCII - - for (size_t i = 0; i < count; ++i) { - size_t len = len_dist(gen); - std::string s; - s.reserve(len); - for (size_t j = 0; j < len; ++j) { - s.push_back(static_cast(char_dist(gen))); - } - data.push_back(std::move(s)); - } - return data; -} - -// Benchmark function -template -double benchmark_hash_function(const std::vector& test_data, HashFunc hash_func, int iterations = 100) { - auto start = std::chrono::high_resolution_clock::now(); - - volatile unsigned result = 0; // Prevent optimization - for (int iter = 0; iter < iterations; ++iter) { - for (const auto& str : test_data) { - result += hash_func(str.c_str(), str.length(), 0); - } - } - - auto end = std::chrono::high_resolution_clock::now(); - auto duration = std::chrono::duration_cast(end - start); - - // Prevent dead code elimination - if (result == 0xDEADBEEF) std::cout << "Impossible"; - - return duration.count() / 1000.0; // Return milliseconds -} - -int main() { - std::cout << "=== Z3 Hash Function Performance Benchmark ===" << std::endl; - - // Generate test data that represents typical Z3 usage - std::vector short_strings = generate_test_data(50000, 4, 32); // Symbols, variables - std::vector medium_strings = generate_test_data(10000, 32, 128); // Terms, expressions - std::vector long_strings = generate_test_data(1000, 128, 512); // Large expressions - - std::cout << "\n--- Short Strings (4-32 chars, 50K strings, 100 iterations) ---" << std::endl; - double orig_short = benchmark_hash_function(short_strings, string_hash_original); - double xxh_short = benchmark_hash_function(short_strings, string_hash_xxhash); - - std::cout << "Original (Bob Jenkins): " << orig_short << " ms" << std::endl; - std::cout << "xxHash32: " << xxh_short << " ms" << std::endl; - std::cout << "Speedup: " << (orig_short / xxh_short) << "x" << std::endl; - - std::cout << "\n--- Medium Strings (32-128 chars, 10K strings, 100 iterations) ---" << std::endl; - double orig_medium = benchmark_hash_function(medium_strings, string_hash_original); - double xxh_medium = benchmark_hash_function(medium_strings, string_hash_xxhash); - - std::cout << "Original (Bob Jenkins): " << orig_medium << " ms" << std::endl; - std::cout << "xxHash32: " << xxh_medium << " ms" << std::endl; - std::cout << "Speedup: " << (orig_medium / xxh_medium) << "x" << std::endl; - - std::cout << "\n--- Long Strings (128-512 chars, 1K strings, 100 iterations) ---" << std::endl; - double orig_long = benchmark_hash_function(long_strings, string_hash_original); - double xxh_long = benchmark_hash_function(long_strings, string_hash_xxhash); - - std::cout << "Original (Bob Jenkins): " << orig_long << " ms" << std::endl; - std::cout << "xxHash32: " << xxh_long << " ms" << std::endl; - std::cout << "Speedup: " << (orig_long / xxh_long) << "x" << std::endl; - - // Overall performance metrics - double total_orig = orig_short + orig_medium + orig_long; - double total_xxh = xxh_short + xxh_medium + xxh_long; - - std::cout << "\n=== Overall Performance Summary ===" << std::endl; - std::cout << "Total Original: " << total_orig << " ms" << std::endl; - std::cout << "Total xxHash: " << total_xxh << " ms" << std::endl; - std::cout << "Overall Speedup: " << (total_orig / total_xxh) << "x" << std::endl; - - return 0; -} \ No newline at end of file diff --git a/xxhash_extended_benchmark b/xxhash_extended_benchmark deleted file mode 100755 index d754272b16e69ec7a2dfa8d8a2c4bde0c994faae..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 44696 zcmeIb4SZC^)jxhW$x3+31_h;xy6R#RmAIStrJ~u8z+G4%C7}4agv~-$l5D!!K=3uV zf#x=>rY(=P)jndYZEdN=%0m$?CWP=-Ujnp>;!8lQyHXWUA%L*I@0ppqxx2}t*gl`n z^Z)$0`DD+`nKNf*&YU?jb7t=D{iTjcNjjaRKFQMc62*G1;+P_l@W^jO0H8=Jl!oKe zC|xR@gLn$V@$@1NkjkGuNwF|h;FAF<-)IU90LO5&q(ZfZ1SwylXU+(oqCzR1$0?tl zf=2qlV`QIE_{mHjSD`i^E3Zk=$H9w+a=Z$)`A9a~R`B#~kHx|=(e5_2F`}L%F3Pt@ zp0qLY&e}QC^~ch?f)T2|d?Vd*_exl2x@yih+8ZM7#5l)c^N6!`b-|2p}#<$FI(Wpm;O=QRc zJ{|_sa|ggb3*12XjVN#+d}RXq)d}b)qLBmfnUsLf`3d-RCaC{Q5ZFNcrz9wMVFLWl z1pEgl;Qw@j`e!HLFDKyts|5JB6O>z#0Dmfh+{zQsyAsf!pP)XkCur}r3HbaeLAf~z z_|rHr;y?bmB7r;&3HYNr1M;~h0sc1dzdXKB#APtL9HX<%!xIMynx|0i22N%Y0gTw&%MA??|1uVO`BNlt#!|;m{;xQX#=O+Qtr<- zJDvV2pLemd+FiTAU*&ZBd|qGKRF~wuWqP^4!0B`~Hd-u}?0FUS9v2Gqd1@EfUFCj@ z#Z^_|bNYQ19)G>vRa#zwk5a31nzN#=&Rtts3LZ6JQdwQLh#;8dyHHTAH^+Hnwk5lM z32Iv7bX9v@3v+6{i%S=MyAlh0?s~Uxk-L-^;-wmRYJu|GYf4LJmV0MGJSbh8P^n3n zTJFzt`IpqWQT@V7uXC}d(p_8nEt_vKqjaCUuDZg73e|8CK!O#{dFYy2r>ny6s`_^A z%tt#tcY!Na4dTyN`)yuDCHU6+Nq*>0i^p5cos^A9bUP#h!$>B;MsO__yv&_!Y@_c96)bbo>HEWkQr>?=z z#iy05B?p3GqGi<)o$bw=U)@k&#bV|D>Uw*BwHl~g*DREphf+xtwTp#zeH&GEq1AqO z>C77NVBO?%v%$cca>mNfdcV?BU+1lNi#FxDybXTA8-pUM0BERH?Z9g90*tJGZ`@h3 zAzzob7X8@Z@-rowUAx$W5@)*W8){$$$X2)(I$c!@o%1U^)e>n(6}Z;Qd8j} z4C(894{6C=ZmGsyAL!ATBPJtbb$-mC}yFUi{mFxoaoHSGE0*k_Tq`o z?5x~q$kG?g=?i9O<#CERbC54LD-JcvaSfFVf(lSkXt;;DEF`1Nt|{AgTmy~otp)w?+4f;!5rFPhrWx1k$ZOtQ5n-i2gGjiXaTeY9n3nb-O3u|L-%A)?XD%n|`YJ+Rpe4Ie%f(K~ zpW-7F`3jX(-lIIZh&z->Xf?*X+zOFJRia^(tb7(~CJvl*FoFkmhc+QIx97H-Y&Y6w z%fYJMR+=*8*4tQqhw`DE`L5h?N+0StK~>xe>Q$f)9p=%{ zRm92qzM;7r(~7L@k++tZQlUhWyfwu{u+(y-)bfdC?*W71Qpq0ak^}8VyLGewO1ZTx zRo3m61IN=BeIzeE-UMR94?o6i#YiGsK-KUT%DZ0F?tW3^U%(&eJb|v_XovD?=wbvN z!LcbUWh*Klnkw=Hc%BPHo?JE0kx=+JYZnn;B8YF~#F8K$MCjIB6Up<1KI(%!7|P(( zAtB;73Ek>9r4spyKJpGhehkwmYX6EL|2?5Q4h$jDD({AF3DZJWA2zvE*t+sP%^b>fbWt`j%s zQK_3dj@|dK&HIks_j%}I&Iy>>&7p1{L8jHn6w-;beaC7$Lu;dHD=F=ty<8R-qXs0n zt|F3&c9krY#SAC39>S%yoSK}!of zNsgeo;qAbqO=GBGm1ur2FGDnA?`@r3d+#`b=5(St<7NX*&H0L&b09RGSBp1C)E}AO znS&~4i!|08QGcYpM``CHEqo2^t)*QZy<}Va>=r6Y5bEwclOmK`9<+?m*c}RJ^nTInEb%cgnHYun*h+c;@ERaIxt03t~w;WVnN1L`#tMrz`%Ii#EpC(&gRSsn$ zbH~0RB&&{)!P4Ey^&qy3!Y5&~Gy_u1$I9W^<ll;V zdM`%v?WtQ*U|V6JQ~TCoGhv+5$uw)rmzVAGzjokqC`K3sJKZ{tFEo z8z$2Hz3&iM1vaPNdON1Oa5*u?%>Or50Ll%HnroG$jkLE0FSBgz_HXAg<+Dh)VdKFA z8$z$f77si1e?xx1VU59D-%oxksL_4$`zxYt8UeP^O4v5b;o2{|woFt0IlJ7R*(EET z>oHCto|6u1sQ$L~2uJMJE<^J(5Y7gQS&oqGUP1`arfd$Su(i%6hteZ=^cZDbx8Wz7 z4C{6wm+w{ddBb+y9(9)1szY1oZ$*+cE$G(S4S(7!!;V^e>aQ(PdMvw+?y(*H!lwMg zy0iY0KK-R)A3>HVdC2!KS=lCcgpAq}qEmioA&508G=I#-^uzZ6wpr!!(tpv#BRMe4 zBq7|3m0H)a&)T1d1%mqAV=~LZwWcP-G^2uVLM`p<=_Qh`kp+Hb-hHkbjzN0w=$?YI8ul4^{O1{ke42-!&<%JZ8_L%nu`*Nn>0$2 z2y5Bv2)<~lBP1cHDx^od;X)+^>z+|%v(X<@_!@3p2(g9nBov$3X1s$eShIK1PGR(-dV3|44J9yD(U3;)h7scO5!4x84 z@@P5Vww^>N2Z!G@4IQw{a)dUX2R>#(JaK^axQw$VC)yO_GCC(&biPs%+h6 zX#RlMMbnC5)b%#SC z>?G`g(o`e0hzmss$-0%dh)IrGbTO(C>0Eju{k!DLxq&wAsK+YQ8N1#>0I5&YN%7}U z@*1EiVx;lJ^t}m~jYfQguEC<0a3CDDV=6SW6NF>rR#3}9-{&OqRYaFU`wdqou_=?S z&8FW0X$X9Z?FL8-H@x!l%P-4@KXt-hO5Lu^oq-N>W@n27 z^VJ^ZHj^XJZf+?tT^CHbNDe+`GDEW9UJ_}?XA#xg2nM1bdGiQOJ6Ln!JLmVXzJ=wn9i99V9~y4;z~Q z2WCxHRtkI>XjXFdC6@uhTn)|g)*_~QTZ+=5EeGYRg@Oipp-y%x96d_fr>fN(Qy|Or zAJfiPC~qqkOfm|tL%}-?&0{cxsDQat<5pfU(`Qj|72!3dl1ee0k}4|jJCcep5ljdl zKv!57hi*W@>Zs{IS~^7P={4|CK}8~USU=+WnNGDL{k&JC_Mj3D>t{UmAk~Ocog%fJ z5YU@CSygb>l|*u#ATbh0>wBC5sRmt$|yLq9;}9l_NmE`F|K4rR5ehv=Yoq;B_8lc8=L$JLF| z3v~+-t&*zMIEQtuiO`1T)Ui}xGt0bzNj;eNCzQ^tVF}!@uYE){c+$kxL#@G++;1yt z@CWK!)PVF!Rd_}(YLE&%4KJz%`i7AS{db@jD4E7U2A~}qSg53-`MV6M8jvlr6;mWo zhQL0ucGf+HW<8E{Xpk_?vc76~U^AsC$5c(CW>HZzi*c)QMMz^cXtZjq1`S{)O&knS zTZ&luiL6G9G{arY01Kr;`muLn?JjtI{V))Cj@$*ZSVTIUUCj~y#8JhosvJC4+j<>apEDZl1 zk@;;T1S3@!)+=xfTgi>&*0R29SoRJI4X;5gX1xp=Ulp?>=1a@2z^6&F>qzLW56GG`+y6TnEzI`kT}Ao@GS%=ml%Qu{0x3DR&2sDA zsq**k#?oLFYNjp?SayXi4OS5+EDc_vjY?o5Um7qZ%%(AFHrEgtnN9sau`a+wjMTyj zEm&?CmYqxfHK=hrXy8N}aN?vYW^5n_;6~E+&?U656c!K*g4ZUB1p$0dWUYffY)I=E&9#L*RmRT6Z2SQI5!-Zd&7F9WZv`@yg6o!7=%m_T@;YEpWKas29;**`WhJ((9UJUpRZl(c$lqS`8+*D zU9Yk=Y_x1zJ1|+Q6S{T^Po@fqehDq1S|CEj^q<8~h*UPH`%R$lh*awB{BDDt+ z>_2-yAySK2lM<~^?*U+4ktWJ5cBaffS3`DWG<<}n0{CC`IvSi)HS zH#G1(TNpRbQcY=|#c>1reRxNam}dtwxrp^-f|=o|A*32#Gc#zHb(rm9R6{1AGt+XR ziR(fes-aq!Ce$TV(UW*tdABHkF6+C2mz8Xm6?M=oD`V@yRg`Z)+3NC{D|mI9P@T}b z@10IH=c0n7xTja3@q&u_v;PWk3{u(Z&G6s{sk~(B7ryetVg^zcE5B?|l1}X?;ySgT z!?DLX9Cxmb;q$KIa6&P`V_y9&fY2#;>CZ@~geslFep;;Eng>|BjZUCbXbS06!}UU^ z{)Y+j^g1;W2cQ25ok}q*A9gtxCDSRsj?6ne0UbL0-NZW8K=Ox9|L1jT)n&XoO^{0H zNAH|Yr-q?|U$0Xi3LXRN)HaqXrZP-)d>)&@#JfXYKlF`X*G(Am#;>Uu5)kInogd3b zamKkD=cXz0!p>}2`J0^CNgBh}9`G9#8Gg3KvJ0ylnh=U~XveQm3hCo`^l`Av|GXWEW=N3A1*)0(*c>bR1rql~&OI$zf9g(8j_0lV13 zJUV02DVUCl8FqW~XdD$`iZ(pnNq#NEy3fg-Wmvb@7TFA^R#Ko7J{!L5SN9ie{Lw;r zZghvCY$f;4>bF^|FD`*LQB!Z@aGamRycHZyc#=c?iv(fW{|-pYiyjD^wUjEzjJa7g z=4CvvR<-JIbZ`v1i2|xsXH8k23-2BJwgf|4HmqxAek*k_7Pq8a7MyshWh6XWC8l#V z3tp^`?=j77(b?8xokk<{ujBa$rM9J`ZC|&&slif%28o0&Otig;+hA!7E*veX$Y^MO z{9-Dd?@83H)(=q?vDK;yRlbFBAiOA1hk`JL>Sph!!l}VVf$%M`4UpJsWuPd{R*R8o zwpx^|da!7#1>b@8l(e~E1HyXH(ERR5qFl?}D758TN)&v{ zMZ-#6aPcjdSaJOk&FWij#kxw?qm#eR{=|tkyaHuvx_5rtMs}C)7^$4S4*f0cQwO~kStYcgl4|UM%LJmaSDTxH9QIG061jPS@U%yM9j-5?(|7W9Z4r#_LObbjcuEJayt`XhX&eURS zpk1g1wRoHFQ%#Ep$+~Uf4D2oj?Dc^Jv?DwNdGU4GPSaqF3Jo1^76 zwI4UvnQ^-V0*cn{`-lvzGw-IKQHxt(SE5|+7N)O=45sQ=c^D?f(fSx42;^U(+gsr# zGCa6whHGoWr9<22GZ1wVxI_!iL4=9AN9Fb_n71?FHXmO8D7Tx*z0Niy^S#an+;mnmsC%8ObFi3dpiHrz zlrPBnCJtE`2kuE}CuZ=Z1ok0^>PcZptOf>fK)(Raw#XLS(o>;ia-+OS=T~Cpg&QS0 z-_ub7bDwM^_sIqcq6xi6Wxz;O(Xo+4y^j+~n!xFiAK3z5F-2&eRM=6>@qfd%Ni41X#rZ&r1hfD-P3j{B#EH z6_6O=Gl_H}Fa|D`(c$^DrT8_XdjY6~kLh--%VXv{brCFlO;P7v)Gu%$GE)!!8A1UZw}ZpH{Txm>&Y}KX z3rin$6~SZPi;DrV3b;<4Z?#>xT3s|@dCNNtcMo`ArMfG@@i6bg#|H2V6scPgai-IP zj-w7t=N;IX#XB(cOD4V3`vo3^6PXuS}ze`I=Jc;93kC)&7n| zT|!^Jl30r>MEP^s5dSxPP5o@dE$32oNQ)X!eqtMORHUBXM(h++Myh8&Pw8_=<=f#A z=mgqB()|v@1_gXkb#_Kq?aitJu2dE9NmT(K zQx$MESHR^(7(1;FQ(fQPk0eCr+JdFH{Gnb4Nun+Bd1}L2l5FeY@FSz*!x4vSRL()m z5*d|;{@13A40H@vhxvayojQa>>gm;C6Qk-kWw41NnI;OFFFc#r(jv3NuDpWtvcZPs z?GPg7lfW?-xqL_;)XrCB1~-uE1Nv{2f!@x`zlQbtgy|d(pUaB+mGf|(nf6{-d_s~Uh!El+w(bxl6WG{7D>=`t*LqkkOA z$C_DEOpF8;ZmPrux2eIBagyz?C=~aER;G~KNOhsKjI;!AI@OXg0;2%OT6}&jY00#$ zhvS3PMKG&z!}imuNry;1y_!436{pNl&U~M%*Yob-&O=^=cuj z|MIben6}r^45R9xI?EKdjLZm@pK2MF&YT#k8KDKxIIfrfz@(#2Hb38zP$ibl{T$sD zb47yQb~=L{a1IzmcfeO7g0Y?oGyi@V+gDsxi`qS#4$&et8vZ-dxi8Up;Ea4dPho#K zplc}BZ&-lsbAK|2lJY&~Vsivj&Lh9!CR{V^PXCQkNP|jc`VmOf~-B> zDF!k)#oz*E&ae%rqa3_XC+@LCQtPWMM~aSYrOO%FHpR>?;vz0?XJnJl&&-tlBizoQ zD`4oLY}{cnhey!uF7CH&B1K^iIwcJby7M8gQp*R-i}nI^SPI)eBGL4cld`8*d7XK3 zhgqg6!wO2Qn^^6b=k*8hy^-R_y*7JmD%isfz(#s-!d-M=hFP8LRcLhQfLZu!dHkFN zuLVtJS#UxU3T+yYz89LRdKy4~fuOGntsj_v8>64_*=4B0e+^9X6eoF^NPHln`##$F ziUbqg80kba$V|~V939?E9w0QDFx;$&69#d|uK(uhuc96*kHT;kACYudiyZ|BHEV zc-6fco909$wt~aXj9bYU8g2!M#B%!?bma^>_6Zn+sJ&fDmH|#e=4r3OdoK6AM2MIR zQ@5bDs+*6^+uY43p;&VBJw}^4)y+r9{EfY$>McA$rglei7+dZiDjgkk~ZcC&i$= zh8EJ34C_{3la4@(O&5LviGt%{^b=Nx(aWAVr$rPT`D!lw2GTW_UUe-;52*OW@F9#Y zn;6>g(xisGk1W=N)0aei1F~0eETJL$y28t1$rBa+`Zud%#Wy4S7w$J|>X@j|9t>E1 z)>48#5=TAEvuh6B0HYs%4wc9IY|NAT}k+8Kgxioz$E;`W;~u4KB(Pi+`D0bhBgdCat2Ehhn3bqc7BqWBbCCac3-L zWo+v6vC-ROqdQ}xm&8Vs`l8`q^o6O=>9JALNws>zG~r*z*3H|OL`?4Qi-za-g(;~t zHhN!QG~C=5Cdvo;qT$ap;(f3WPh`LCt4X*bHmRyFi70zCOzw!KT;G>Ol+*fB!<%B6 zv?Hp%?@5AD4${lP%}`hVeLeIB;%rCIn@;a?j@GdD#&|^Uq1Wl@qdZ z6mO}9D%X>7!>fuZc>AH(uy`^#cpEHmW{xzql;i!DiK(_NCG0W>xb(f0`hC0sI-0+U zh}X=apLpwi*8x+sKJ0x|dRw&odCYKBK(gG5GL(tw4&^gh`IufxEug}Ib+lf6;J-p1 z7KD zlZz5Ex8W^M`RK=#SME55FA_LDh;E)`{%yi%8~^yOp}7twwX650c6)0nN}HCtdEbev z{)R7`81)1WPw8tIcGI=&=6N84Co&oDFX8)7@UC6M=kmf`m3Y_G&@u*Tlx-8pYxj1& zfAjDfkmoBB>Iee(t0j6FqZkQ?s0|MV-Y1BMVg z@iOxZAmHyYKa2Z*OgvpD=Cp_RV2QMW5eD-LP%|p)H{cUqjD)UZH?@b?ArRUPl&Zh% z`*YZv&&rpiOb%!SY4S$wHR(yF_Xjff;5#DpGF_Fr30nqP3EP#Ea^{;3>*shM4J!!; z-f*{Dw;CSUhFVTr7Qq#N&|#B{SKo)(gC)3;)ry;lcz=LimAnql;)A%X9{Le&$*k`f znmed*N>~n-V`%meXWhO7SsLwS<6D6j7hLKg(EMY{A8br_v=-wkM zJSbaVZ+OLyA;+! z&;54gsEiByqh)27DKvI1b<8jmbvu^5qr;;?LiKYf`!u<+pAB>v9o8=m%?hhsY5KI_ zBnX-weg^X-QTb4btpsd-5w1)$uALz z;3m>aup^&@VcGp?)v}1c9c@W3Z5hEF6VE9Tyk0Y_@DzL#v#h5M{5oon?3tfBbcg5* zPhQ^q{-Mh|bYyzIV{dIB%hPr2ewfD0cSAQmN2=n5MO1n>cieS9G_a#b@6h$w=}mqp zt42>X&4oTWTGOW~BW%j?>8-b=_s&pm8`0|s&Kzx5I`KUVz0)#xmgruamif29N4?aH z2L?fG2$P)}4VAE9MSLusH?Z+U8)l54FYnGf56*5Wa&j1pYhTB0Aq&F9_BhziXdN?RhB7AIderx6cm&d@ zf7*412j~T+K5d7N%Z5o%PRvY4<&KZ^VfwPIlGY^UNQpA2q_rgbs}iN8;44y=a08a# zC9Ua7q*NJ!%bSH?k;K0WXCVj34Sy-gJ~f}HPciDrppIT9Nycb#7$&20@dZaH<(HHg zobWh~jY5^rs*4VGO*IeEY0ExnNRwNyGld5I83Xuod^nU-WX(E0)Q5fziUS{ubqXf% zP%+YJ;+q24H)Rol9WQ9L7RbSuM#KGrFR{?{V4J-3LughL)D~m(u-t0F1);H|{_@~W zfgT;*EYA7yT=Iq=-81&RHK{+RH{TUouWUWm(7Ad4y*H10YXpon0%PAq;3Xol2b&sk zP)o>*Uk0*k`)5bU+Py)TU7FINKV9$awWoIdW3P?|PS?o;9bI46ck8;o{7l)_OP=Dr zon5b-Xb0Q`Tsz#mwjN9$4cqLktPFc=x_xU?6H23J>3&x8u?RNFgHcb>1ba?fToddH z%MQ79_Q{IIGZSd*4~b(rtyU&@VI>yZWxQyP6$6a)PbukEdV{><?37nO{SqYq#z*z~LmB3jEoRz>?3H<*~0`x1H!~PhFoP+wdc3v9`95!rv9_VQ+UTh_)_VQMMfjaka;4If zQBhC7{AWvwaaa!@U^=?02iR%u zN>4)#M`sr@Jg|-m-vT#BnzM6N>>LNw#iAm3{#jmsMYXZA!e7Bzg6Gs?sn|QuIK^GN z5Wg|aG(l=?B!$SyMke-1Lr7b+YEj-$1EpBPltRtw_tdz-mbyxCFbb4WDz9_9D;w%W zsYa<0ojKMxAHVVJ_GL=t)!xOG-o>?QrN$cTfuR)f6g^bLLu~|`;8dXpKfi&mVx*7g zb90f|Y(}HaIp$n*o;lxKU@kOUEoS<;Z%d9P*OF(+w-i_kE!J!^ez7|{J109gJ1;vw zyCAzT+nQs}vE*duQrFfJS_2P7&~CKoi_f#t$Qrxqxkej{x@IE1yz8*ZnW>2b6HX zt%@KXIR4qAyKAPTYfRT&G;B~Rl}UIy8hYfZNaRYQC>aEIqa>N|pNs$YUqmA9pp(+l zC#8*^Vi>wOwMn|+LhDsIrptk4`ELW9^B8162=NeKKmN;rUqkuDLo{^uvFH6r1l~sW z5N;LzQy?F@A3zV4zZU=Pkk#FUlhe|dC)v_Q2a=P&ryG)%Zc9sDh+D5_B)yIQ(U9eH zfKqW<`U;|3o@`4q22v)cnUiJ@NizatOG__KOLYvDGC-CNo=+l=kMbZz@GeO+)(l~! z;4cgQ*MYY84EPsX zbt@gpWWE}C*CVf6*l|tXu9amm)|MD(RLV2h{TzNBwvi?V%{ozRDa;b`Ng4NaOJhnhN6 zj-_Ebm4bS#1^>nZwC^L7QA#>8arim6J(T=lN>IPzoWP*ugXSR^M$jmXMf?{cPdaRZ z1$9fAijQIEqz48qPg-$KQ2$`cL&;^JxeYY8!A^9-9;93gnmD=HqjHm}pGwl!=#rmH zhTtal6P!&gm&Vt2j5Asgq$GhSGNIgaR_KE%4<Cy8^dSm= zevtmPLDIfK`aYYDZ!iC8a(jwisg-_sPQ|A+(hpPhe_tr=8m!-5E$tqn|F2r<<)QkI zs-+DE{o#eui|P8~HB!sDl={T^^Y&CrkBlbz6&LECsg{0nk^b{)=~tKNBh}LHFV#O- zBmL2+|7DGI5^Z2yu_t!|TOdDq&z{$DI#O@#Ssk$u-sJeexKn;F%0X6l| z0&42YDr)3ks;H4~RT0yZRaDF>4;9(zp-Oz{p~@}0ldAjVomBPCJE<}I@1#clXdyKo z{gNW1p8&7Ou}D(w&g8X&rI%CmzZ)zaNYNvFGDZK`VCfh79!encD?xtt`Tvjv)ZevN zf5#p}nms-YReIF;(zy6TB90R{{unu+_habkVH2DreTPS-ZIAH)ZmY2;RX|+WVo$e7 zSLXmV{mWAkFA=N}>j_oA=7>ogZ-B6;N2Jq*1A4wE2+3B_Lw21WT0dzYkxdHyH^(xg zgfkm_L%g)U*=Vl6YY`*xI4u}-#5c3&m(@39mNLe8i z!YC4PY&#&m1^6U<>4NcEPRQ1(2(A+N9)TCbRoXA`bIl0gQR&N2A;yOo;!*Yc5{whV zueyTcX$?Y8vB2*f%j3*xfS?2Tf!cMGpijS=)2p913w%)=zFOc_yQR`U0K87RNGf}R zV@QtlJjn1DNUELTSV^J_LsWm&4yyPLMt^?PZmIZ0_3vTyBPElfQue`t+WRT!CFwk= zuDOqnLOS%T4%RAu+zny)??mmCn#&0MxoSiM3xU5J?JD{KN2=@F-3jOi!Jel}7fPd7 zX_z3G2K+$$Z%=?92?J~dAEsa$R?mWd1aWHONJQDwo`BCgz+WzCw4gTu{ZQEZbJ2oy zwwc8542c5L8D7hQhsOgyBI!b@-}n`Lx`n=}`@-9SzYO&0t9X9ZelJPDe^mlJ-RB!f zp6>%s{nd6S=kMk~vS5NcH)%w4J{4%GfbeQW17{_`&j+6P*ZDXx+uI;`MBv*z9Iwu2 zqtTBf&z`F|{z?v{5g-_-+}R263liY(Nr3+u;gc}A8AX8t{1SNTuXz1@IsqR&I%uGJ z<|V+l0#EWOtKkLG{*oRe4DLXD>J#992K)%vpQ2SPJKOJ5=#PvZ`kBq~w7;Y0W#FmY zRURIHp9AS!$e+fev`QcZxRl{9lI95erly*JA4q?E0xvD(lx&ZVU=Q%rzpKV^Jo9xR zc!=RSPWw4zDAlL0U259-zz-y!+64GtB*2Fg;M1WB1M$B)0e&j*1IhEp{Z)!J;g1RU zY)*i`V0b^(WPGknfS1Z$KEEZ)D>IZySiXSwR?Bn7%yp`JX0=ui+Z?U+l;M(^4Dm?yryQ{Rk0w1N8Y?|$MclL4k4^&vxx8NJp7o}zAHq?6PYy#eXzq3-~Gq-z6UDb9_2SciYZrKG-S!$sO-^>Hqb5H)7oR!S0{XPzBRel2UfrC0OCBN?!sKSd6PsU!D(mUgv^p@4Sj?XC=->>YWu0jS?MERJ(E3K)pQ>g>$~A*5j=3`6`w`NPgcE zX+A3Ic2>f-1|S#tAq+cf(` z$vN3EquAzf&X_c*ycAkwD|VD32h`o0Q`g`xbrnr^*o!C5nd8jK%H_l0|3)ubEErtq zC8rNZLZyp%)$(0cK5wlz$9W^p59*gd!&o=C7UtA?7nd&5wk6AAm7H$sSf2Gv2Y0^D zUGKTeU0M?(p{#7nw_|5TYxq%EDeOc|OihWWeTK8%U+JlJHq^T-(W9=$3YaL29jB|p z@2V<757~{A>!S`YI6Ld8brzQknAbAE-VIw~;;j0_nFW=)%@nl31&CEw}v@_9~Gn*pZWfhroE z70afU=Qu@4+>~)8(~85A1GQxGVAY7#yDZDM9M`dHfJD~fKcT0V0@OeDyxl%!=2WJ` zrHiIx%q*yFU<(+Sx>~wIP#s-+*vmjxUO?JjH)9sJ|7X73F{1*Q_Hi@79Vb0z6?so` z6Em-(5{9eZA7hf47UsIV4SuaT0QPj#F_OQ<=$>e?LnBJb)u(4;!jV>vfv9y;>x|12q($Y%Q;or7ZHZ+HpHRU$yze2vA&B^9AnNJu#Hg&~Je;Y|!sMme&y6OrSCc_#O7h?nXgoxS2;_=oyv1oOZ4fWxA0vly9{hyVS z{q1_Q0CTb1w+Q8H6-S+mwewA7g87Ecr|9*8X4C%DSd0L_jnF1$$E%-x7RF9=`3M6@ zi^o}Xmq>EXu3hXw)n>Zu8)`70Pn?Lg7@tbdc#P82>w=N+yGv)*^p}=%L5;Uo%x};l zs+78-jj589RllUhUoj8R@8hsa4Po)`_SH#QxaZ`~g2~CM^Leof@GsGz<~4Y#E63p) z6{o_=WgP9n7&$E@q^!y%wJ3r^zmKQjK2<$#;KW3nNb|X?D=32q)m8hYEH;y5A(*wm zizo$fH%ZF!V}mDUvDrM!=Vi;kEO(VyO;=Tdn;JtgF03sYUG6$R_GZ)*j4NMga~^6K zg;&&gz@9V2kdm-DsHwriUEPxZTaeCY$Y;vjlYpazA4G-f`HWf!(Q2P75P?f3nxFiT z^r%p{l{pfhsvk{72Tni-ZiI+dQ zd+E$b&99ylsc?$Or`BJkQ{jC`r!y!uuAW1wkX0HqRDY_cT7LxD6T~OUG@2iN5qi|~ zG4BT-T#pPGeaaAa~Gny%0eqAEJ+W%6MAQiAKE`w1dtKby`sEKNR^?XEy zbT>=;#Ick1B2k+^V;QGbAyY05166-i)Ia0%DAW`3=ZVy04b6o+IrM`O}49Y5dZomaFQ)AAqAKs`=G(@z8@r zjrkz1{c3&{Qo1&O)PLP3@^cXVRP(8bOOTmxYWYR0c* generate_test_data() { template double benchmark_hash(const std::vector& data, HashFunc hash_func, const std::string& name) { - const int iterations = 100; + const int iterations = 10000; auto start = std::chrono::high_resolution_clock::now(); volatile unsigned result = 0; diff --git a/xxhash_z3_performance_test b/xxhash_z3_performance_test deleted file mode 100755 index c3573475ec35b751dfad59dda9c1d912ff3982a1..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 58088 zcmeFa33OCN_CNk!FG(DdL`OTKf*Xq{`F-xK_qsa)exq~#|MNfp zb8Jq(Tes@gty{Nl-MUp>dE8j;oN16{N>7=@MbblSEFDRuDL(B>;+~JShgxWa(ll z0=S9uM0t?_C>5VWhQ2UL%Qpg2y+lf!2aXikk`8qV2~xcaebNVs5*n!Y5m@!cSe(w)J667YxVYP z^>i4g=~IWgK8X!|^EAHwVLHm_qr?97>a=?OVVS5V>5$r>&-{P;YW|z{Dz$pYs|BC_ zaI46cbf~v?De944zVAmzB*$I87G}JH8$(qtoliE<<)Vd~hOuuS#|$4VeewD`K76S9Y5yH( zpI!5}x3{e!8j_pp5Dk5ZpEl${JP9eH5&HNG(k6-W=rbPQm)-wpY+3IdG59V^DQBMN z@hdRZrb?gEzW_U5e$55)w?UBe(Z6(o{FxWvb0<1~K0dY!@G(I#=c8YB0X}Ol(BJzn zKtJdL{2#i2{O$|znRJ16AG$!k^#XkUasheXyMTV4y8!=5(OAsp zb;+VIQlt4A?GBViNJZ;JMjSOrAD3%Iqo>K`^;Na_TrSDwSWw}rakscv)O&sImIW21 z4W1_Vf~w^WZc%prk}Kx>GSXcxUtNo5wX4D1w8B^Ca<{a2S}JE(ORg*C%=hKGT-9sV z*zNX=O@ySJzdwxO^>D^**nox_o{W9_9J23RhKgv%9IL96TDq zq^6;A6+tk|sYXLho=n$e8TJhCT1eXHs&4R9ugq-ntS(>0M4kq3dHsLac5aK?>uy=) zE*H&tNS690WceJ8<>m9{dlo=ZkR!aHCahrgd|!68Z*8+19m%WlxK`KKxSPuVOGVhz z(Rz!!xuL2W0yS#NfZCu@q3`8YHLj`#bRQjulB-MCD#9pnUQPB>|GmDfiq z!jRePJzf{a!|lSd(^A#47Tv6;Lf48lYh2Cl7O$tNs-fPu*0m}<$jO7Db5}L$8adAh zLPb7%rWj|9+Ofd3Al+3yKgU%$dw!;?LA0M2E>~4cOVwIelUp|+Z5T6~TYW-z;cB&K zLMyCS7Fmor2*9z%?W?M9fH_vS)Hk}Jy1FWFovYc?P+z^)o`q^nZg-8A4TWlBoL$?{ z>aAlwO{+CC`)_Qv8oKeh%jXea9*h<@j}kikU(SNYRv&Q;4*h?@hHa>(-rMZ)y19$< zeOc9>R-Yy!CRxy0{u}NYP-?ZO33kz1?JIADp)YJ&T@R-7+}_qkI1X|z)hk`qbt_%9 z7#n23-pB`#(`l@#Z_)&*ttWH4#w|6v8@+BHf$HY95{SLNn(9fDC=SXYbVW646J{r@ zTIA0vEp=t4rAxD%j*?PWMp{-dWe+7YL&=P^Y(cSjG3sTdWoGn2?RkAsyHvV(adC;m zWlzgY%kNW`(HG4RqwGs(?}OU=RD&}%Anr2ZX~s7~io`QY8X!djDv||w3`(gy78EAQ zif<%RL@mSTQ<;o^5%^+x;}79mu~z8oSLKAY3SloGk3JN`?b6CCfhW}0$4F@FRV{Dx z&+b6D7cIS`;aeGxl6o|}b$I;%iU_{~P9GVxzthSHFFAE5M6q(fN;1?j9xGW9z!F}? zc#L$BhOd435y+=VsXET(1Ec~C_urTTevy(x!(Vx1B~oT-k%nK*^d@P!hSxK0l&;or zU&_z11u;nLfYV3cAL;v&1LH-0m$v`W^EYYvQR_sxp0DGFZWQ?x8z+e*KM#lHYg;zX z4}|4k6h?nMEI)jGKNXfgE{r~Ioj_8##27ypqpoajIb1E!f zw;iU`+9i5~5W!DWSiUy&ToxCWuc?^x6T|XJNBYMWmaoSuRF)i;uj`uf)5G#%c)?Fz zSUwCW_$dm@w*+$~Ne#<~!3RH;VfnGaTuE9SmJe$VewKyhlRfL7y0H9#dM03VSblhX zxF#$=K8$`{SU&CJ^v{N{{K0xA;HI$rAz}Gu%O4Sz zzdbB}R9JpjSpMj+{QY71wy^vIVfkai@_$VJsDU3f@S_HP)WDA#_)!BtYT!o={HTE+ zHSnVbe$>GKKQ-{B^`dXowojte4)c31Y{%Dk`3$`W)V4iQySYQX**mV1q~7sQ;b|RR zBoTcbmGm6x?d`4I#5f&b^c)P~ba2tLD}>X5MbBd)oDM2_9th!dK+*H_5KadZJvWDN zI*{mT3E^}Q(X%{+(*Z=!ybw+YJUt~LoDL#-GD0{VK=h0a;dJoOGbn`9fkTfWgwsJo z&lhKd{iOqjo+BZg4i_-4EZ^5C3yN{D1o4_xHo^=!f6d55J`!enUTeRX@C`A70xJzp5X8SwDPE zKYV6Ce0o1Tryriy51-Hvzo;KRq#qvJ50B`FpS`m0c%2C1s{h^YQ>z1X6s&f%C;b7Y zSffrdjZcONv_`4^V}U=y&I7N(7=q)!aK3ueCv+;Twpo%Sq_<-N*Qgz$mg*O5>|FsD zCVKbjV_oXLvLrrqqeS9Fu8e zv=~&s^OZ!kcb9t8H_hPK`X+={_q8Y81z{;8usVY(z8iQKa-7=>i+a9~`e-P;T$CKdW{Y%1}h_;ODQ9 zq_0AikpDSy)K2rq1oBV$2E$eUnbL5T19}f@{o1Yfud{F`(`WA>kaAY_A6IvNHbdQc z%BaeF)tAru62RbkjX_lJVKMLY`Xu_g!pAXwQtPCJYFl9jDAD-Vfip(ao90*q$L7jW@$s{cEO|0~u1O4v}AB}Li0RDVK}+V+ig z^*ps>1`={>zI9u~hDfzzWRlu(Jz8HHwbwKnst0+Hjb=8J*GFIeJH+0%#aFvA&=Oouhtn zIc#Y%>4H|P&g|Lwq?UIBlbC_ohhnv(D4=#cY&=d>>p!)&{|vUb?)p5*+Ws1{tWUR= zQjK9}SeU@i0C$We+Rp4X1%lh#RMugha6WFOL2moPxIO=k;8sf9$T5T4EREaklt+sJ z@|;@UwW5VRi;>%3-uFN%MxRge9ZZ{I`8mg5_$*RJF4-PR-xvi%~m}=xmk) zkt9IdZW~Bj-*J%Du7A@v*wNujf|)RNis@0d-$_fHD9NGwf(R zq~;&<#nULNJ3lmDxwK~iXepi&1KY3vi;6ERUdS`o|25=Fc6O|0O*{?t(Z}e7Q%N}l zpJGwBNw6;GEx9RMhCOPu=S#RDCAu87QTG!L1rgHlSj?QTo zM`xKOPVLB0{g~z@SO}&isq%5vzbo(@SyTSo*7lv$1%Hp)IX}+nKTMqE_l~CZ8Ggv` zPiHR8pec${+q!IO+b#^me#}0q-?=8v*->&z_2;P_EyvaTf408pz>u|_jk30NVL}z1 z*lV(`PlvecPxziHvu-n#ZHPps!MeVJ`hdDee;3xK`pjXWgBu5s-*(E764d4t^6i@t0IyP^~O(3cz0 ztM$FUF7zd?e8WIw8hn5C_m)|oSde$Nw%orU|LoD<2JP9A@|jcqe9z9)O)urqp zs10e=k98a-Vec*WpKjY1HM_&4%=Vk2;k)zqwZQ&S-18=!$tGuq!Re1I_8*_q;WV6@ z<99}ae-Ze<>}WfD%9*lHKI=$1-S*)r8u6P`Q3YvY`wiI6?HD<5u76}){>hfldIpkj z!uWK_)|-bQtv)RVy4MIBSFJN)oF{3_cYb8nsdzFSqh5 zD(o!$T^8nc*4KJiv5(@Z!9Xk4f6yAMc1%kOybdg2IMLhd^q+P5Kf)9@2fWBT`mu;a zc2kwHD5vG805IfVh``}LrFP`1ozEmP;WQvevI!W z;^4@rn?M;~`PWN|5cXog6Js@{~ zeayfA6m0UlH+Ofxc%}<*7xKEg&)!&kSk2$ry5G^kZ8$pO9Q)R-Lu>T8=?F_c9?5m; z0LZCz!I8PCUl$yHt`5EJ4(UqYf2tj~5=VILGisp+UShRF?W~j$S?pH*zo4Qk!CKw< zvEo0d+IOk`1DGw5oTCgF*l z)koCoy%qj{V_{0^R{guTg9@Yhoijh+UBdR`$nUnc{~0~oLDqzo0SoIhOmwW+zb8<} z$z9|~cOJH>@&W75cUiX`M6H&8sOt~5J}V#6=WzH8-V~rEx1!T6JFJiFQT;p1@(+8b zl=%xB*+s+KI-juo2n`M>GRM_9?M zw>gk`(;4fV5x&K3dyQ(_UK6#pSnaqj$+m++6WY5_n}NX)srx(6 z;8ECF0FKHQaD0V;scr$YuNScJmw;-=My?Da-<(tlF7U{M?<0bf=TN)zi%ng8Q5e?YB2IC}ljOJTC(SAJ2Ga=gs{8Ai6u z|ApMuxkk2bYd2M*s&(5_(+C!Am^QGu^RnLJw$BV3OapH^OBz`H_)TY7E4QwNhA?r8 zDKw#;mu*NX-flwgu@>47+D`=PKF4@;ZcMU)7Zx)N>c*rvPGiw=Ce^8(DgvzMtnJU> zU`6$B)(R_8x>>7KiAtN35~-3uYHv{-_&mkRQTG+0dE!foN0c^@Hf%hi6save4krnr z;v5|}MmeV57-wz&6i!d=oP}joXNZVot7sF(z=FXTid6ZFK-!nE?6z4^Hfm0YTn2gd zX1GJt%!y-|HM?&*W19o5t>4amT(Gjg>39ZZ^qE06RzwE(D4RxEQXU~)8nUeCf1tGD z&a$NR4F)#7O!SQUwM^I_DL0SJ3YOPR)>mxZ_BB}`zMsPSjIcrjhQUZ?M{UqDa4$sj zAM(G0?Jo^E8Q)z~Q1qQ={G)(n{?Cz2?G{A_bEVt@r*{+-AQ@UAhWV5tx+nPlTbfYWUkQH6rS#frQ z2>`k%Zu@q?s*&aL2ZRMpb3=(-f*L$6ST7q4#oGswCOc!=G4sgosP~_KCQR=z6=|k- zfYWSxYS8osk*;B4qEMKgs3c5}{v1iSHMT#06k;QFQhO4Yw4I8w-tq*_&1gi4#|}Cp z#5Qa+gyEeiBACFGPlYrR*|8?gaiZ&BX%N|K6Twb43TZ^4kVaGz(wssiO$xG1CJUPg z>CTS!B%;x6+|h~P8=-moqd4lM3BtDQ->c?tOd`JCu_`t%Fl+?(-%{I{5NzD}|FE`g zGm|iT(OqXs7wz$Gz8?pM)KPAiw%KJ#$$@#FpmQBga(`lqr*ki{W70ZRsdY-^i%u0W zjp$S!rTtOiTGmv|C2gn7)>~w1ncXX$*+Re1PJ(xR{U~O6=YvUGI1kN10;eCYkyRjk zOFQ)(DiwL6b*AqSt=~noKghSp++j`on5OALzraI9e&HPmMgw$!1u08XgCvJ3he-aW zkvyuAEDMr!=_Ge)Bs^$n=sXUnl{7&6Pe;cM@N+l7&s|KLG|kUZ=bW9Gl*E#DU|U5J zE^anvh@)+$aB)=b%>PI@(Je$wA|`@4dAALSQLODh#W3;`Ihzw$BHzI3qPr-P4&zhQ z*H8K1B3D&W{{gw63wbQ+Uf`3Dd7&))3TJu#LvT&zpJ0R?J3kpOJXOrKKxrZT1z_>Y zuMiuE^&;gs)-LuvPl?6yJ5S+DU;<}^841=%Y!p67UlEb>lvqbWyIascB^(zr4(b_? zqVoU6OKHKuEhRV;Es{H1`pKW3LpO@;RmKuu}+`T_fPA`ve@nRlw920M89%5DCpE z0+OkjWIFB1-X$_FC>upVEdMvCL;(%&pUdS>i#yBZnbvI&Pp1Cs%gBae8UDX#CGFGw zXGzg;M7rNYh>n#wAYp0j8H;U&PN7c`r~l)?`xWP>1a5mTys~*#B0~wFo^};GTOa2=Slh$*B8kS`~$}e(fU~Uvk!+%~*Rxph?S6 zhZ?2ke_?Gu0*2%+)6s(3aUo}&9`3Ar=D=v2I1Q;&d-vjqqr!iHk6j)I3wtjey!fI! z3X1)C&ronkXD+^2Y>+JlIHa)TscriVZ6C_kb}RO))@=y|#TydxdT5gyjLvWf)ppuy zy`=?bSSo;I}`FAXV)D+^ zEYo$Cvo6FkM62qwO`z>8O(*le0~Yunnpmt?qg|`oyVJ>D&i_T*X`HIv%(^?VvyY{o z*mDECZoc2$fP+R zrJXmTyHVM$Hr?==aeeAtOV;``WwyaBIgzGxhT5qnRdF;jp7 z4xROnAa*k*l&1PA4-3R^D6ezQS=zPg5zNYOYEn+YS&E&2+=b*ueQPY1 z3+!jvy=s2;+!aq-OtihOzJ8Q!m^OWbDYmmDz3rO;s}kjdoh89#eZx#jCRAd4H$)U~ zk0K3s#>^ZewjEFl?L53Vdm<0JOb>@efENmf=`U5t!-{<2VY`Tx7LabIv=-FsvHo`2 zN8&SsHXcmSb}GVp%fx7^M!Q3VWRN9$w+(C4PMlnm1gb8<0p=c(U>$~(BoO&Rg2PNB zLgGV6>n-a+Y}hVCrCkQm&;oY~Fu2P&X{1bjf55wp!zdTK41~$pWo+e*$X4EcsI<%Y zk{6u4!NbuR`evhf05Q7`+o$92qC+@ntF8D$hQLY^0$RP`Hs>Dh z$bVQl!^aic)3-ihl3-qvk@NaXd#* zy}Pa30HzgK+fS1YnHmG1%-%*s%@{%A6zFEQ0*qW*-979Sr*pn(0V9sBacV{Zp&?8NqW;J5GC2zY--6 z>Zcy}>8BnKivat#kdJ?l6CqkMAC%4DUeSq|wuO#E!xWY2Tj)G(#)^C~V|kyh`3yGR zzFX*?Q3wP>=d~2k^a~g=F}wh zIRCtJ_{G~QU?6qqj5kXxerd-8xY1|DIq^tOtJla%yq9RQ7X?rYi)mv zX9$AP9oL|Nr>pP?Z2yoc({X546Fs_g@;{E{@RmwRMF> z==(zvdZa4v?`Z^InhAY&X5LGGz$~~2h8dg%oj`(nX8$*VC$LKN{PsV~uJ0I*-XenC zWqoH8`NJK&`=B4iLh&l>dkyS+4ea|xvLfwJODvjvm_^n>R(=By7#nMmIMLz~vbmtO z2Up1AL%q;SQl)i$E=0$bpDo$2VuVt()^DVN@E4Mf8H>0$;BHYcU4JI|T}TVKaj z8^i-dyA1a!=^}uCUmynLjt<;7!c`kb$9*Pth3nt6wm%OE*Ik<@`NmtH_Ld$k)%_o< zaRH_atS>Imgjw2C4zZ}|m(hgUVZ<$)S#M)8W5KjrHtU~7%lPFt@b`Zb?LIP6`e7`1 zS<1TpU!;SL(mjFYSq8p63uhOvIgqOL4jy*g-7M<>wb91w?Y^`AKMN3@$^7 z#CLuYy3+)bub?pwW&%#`z`NqQ&_wF_xlPB4O3$EDVC4Dv9_5iJypKpuzjj_O`4DQ_FF&e@#q!}V=qQE|9ZZft#F|429nW|Mt-zV zPYe&%TuU`OHATVU!~Y@(Bc3kiiBO!7c^bm~DA$mpz*J84voPO=9tXx&Z|iS*qMj0L z@LEpKst{SvDR==r|F@wucev-*{WBg9WgIQgstMBDP(pp+vAFlu^I1px2cYTs9Uj_f z_|8xEcOtt14}JbpLwt7%KhEQVz?XcjtL-d~2M&_m_>VjMui}TZY1Z{efIB-Ue+_`C zdo1wSE7aJ>bRxG8-Xk!N@Xm$lD&57|R~|=nDlRE4#(hy|XGPr6!5lAk3|0O3jT5Y+ zsI)+(LmIUsr=vJZJ^7`h)ATCcCtBaz`Wmi=Vf&M>`YZ7JH?9@sOFq+Vzh#dD_Y>Bi zfGN;b%Z}D4Xa4KH0d!3)Fa;ve5Q9U8nPjEDw`@&_Cz5oAOJ4-CMFX6kG zu6faA)C9iDY+Zi>%yAQnFQn2gx?2!xa@8l6K@#@DI~^ zHxPN@1}+aZU_Yk;m)5}RfIG-u(WCpd2F8JBng2s#zn|JiWh&mt#q7{zWYa~%ZVFUL z9-U@oh~{l@*5jp$j;$OoRjfZ@ZT~$9v+f4!_%K)pI=%`W|44Lv-;1K-Gf=zxOq}`G zU`Q>!-FZtJbIa_=BpfjkKioAk^I^H6^}%-iwPA!*v#@gU#b#>G1P>`kq#!xj#S4{w;SuyXb`aa=}nWt$9?`EIqdbK9;6! z3QBbM`CFPlcOgU9r|v(Uo!JBNgQ&QcO&6`(K1t-GEZFoq986-|16!UaiOfB4mfC)U z9S3go;-Uu*!f3x?ZT|o>oc0`4Ax(#%-S9cJKMP(OI?Nb`<_r z=T@X~+YU$(O*%F|JK(H|>okq)w?xxnrr$@;k%-g&8{<{$NqL%e_sf$Zxc7zD z=L2^T_Z=^tod5ps?%iW^rr-kdPW9x+7+s6H^ECc==9@@0f+;S0(g^J#39 zyGgDO^gmSjAc}1bU3{zi{madTkg)sA<=F&rh4+THsYhQ0hLE)WcgV!|PeWD91QJ>cuzT12<@HgOeSs1Ix$-s29qu;FZ zp%#TzP}ZH)efonE*4BOIV2gi5JEFxV_)W4fy05xHYf9?ZR3$YpU|>?uG9jbN2C8iH#U+Fp@r_#i@NM@_S_1Z zfE6u;mbT#E4=ybBf9dr9>ypl_(R5RKL0RVme_3(akom=JXK)+hF_@MA6=&yV$ICiz zPA(gVzjixS*7?)b&mCP4!nwEXucA1(K8`Xl^W)0oT|0Nhl-2M0%i7%g>np!vList) zdrst?qCEKxWYxbRa=sN*N0{mek?-&iqz|t8P2|E&iei9{;3wlyzGqE{@3cU8E3H z=u+zUlXPnS+1B^{`*HHMGhkh6-(TNF9q{kk`EiW>Kz$cAK}Z}f;fudP7W;Pnuh7wj zA3y)EXh45MWnp2V?TSpBidVGSX0|p}`|3SSwvyKRh8kO`r>VAnMQckH=Yfy}vElWq z4R|$ieKl31H@n(=Zm-XVcaP$A!d~gfeZLUQu5RTQ*B01jc|0|? zVCqgGen;-v(vN-)-VW=vRr!4GCT=)+df^4?QvLJFU+HeC^|UlrHC4N9#dxFXT5rAA zCOWVH!a`8n>Uv*Y-@dH&w5)9KRMps;sqK~~FR_=RQ&UrI;ruGxRo>PXcO#^;C1OspI@}}58%a!zctkp|}B5aqrTk31;@ls&wKT)n(!{wf4Uwvc!HJo2yE1y$b;w&$d zNbO4l5F<$l#~=Hxe#O9(g=K2RYR-WC8gM; zS?(t4ue-)3E%5lN8uWpOWDA?>uWog-O}I(YQhl@uu_a66QzSDCo>cp))S6Onfc>ewnurg+`ey6V?q(W4K) z$q);8*yr*hfg}i6bi0N>I$h+4p6Ti7_VkSO%=E1E?DU-U-1NNke0w^*KHHvY&$4IR zbL_eHJbQjdI^KYtk&&5^m64s1laZT|myw^Do@vj_$jr>l%FNEp$;{2n%goP8&$4G_ zWMyV$Wo2jOWaVb%W#wn5XWO$gvNN-@va_>uvU9WZvh#D&bL=@8Ihi?GIoUZmIk`D` zIr+Kix%S+Q+|1mp-0a+(+}zx}-2A-sJbPY7US?iaUUptiUT$7qUVc7A%t!P2V6B0C z)XqnVB#$so-HPtv^ju1R3Tqr-+|#|i^b58PFd6XpGrhf!BEq(H_4Zx|DDA{n5#TuB z0+c_xtG9Op;HEvjy+wdq0Jj3hVGX4n_ZC2kzcwK{+yvN#korNubS&3hfHnjMHpHHX zKL$U*qEC8zHv=C3w72&y!1OPBd(+Ww5q{M>K<(p`Ab=!aGf$G&#K|Kpkx`q_7Uk35 za3@372}DyCNedpo`xSrMCKdgyxA!pUq}aHbv5A*hmDN$}q#48WCuSy%B|55)mnlf6 zpbM@@nfOq?58va+KS1@h57BJISKZy)OVKEO((&Db?`FvGS3s#GHg2P#I5zPXV{xpl z%`_`E-LNn^)`pzo*tn9|C>%B(kZlp6_IZ>4&nHfEuX8q`7#+HfdkdUK>p`pDN* zI$6_^_kKD|l1AwIcA_i^-^JkhA;!w|Ck!a$x!q6_n|PbCB-YkxDv3?rXfBRTza^qL zHm@ymR_rq4SVMGd9?7sn2rHqy_Lp9RNij9&D3e$7||AKylg}?Ot2isM$$BVNzd&c_4dvOG~Ft6 z(n)e{BpbNJR2G}uW+p>;R)~OM5-O-rq%zcBgL)4JdV3$D`qiR-c)v=6{kkN!$l#A= zRfhL&mLgSxPZ#Q2Ft73u*P5oBJ2vHg$EGZHlWhF_{DV_TeN*wh4&!|4GyIt#c1mGm z?KtmPR~juQjCI*LV_mM$JXr>j?!%mX8EMn6A#Au!-eq&f9=O=>01UH~4YODwd)$mV zd8k7NB&M~f1EMzLEyxwNNN3JsajP$RwG1ohDD0xo~-a+xRTw=2|mnyxU zOKf^`iOsF_Gx8&ORPkUQNpo{Pwf$H=N%>sPKRtqXz!J*MRR6w`uwFA9nnX}>7D!GIK5+^K74jb2^&2mywP8LHeV$m);#{`@1-B1;kqxul`sD2 z@2A(-O}!i^^d2I36uy%_`o!6w1r6j%>2p{sr`sg-*{Bhc@1+l|h4i6#E&QWZlMdY= za@iRoxm`;nXvBJqLaz{`&l2 zh4UiD>oi3o?q*z<6My&1c!E}r(5_Fp#{T~?p#Ohq{TZg)L{5b-GgUuRTr@>7c z+@irpHQ1%W0~$Q6!Q&c~#z_2$)1Xa*=^8B3V5J6^X|P#?>omAYgIhHCs0O<X5#$$um=_ynbP@cnigV482>pGuTPQ&L`9}y{*H+3g}{WQG=ZJJX@kTy;0 zD4jKEFws1O5j1DV)ArBwTcXd2&!Y7GaFpiUgjtlPu-2Rx&;0*~>gFfZP<|YwF&D%) zQ+gB_o2MpRN9kqgwpks-?G~YrW`}6^6Qa3G$TMUh(sz$wno?@_K9SC(x?6@*{?w>c zdOwiq_tf9+F_aZa3N)32J|Z$ckqWa(#nFS3kX9B@#zquIC5q17g_=>rM2DV*WKqLK zC+;Ph5iI!FKfp@j1}IT~M`hzP==Fd&3vrW-73k`K!Gm*w&;UoKpeq-X0Iwn^nKWsX z(x#z((^jMPJ>*4xh{rSA0c@+`xLl}{P|uQCuFHAFw6Br|+esbKik zkoQ^c(?kB3@o$FEwG2b_w?k$!{BFqa7@i%nlwt3Xn*c4*l00M|5^+__y^`Xm_gD>t zK}?2*WlCrT3%w|?0WYTlN@xXhOHptH46dRAN@xYMD^Sn{d^HtNLMxb+kAec|WD^xo zLMtewt0Od_AEE-D*+QzkDil0`0ty{uN=R`v^{b@l$G;+Kd=KjdqSRn1QZ^4l?=785 z7Q@?>GOWi2%O>SYhCfqQGyJ)7C&OPTe`UB?d5PgKm7@&rP$IGJ8!UG!$qesOW-z>4 zaWcF|X<>M;au>t@IfmPne=~ei`3vF* zgJp-ZkKx~xj~G6sL?X^ISpKeD%ZspMut0;+ZgUv{>X5T@*Kl%F`L+RDvMI(sMOG=>zmoPk_T&ux* z7{07Lslh`G4=N`$IC3Pc*`mlpiaBAChb-kpj6CFKPK=OasV^4GMRF`D+hQ3b$C8#U zmLxfr)N8RM%dw(*iX1DdPn2V+`p}7R88MGW#|$;V)M6r(m=V{*jl~wmjD-iAaU;33 z*ec~axH;oUc&pgz81k4>5tYQc<2>+fH(*8b;~O0d7cFz~lt(1 zA7QT7oj~2cBJasye(@)0AoeFQ*P)mgyo{39sWhIvej+v2@*xE3LEf=oEzb8H#ac#7 zz6D<)LSnGe>L)P6EqE1D@%wXXts+oQS_y#kC9|v>^kQG4!X3Yc} zKf&5W1lJRFkbpTP&H$TV)I!jEQ1CmwFuD%eQep&pbH}wvJ%NH_crIFxyH2Dpl)oPql8~Oj^cP4=L+Ro`e7+&ZJ`%l( zzsHnd7@V!7LSKf#If@q>4#VJFtcBSb_2ibgecwwn)>ml??p}=qbqmAD z5~YdhN|nnPmMcp*f2PvNaF()`p{o3p;U&rhrkkx~Fmx)@8CEElFr2IGWx7h`Aj344qTzCk6mc<9rgsdMItjiR(S}S9DKZLA zM~oFy%=Ert5J4iK7*7zGKf~~h9>xI*1u60g6eIXFSuklL&Y;lro-9)xiUUPygoGh9 zeJFDjLSdoEHa~$C!Ir=-pMu0tJSwN5zIae5D_ufijp?v4)&qp%NN#{1_@4#wF`13A zrJ$tPQft!==B6V?>q97}P?H-MaZtnv5_5uy`%d8}SK;;~^M1_vF|CXwQ4v3=lcGE_ z1(^d(=Fen!H%dqR#t3F9f*HlG{c8*}furd;BgM1aSJAOFV#&RmJ&3gZjUk32UD2sb z4@qArMrT+PAu|jV_{y|zlFVNqXhq-iuPAGZ>|abQ+QmjTceVByCvJ5jj-$smxi_1EDnQ zQ8I(ih8zJPIjK+m^=mid3?7!kff# zGc3G01Ej5t0gyM1k5qc zpm-w4szYIX^d8idj347U!5T@fQZklercOvOSAZV>N$UuZO&Dw}B5V}W7e@>xmb`g0 z1)!p2^RT}lW9;i_{7{NLih>T~Bn*2>rp7Q6eM!j~Kr=JSxDcUIN-iUD#@k_@DS3<} z8qYwslzc{P#vM>nN&zFu#zl}fWhx`-#uUtnlxd9Q8FxV7ltM;|jEkax6fvS2k3qDQ zVn!;B&rmxhj4U=zha4$oL%v4Pw9ME-vdv8R21uRJ52dE4EOoQ-St@Zb;xj&v&ZS(U z&=KAm;}H_4V$dd#dJXmB4j(%s|~S9BU$*lzqc zhA3qj%hqM2t$xb#sAMqM122k(CPwm*L_C0YCM}X>vLf14Ypc{2@SXH~qm{B-D4QNq zQF3*BDx{Qq{l^F+KiXy49NggoXlluh2w2yNv>5xMZ;Qp_7Lib*4k7TQLU7_`R^Cy4kBb>5C2bYUR#Gt?74%y?1!=@e;#DZ~ zGV};h(L;*dLdyFcgq-{xH}kI`15Oc7tu1OhVlSy`n-GtVAHvm`Mxs9@%IHXf%OrC= zG2g^mq5}#c9rM*y1>2c47ODayRnhT<7y>~ML6_zyy&@RXnFia1(3iQC#^8D8emfPh zT~IxlP${w(Mi%46SWjAMwEP5+TA+iF{*>lHByj38NCjFv%~taOAD zl2s6y?NIgPZstULe^Jij#H_#snB*~9t^y=U=*T6k+?+t&`GiM;PGLk;z^2LrZXSZM zp1h1@qth87Bz0FZUygY{>1G~ZIq*yjKi;zoPdsNheQZK6I=T&hSgHo%AZ3 z6`k~iF^t$rLmhA8G6gZVs1_VlnewE_hw;4B*C^$sMn+NE_z^g!4$!>o2rPrC(Ttdk z^cPjB3L{a*S&%8!!idHA2lO~KhLJd9G{z`3mXQSGO;krX|3u?sXfQR7OGX+CFaW6o z8L=7bpqJDH%L5=tHl|RcgRLikq)WU#Fk4|ElTLD1=m3kmDVdj{*5rEb7aeDX^ul8! znSVwaSkEe@W3G^LwDKaVKZmQ)@mK%)5uIcs5n^gr5CN?+GN)LLVt&)enlosAA7TON z2s-HXUn* zx6Q@7h7zFKblMr-_Hoj7&nN;^n+`$4+vehrh7zFKbT%5+c8r(oV30hDAXTR`(@^7L zyaZ94Jd}ut3GFUIA_$_04G4fH-7RzIO}h@kMVKW0YBlLwdB`L{+5pgIBvh`MqzWf7 zNj8k00Z2Q5-=BwQo-NM!kQ_GxZP8gw_8QRrQH~*=QBrm!6#OUIN`Ze|oHTzFsEk`> zBQc6wa3@Fy$c8!$zC!1N1L7iY2mJs!?pZ1^#9fMZ2bkh=z$=o@^djl#HisSyqX^I8 z%z5z1V@ILlvb4-7IuJ8B78t!$vVf6=#@C>}v@038%(xReOk2XpBI6R` z=3->A@etLiV&rn;cT`f%$Q4EpmADzX()coQYhYxF@$bZ~k&&g6xdihu?HWG3pc6$l z0}hp>q_>Ii`XToqJCaTxNBGddlr&{4GAhL88maQ4moeBWlVT^HM*ky^6Mx!G@K1*nIrC44$PA!l;&E_^ zOhE2LT=3ow3<0VrwWUwzBL?ZCHXC&=MhJ6Ha?MsYw@F_d+kjyuOgMB+M zJah~yawB3e+V-nN2ur7;TJ{$Z&b~}!(;=zGL&5a1f5JTI$W$Ztz#{E4M5s$As9H9? zg3w+lczmj7%aoELsRQO;pkBrvUcl&}Rjg!nDApLX65l8}mgG+(0$P2=_?X{<{xe?U znLnS3XwSfycyN~^rcy7gf`P9O1FeN8F)nsRi1`-~-5cQ74ch=yiDZBB7EGg4s!5!bCEsu$>L7q_&%kbTq8>=}XGFpS4Q| z#aiw<8s9CPOUK4xN*MN68oVJ!Iz<*88s;Dtb7VSC7JZ@UK#Ew5hkd?S5b2CLR3>ab z4dqhO!|<&3U94{NU#SDH@YJ9~XdW9W;w^BqzbU#!N6n%(E89fpAz2f|Z~0H7pV{fd z4}m1oC1a?UW4N+@&7Gj5Xc34L2gzK4^6XsRo6+gCD5CRh$vl^evIY@C2iBTGYKYgp z1F80mVD1Pf=5mge4~`cvL*<--O2#U?loOB1WqJ~}pO?t@7?{FDzY66I6BiiXMpyHO z^Q8qoXEwcqxsx|S+*Y_5>HJ}dbg|v^I}qj%AGU?kbnu-&V%T;{4}w7XBZtw2aK8AQ zKYG|^N^il)<=ckSYkN$8AU*MoGv(k6(M@)gnphhh|yehJP~@q%{r(flh2K6Ne!igfrbFF+N;WQRg}$-I`EPr=`4QaFc6GiKUR|H@6SeF z3~T~n^mk_?vw>Yq82#bd$Wma*gwdb2jl2|C3fIG*unl|++8+2cJ)Wb-Kk0FV9-qD4y>h=Dr4VYO&Li)y2pfgKusY zI@?l0S;asL@ts7~r!GYb9~r_)t+uGxiITJc$x3{qj6mv z{v#515Hb$P*GPOxNE(ntH1#czCG;9|tSq=jgpvXv@1W!jd zq5>!#2ih_CM!f}OG7|LDc+>$PSx98yi=)3SVQiw&l2kf+Gd1`m@{2(-gX%mAWDXK! z`$FE^b$Rs!F{4j;mW%<4C3!<~>O^KeA!xyw{oB7`;cA>n|XAger#QdR&)FPv|Ws62(q>3yT553_k!P+nruwvw`I_bM0d;9#P=1Yk*^D&*2PK^WS zCyiP{q?f#{lYR{{dReXzU=rD$E`YLvNSCvml2MY*2Fb+0+B89BJppq5EF66^W+6`y z1@#8t8!|kd*rX@)TCB*SpdE}aPmr-l*a$fQsnU>`jIX9py>@g9axNS7I5kKUq!1)i zsSYWW-giSUBapaXb9KdDkDMhVnS32eZ_vqUm*XdLd?wSSgq(ro%482%*_Ob&%Q+e3 z0mnDEo1~m#Dzp6rWOB}2N)Kt4aubL)Z!bJo-f$n1L+Ua!r2JU=S$JvQvPfL4yNI)~ z;uj90+##znr0H5JQ<|ZrvZNwTVKt}&kwRQ2zi5JwPozpl8m95h@X1rM=sw;M{ADBJ zb}GVl9u9hvAR~t~evLF~3YCm+ktXHTQQxk*B^skVoMTa=Z5kF%Amn^(TM=0y-An0j zp$VipX-HTGTydH_V_1k{+AtZFB7&Lb ze8mwjG9#^$GA4=|h%!s|c*D>qN^l-GAW2e`>536D;qN&d@mV;YQ6{h)xQBy=!GYw6 z31`_9t22!yRydIemO|`MX&h%qvG`+*q5Oea(k#>(logUAew1vFpC@lGQ5FteJVw4; zS)@=;67qw+h0SIK5o&+r7`Xw`4nb~I!5En|M!g%VRe|7Gx-`MY#G-giWK(R$7id8BEE z$Rs`>yJ})$;Y&7`;C7y%!q=o!_)!K zX@fN_7E-`49ach;qE#BG8HRo%R}?fao)goCRci_i)haz-VGSBC z>svrWS>8A6R(Y7P?wJN{tY?L$6>C`yX&oykevy$bVHR5d^w~Z;$QPXsa&>CcMN>qD z35uAmDA230Y|_r0(9|UZm;r%CDmLhJZph$?u5xH_LJ)c>N~6N3!#tWW7-FG!F=y~g z4^LNp_!0I_MGg+iN-%8X5-uwU^QenL4ir~oLQ@@Kda!$%7b8J>c6*e^SD z=Xs?fFNCEmQQ*544kdw?(xJ#z;d~tNHiew3)QOeFjPswHX||K+LfwQm;$fhaVHG{rQ{HWOME@F(h=(cfZ}fN$57R63cmt2f zPw-I8b8yJ2@579rOLBy4Hb*>S9%w8^B0k^BdH_?!76Ud#QnIVK+cX<$w!gIPA#%Vy)?2-!r97za~hiCoVdZ_bkp zCON`5R5n{1&7%o1uD!%O-dI0v8ZO=$Oa>~7A?At3pZpMx!(_qE2WBgR%#f=wtNS6$ zMuahQr|FU*Hzr~QNmlzqn2ic!RvnZKxsc49Kq`o5rEH?-&Gh&JeWNk9$8 zF)}h-gb#=yB++;k3BY1;0792jAo zBAcV9n+L1rm|9f26qQIq*_bXW#ahkgtIToeoNRneN;Ah9|8(OtPNVxs+aUQAum?Ld zL39HapOa;dxB?_`sP?jyW{}}~R=DxrlvPqI{sPKXTjllHb6h^j<*IQnZ(RY%`3-o5 zi7zJ$1*@yQYie5>C3=-cW(G2DaIdL$%*UI`5Iko zYpT{tF2`IKT5!3WYKT?7%eA7Z)m6P_O@^K1udQlr@VOd1)hk`io`(ABwdLpzTBhz@ zG2fSo`)Umh$f|Dj`driqUSQwQ>a9aoz1LHnk?C6HUG1%|YO2+ULIu!*5AP}oW#G)l z=V@(_e4f?SzLqMy3WkJR-GX<$2=R2$Bv);V+uh>!y6BxaV9=+p)Q#EyStZr0mY0W( z7!M4DZu0Sn1jP?ZU)|c`s`fOrHa21WFmSAa@1c5oI=>)>M&FGFU96?%D!hyZ>h)FC zH=vu1RV^#=))g9*MjjLtK^v`jFA&kyH#S2};e$hZFJH3;+#0LaxbVuK6-_RoN*Ev; z8uy~cUESbY+w4wmYHetMWu>4($QJX^1+9QOMr+d{Qk`fp_V!da6B8?KNt}&*c9+1JJR#4 zZge+RH#S2S3`XN}3FaS~pPuDE!E2MGh6cLmTBXf@GInWI?doQjldo3tt#UQdi-o-P z*SMh%60g}+?R7P`xU1cumAr5c=p(xW-Nh0W8@_J6B)*WYroOh8oo2Z4^ZbCdRkc*Z zS)o7Ps#U_x5T{za2gy}azoOoUvF0hm{-GKzw76SZ*m~ipYggCTxHbKS3s~iIUENv_ zpXpvxPlKzuLSed6lY0eTJB8Lrz=ZYk@HZ~^vU~7Kxom$l*T~{An!MZq2MPHJ8gxyfT3zLOh8V;KiJT&q z0oH(6qr_DBUW-pgI<&H;Dr{nqn}*<6(P_PJ4r!O|Qk!MuyICu6Vy+cOy&lcmwXTnqu1?*AJpcrSip&vG!VW9Nw878 zfXvfUNb?yK68`p^W_xfcCb8ME)p%OzO=B)+C}^N&*lz{{B%Xe?J~uB~%~dtoB!jl# zge@yB;fru4$*T~$0C{WJ4OdIGV&1Is@nWinL)2&T0n}w4$0iYUu`+~%mHtLkkO90_P@Lgs@Vqz>3k_0Gc|ij1*n%j$z=2PdCxxrat^mOjyGspVPN;)X4| zgYKOtD9ts*eCS;Gx+k1!g{!Kjrp1j2i+vy1jjj;u zBv!#H#Ey;2NuNPqskut%(&ypm&*#Bvj*zRKLoT0ZC1KZin#fmyBaJt8fwnRDLKMUq zC~Efl8l+is7TQWDP0C2uUVLFoZLDo>tn$?r;MQg@z%%G+Db<$o~!V>%;ohB z^}e-*b@eqhZoD}%EHAabsiD5f?M)4qRe9Go!Hzvmo>p&aYZJ6plgeJni;6J*>XoT@ zp`wpp7zsf@2%)rs>IMW`dNIGGvbMT542S0vF)Y7%F{Et7OWMBbd#yM*!fnGh!SU7N z9hcyQ$rrYK@y?Tm#l6A}tMRyKdGo?MxpWE0^|!crCnLh}8UboU8(;RkZVWpc0cJj& z3HcH%6)l+Kt6fzsEAWN&xLh=&**dH7)=g}vYMU54&!&@l-Q*MDG2EbMxkO&g-BgX) zFFYIU>i=|i?J;syW&GURODPYtTM`}uAuCk`OJ{dxw$oO?^s!Sq_Q7^{8w#3Sc4wyD z!JS8EX4@@k?1H>B7}Q`uB-w%y4H_Ow0%|}TttA>G5{)&Qv=RmXP*Y8WL_+ZQ`_B1h z@7&JBw&4%L$?iSpeCPYV^SI~vecznBM@~+xS_PAoF4t0y$QDYLZ|*SaMZP9>$jRz- zU1q^1LJe#!8yxX&V%56K3=3qA6Rd+$L7XBgjFe<2d(so5of)`ulG&Z@j#5^5x?<(H zWgZQ|wp_A{k?f_Bjx8YyfSC|Wo#ETD!%8O5lUbQo;q}>Jk6xgg{AzOwtE*jG*!*%j zOUVq2iLZ4g;Pj6d(-&gLCa3POIli+!#!_Qx+KH}(>hPtDq`_)zqJM&0e?gflP4w@~=TAgQrj@*nS6k#nDl+b8 zb2|1~g8b5@{mFDYv4us-qR1x{w=1Sgu*amfD!UY!Y&#_sXD}<<6F#o>ZQ>T)Vj(dJ z5GKSOHh`u>@?cWHIk!^7>a4}&vD-xqfL&iN1AtV7eFd@?rXMaNM>Mz?3?8^BT z=1-3pDnwbj6o*kzE|=sD_nBf(LdHfGZTGvsXz zh6H`b}eB=5l8Aw%4<3 zrXBdUH|wKNv;N)w32Arxb3T~Op7cx5!&|kNZyoygv?p(tm~wpFu4; zq(0{#Cdvqo5uKInP0pbf4&4X&8O9a=Vc?VLIL12(u8{csUp^6S!r zOt4VGWbT6OSQ=hph){|0Lj^xx@_LZXt+@qe|N|7aF}+(}B&O0cSa1j`63u+cOs!y{A+0 z`D^4(lIuaQ~8n0p-l{bzK}_q%{! z?r@^sVZrY;y&tyF-?&8nKB-gr-{=BA3kF|{{fo__*(i4yo&o+Lz z1>OLh_5IS7mVeP@bCCG{Vx#xXYVL=-@cBy@_=T{D>{Ons0B62WTkAtpaT)M7FT!VC zc@P!H8zs*J{J3k+D;)f{UHHG&1;iwb3!FD%N&CD0_8R&<-5lVZ`2V{L`~tMkV$4^oXNBDKy76+gw3~%RpVNSI+!=?j zX?Fq6jn4!8^>rscIlzhEccU$%+(nPz7aY8Iz`}WF zKiyBe@c9GaeS*>c_)i!7b75-6dL!25)<{qbNIxEY1A zGMS*&I4*gDCg6p0daorwV}T1pL0 zS4u1ig<;T6GPen_3dxnS`KcV3q{|S<79lzbn|qKBIUZ#AIA-R`o66}_c2hZ%8pJcb zY6YK3JW|Uu_$o>|lU$BSl90g^zGRYFky=Fv@%UYoRjHMk!2zNWIyjKRhfxMrEGNt4 zN_iylnUyp?tCEE)jf{mO8@E6Jo*clTd%PU-0G-v^lp(oFK*v%rX!S;O8ecTb8;ItM zJ8hXE<-*Y%5>~v9LN(kuRh@utq5$nvBOITe!Lbnr5wN%^uw^=7gg9E4AZDzO??nSN z>wBTZfSflhOqa_vVTi=gmQX`RQCsq*FkC;fW^*>oZW#)p{R|o?`ruG_vnOeY52 z8-7o`Kj>_z;;V#Ivs0Nx;bO+hx6`;AFPU;e01^14E7d*O-O;)vV2B(RMQvl1B?I9G z$m~QQp1XClIanJn)pHwfEpb$grqI5l(AYU;H_T;5A!5!qVO^31yvQ$FK^mRA6|q6S z8-%uu4u;8<;pS?AW!za56BLX*Nq}y3$k{DPVnI?hX}C_=RJ}+}YSJX^R?HXDiA-{v zCeY*MKgnKA`Kcw$mPa;1b;x!()hR%Pur(xmV9_8SnrdrqTMo3_`=XJDlA=DPa(n{wL4}qO`N`E7CTrH_!ekda>I#5+Kl>j+h$gYY2{UD@MwEeAO*Ek8wYg5Mim{VQh*qH=*9$eWC<9W z%*=2VXjGYJb8ooY&d621%o1!>>djm^3-h|_SQyP9fpNg$zFbV=+6Re!YZ?0yvD|5N zBpE!*!)$ga#TMg?ho*rrmCMk0y$Q37Ql(Y5G-ntr5Ey5Xz9bW5rMQO{Oi=ZPuaN%wtmY+K#LW2C6)`?wC_N&<+cHl-~=R-{kzaDF>S>^ zjFV|LLz<(XCtFR@F4Mjw_nZR1kv zY2W1hXvo7nw+#(#fh7m#j&6#WU#an)S_>AYnhtA9auBtzz*eQTVwBtZVj{T`J&$Xo z9j#a}se6C78b30NI=hlcr)M^)HW>I5OK_ zRsveg(;5-5w8R9yyO?c%KW->Qr}#pbDc)LgRSF%JD!$M6&B`q6Ooz4b3t!|pYp0zZCWhix;^Cveqc{Fpgm>r2tUb;@4>UbwhX!*&q%V>vr z1I*Fv1_tHk+w1u5Oag`wfQhFs&_|i;69uCQVG#i@Oz(#!VVVn`)3?yqWoUHO~=ysxW!|g8q{vSbdl)kUe;;Vm*i4oW9!s>qu@hCln zs@6GQ@f?(rVR7m|jaZbvSLvM3E19BB>D2#0jQ-dXi>?0mJ|3l}ti0X*7}03{s<%i$)Os75&M2j2mVRaAQY?&6UOv2lM?to}-`{zXWS(wkW!Gp1&J z9p?_(%3tG`ftb8B|JAcL5Jp_z3q|2SWz zQ~YbX&^H|Y8y{0l>&NN&0lGMhn5C~heq5ZebHjvtBB6m zd=<>N&OHjFU*p6GM|~~b75Kjp|E+#cARN@Ht-dP&_ju^A4Lrla9dYse*}SnT3U==I MmgtcfK`d(i2hgPK3IG5A diff --git a/xxhash_z3_performance_test.cpp b/xxhash_z3_performance_test.cpp deleted file mode 100644 index c352edf3c..000000000 --- a/xxhash_z3_performance_test.cpp +++ /dev/null @@ -1,172 +0,0 @@ -#include -#include -#include -#include -#include -#include -#include - -// Include Z3's hash headers to test the actual implementation -#include "src/util/hash.h" - -// Test with both enabled and disabled xxHash to measure improvement -unsigned string_hash_original_reference(const char * str, unsigned length, unsigned init_value); - -// Performance test that measures Z3's actual hash function performance -class Z3HashPerformanceTest { -private: - std::vector test_data; - std::mt19937 rng; - -public: - Z3HashPerformanceTest() : rng(42) {} // Fixed seed for reproducibility - - void generate_z3_realistic_data() { - test_data.clear(); - - // Generate data that represents realistic Z3 usage patterns - - // 1. Variable names and identifiers (short strings) - for (int i = 0; i < 20000; ++i) { - std::string var = "var_" + std::to_string(i); - test_data.push_back(var); - } - - // 2. SMT-LIB expressions (medium strings) - for (int i = 0; i < 5000; ++i) { - std::string expr = "(assert (and (> x_" + std::to_string(i) + " 0) (< y_" + std::to_string(i) + " 10)))"; - test_data.push_back(expr); - } - - // 3. Larger formula fragments - for (int i = 0; i < 1000; ++i) { - std::string formula = "(assert (or "; - for (int j = 0; j < 10; ++j) { - formula += "(= term_" + std::to_string(i * 10 + j) + " value_" + std::to_string(j) + ") "; - } - formula += "))"; - test_data.push_back(formula); - } - - // 4. Hash table keys (various lengths) - std::uniform_int_distribution<> len_dist(8, 64); - std::uniform_int_distribution<> char_dist(97, 122); // lowercase letters - - for (int i = 0; i < 10000; ++i) { - int len = len_dist(rng); - std::string key; - key.reserve(len); - for (int j = 0; j < len; ++j) { - key.push_back(static_cast(char_dist(rng))); - } - test_data.push_back(key); - } - - std::cout << "Generated " << test_data.size() << " realistic Z3 hash test strings" << std::endl; - } - - double benchmark_z3_hash_performance(int iterations = 50) { - auto start = std::chrono::high_resolution_clock::now(); - - volatile unsigned result = 0; // Prevent optimization - for (int iter = 0; iter < iterations; ++iter) { - for (const auto& str : test_data) { - result += string_hash(str.c_str(), str.length(), 0); - } - } - - auto end = std::chrono::high_resolution_clock::now(); - auto duration = std::chrono::duration_cast(end - start); - - // Prevent dead code elimination - if (result == 0xDEADBEEF) std::cout << "Impossible"; - - return duration.count() / 1000.0; // Return milliseconds - } - - void run_comprehensive_performance_test() { - std::cout << "=== Z3 Hash Function Performance Analysis ===" << std::endl; - std::cout << "Testing with realistic Z3 workload patterns" << std::endl; - - generate_z3_realistic_data(); - - std::cout << "\n--- Performance Measurement (50 iterations) ---" << std::endl; - double z3_time = benchmark_z3_hash_performance(50); - - std::cout << std::fixed << std::setprecision(3); - std::cout << "Z3 Hash Function: " << z3_time << " ms" << std::endl; - - // Calculate throughput metrics - size_t total_chars = 0; - for (const auto& str : test_data) { - total_chars += str.length(); - } - - double chars_per_ms = (total_chars * 50) / z3_time; - double mb_per_sec = (chars_per_ms * 1000) / (1024 * 1024); - - std::cout << "Total characters processed: " << total_chars * 50 << std::endl; - std::cout << "Throughput: " << chars_per_ms << " chars/ms" << std::endl; - std::cout << "Throughput: " << mb_per_sec << " MB/sec" << std::endl; - - // Hash quality verification (basic collision test) - std::cout << "\n--- Hash Quality Verification ---" << std::endl; - verify_hash_quality(); - } - - void verify_hash_quality() { - std::unordered_map hash_counts; - int collisions = 0; - - for (const auto& str : test_data) { - unsigned hash_val = string_hash(str.c_str(), str.length(), 0); - hash_counts[hash_val]++; - if (hash_counts[hash_val] == 2) { - collisions++; - } - } - - double collision_rate = (100.0 * collisions) / test_data.size(); - std::cout << "Total strings: " << test_data.size() << std::endl; - std::cout << "Unique hashes: " << hash_counts.size() << std::endl; - std::cout << "Collisions: " << collisions << " (" << collision_rate << "%)" << std::endl; - - if (collision_rate < 5.0) { - std::cout << "✓ Hash quality: Good (< 5% collision rate)" << std::endl; - } else { - std::cout << "⚠ Hash quality: Needs attention (>= 5% collision rate)" << std::endl; - } - } -}; - -// Build configuration info -void print_build_info() { - std::cout << "=== Z3 Hash Function Build Configuration ===" << std::endl; - -#ifdef Z3_USE_XXHASH - #if Z3_USE_XXHASH - std::cout << "xxHash optimization: ENABLED" << std::endl; - #else - std::cout << "xxHash optimization: DISABLED" << std::endl; - #endif -#else - std::cout << "xxHash optimization: NOT DEFINED (using default)" << std::endl; -#endif - - std::cout << "Compiler optimizations: " << -#ifdef NDEBUG - "ENABLED (-DNDEBUG)" -#else - "DISABLED" -#endif - << std::endl; -} - -int main() { - print_build_info(); - - Z3HashPerformanceTest test; - test.run_comprehensive_performance_test(); - - return 0; -} \ No newline at end of file diff --git a/xxhash_z3_performance_test_orig b/xxhash_z3_performance_test_orig deleted file mode 100755 index 84a1e111ebf1188617de889c9f3e5885d1d6892f..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 58088 zcmeFa33yaR)<1l2FG#&O;mXM9J;QAEbku;Vf#qK=L$E~6cB!41KM{C~fyd%HUU{-g7J-}61+ z^VmFnPo1h$r%s(Zb?Q`g<#JVd#T<*OD(1(k%v6XSO_4dpMnUi;BLPsX6e#g{rYdJE zQNV2?PnH);fKvH+$o7CC++wCY^lX z;}p*j{Pj$Un=rDTXm5o<-w$TR%6t<>)}wB=H_Gzum-mG$jDBx5J7dU6b+O(7quv3d zo(U5TeVWkJC)w~@VDRk^Gf~Em3H#TpH|q6=WwM%LLbk!rqJR5q|C{!zjCx0FB%l89 zL7A&H;1ve0PnOyi&%{Wc-(grBL64J-3-YVQ0c3WlYdc?LVhvO(e|Kb9pK<)r`e%W5vqk1<9=`-r zW2*Ei{WGxB<=37ee;Wij9sM(B$e(itKDVIrr{m*110Nd{b2|DpXW+B`4E??H4D^G} z!2g~z$nQM^pUG!v_ntH4JI=u8&u5V5%`@od$usa@eg-~GXW(<<4Ecx8pohXU(D$C9 z-JxfY^Pgwn&-vlRxBut7Gw6-$%jxXoM`y@~_^0JRH>AqK zXoKbpv^!84sT6OJ8HsF=ACG5MQ%keQ=dW(_dpwHAy|~g->uvL{YVi5JZHp^sH?}l; z7gw)r^vbf+mt3&OpOxwH`0LwR)_NMf&8z(N9&cM)OIy{v8pU(L{6+qJkEdqcI+x3p zwX)jRP=f~B8k$$RYZm!kuA2JlHjlrpy20;r*OV`+#-qH@Q|YO0ZS^+SmV-wVnAA2_ ztsw-nyc#sr+>-4%FUytXTMtQ_JT;9iHLJ6mTh^AZ5kxJGzVe3uuI>Cbug}}I##=6% zYoRO+&B*e*o65@m5J8d zyseGZH4v!DPzKZnjY@s5tgiJ`H=_IKIFwxNS&7kW_S97SYw95otlc|x@j389x zcV)|QHmKc;J&Q9v<%{w>Rr3~Qdm3f?1(9-9x3yKT_cVJ=12Tp&yS3dfbr-2tS2naF z^eRM_V-5mvto8b<8yaDbRc#GTUZ}3V+E?#sZE0+%S?|h0wPvrk*2soJjWN!xYi#$` z3qH+j4Kw?1Y_4S{Omum(JA(b@izRXKX>-Wy8~sZ^XN)pHi3QY@INETl zXrxH3!soM0#lI+gvAl^7@dvS1nCn;7#Pu4nr;*1GW4K*Lc@^-ahK6_rZ9Q+~-Sm^2 z5$?q*uN(M-0*_I847`0r!vIEvp9AMd1?_K*GUBDjZ-FQd5wKE*dVwb>4g|2os|6mf zoMqtapS=(AX-c|@i}C@=Gy@M@l?Hy%irc`SyKgm8c4eu7Un1yj%1Q%o5V%#j#K8S& zKgAZrqHF-pkGVfG_az4>$oy_&|6}HFG4f+J$Z|8^#9z8f<})@CHnQxK64 z0}6eLBl6=yxr(AkcP2GM=??Js|Pt0!7q2Amb7b{Bdgh%moj44(~ zU(b@Bw|aYf>$V7-2N*qv!Z;5udUl0z9$54|5XN~>(Q{WA=K)2}Ps2D5CVH+3<2;b) zX$#{#i0D}v#(4nIvoMVFfTyQ4jPoF(Co7Ee0HSAH80W!5&!8~Q1BV_<80SGl&!;Ct z{pA5e&s$-f2Maxi!Z;5UdUl0z9whWU5XO0c&~sN9=fOeGPs2D540^5!<2)$nX$#}Y z#8-xK9vJj24C6c~=qU~3JRs=F3gbMW>KPZpdnf$kB1Nflj44yZ`1Vft=kmVzKl=*Y(3M?uVb(51-!;pVJSY z*$>a_hiCM|C-%e7>W2^QhbQ#Iqx#_|FYG&B$3nOscw_JJwLu;Q>zx}@eh*Wu)hF8~ zq{0N+WAwns!9T#xgD=1sLgT+=k$&|DJQdbE;!+f(w_^g=>YcKd9*}HY-9Zl~`rZ>C zckBDhQpBMf6Umdndhdy=Y$=a0wS&$<54`OdvjGXD4(L0BXX&m3dPBE25Z%}nXVC){ z&n4@$e`Ct65SAIiwOOqAM(_>DacVE(^sD!52dS(3!i#nXHS|O{ zwZPt-9IbbbO3^#7KOmg1o`qN?5-+@{Wclv82z_ljp<(v&QhR zg)qUN0Pf%!DY&hhCb_-FvQGQN({Y;};$n7uhn;@0){x+h82DZ?#C+5P7pu(P4fJJDCGq^yoglfBn{4eS~#^n#ZGxfrQ zj*YRf1rYTfbUb#n=UYyQ@L<7iSpPU1=oIyvPN|<9SziNkYW?lu`st_CpB7m^9Z2vI z_Q13c+I!&W?mjqe)*bjp?`%O>GDa_a%|A6%u6It?yJjcqh5P;SdM6THt!glu0(9(l zg0%g0H?4NlEB+zwPJar_>Y*qf<$CGADA5_Gb>^NNG|{_-F*01pe;+5VDV__2R5 zM^WGTuJyu;dKQD0@su3ce*Irsa$d<2F>?c7K(5q^&b2}lk3oI>SS#RE(q4j3vFn9L z9UGU@F9v$t=tbJUDhfYyY0zG=yqQr{8VRBaAJd)98_#uBFQ*dbo zO>vCg(e2bbc3~h6VD_=(1t$kLXB?!61{WX(Tc8fptaWH6@gf+1?|u3U013dz39tLU{`!>Kl*YNdbO$7 z-;KT`mTw-2OpE_7f!;F5!;1?})|Ceq7oI%wn~*)b(>|(DKiRYMMDx>o-u`6VPL=jI z+}+tu%N46A%r`g@-P?Pj#gd0$H_Ci-qql+}{TKM{&<9a3)(SIxQ7}=#s$E`JEM(b+pnH^)YLmvveK$I1fHWu0YN-;@Q)^1q?6^t5BC zDeFuO^p*z(mUS*J_=Xz)rY8e6K<;?BEbC+)sZR>(xm=jGn+;*MR5<2haC=27zhq%o z(f{ONZs&Yqh86o6PYnTDx#^wu1if=cO7KNsLCdk;-ipAQ@zuLcwz$Ny-FXj ztK+b$Kl{F({gV~g(CA;jG~tc=V}7B#4(frD<9gwV_T78ly5juwPa!@N6Fx!Wagw;Z zHmpOu#LUs}Aam~%A0ONE=85JPnR6(jb=c3|*IseQ?0w-Cl@n+0w?}sF{la%p-TTGI zfdj{3li$9wd+*=B?gre2yzadxuPQmL7w&97;O-P{xH}Ww`!{SrYy4dOmXLe`k{k2^ zkkjabJ9|sNF1Q1tI`psdrvSj_}%F>qRZ_5^LRhSCxv$Vz(an8H+9iYklYY zTHuiG+NB2$Vzxw2*l^yIUkdG@=q<<9Zz;;YkImxXAe1nU3a+N`rR(RMq zwJdPhb?D2NO1}KOB=ADvv%a&!I%2agLAVfkuvYt}Oh(pHUHb`?Sk*{io0smS;DYXZjAT6)O|jU#mU@a^|Uj4P>Y`9*>ulAMTTkhC)tQg;tj(t|WW1o$!Ez>(MPjT*GXu`b<+YAnYNPE9+ z88R9>3&7F25>BX;Fx@L*?iCUi{Txv5yk1m>k>8Y31upQ&L+&8K$*b;2X=TRAtL{$O zA`|zf+%FT4rW}=t2U89*@fB(hfYRi8QxzcrX4K{e1wrL z3w)|}cdb($+cw&&P}Q;R(HVrrn`aCx={m2sq~jyYX4}B4Pf`PGAG-Ra(8_h|p&?A1 z5{4%1dD-T)lI=G19&4fNkn32m{u7Kx*Yzn*@WNt-LA^dDQKYfxRHW4FT{;4+CmkCf z$H9soxXCE2Lg`ILr7BdqDJ7Ye0x|oF6T#U=qQ{d zgi3UGUKQh>epRAlYmt0qH4BoE3qVGKer7(=nHej3d943^z7H^#~4q{wBE z*K9^~h|L`P7_(;g)n7a3Lu;G13qLMdxn6NUjxv5`(Z-5taQ6$-C`&0I(rq9sdj1DW zE9ojr$=qxark9PLv0p2s{ZY9E!mMCtQriIYUW=qNTLDXbd{3gsi+8ulU;YZT+4ztKG zy@MhxOivG)-XQ84CMFA|>B&mc^!VpUrmYG43&bEc(kE|B5hWeRV;t8$jB_)ND0%GQ z86mb|P6#7*qKIIEQ$Li_D70fknxmxa6w)BFHztCMHVSEEp_E2elF}SUB|{2YrXY)$ z2$>a~8&gPQ+PJ$5!8bzljrZfIlM_VPa$uicczp`_`o`(lyuh##+<(KiF(HI;7yiT1 zvCU3l_My8KY2Do8U2`W64B1i9F1OibDXGDQAE0xc6?A`cif4*mV#j23s>z#?*|Ko2JhO#H))2SW9KTmFe%BBJFo|3 z5-x5YW{A6Ej&yM>uPA&^I?=5prijU4PVcrEF^Xg3k1>p5iJT`ASR!A>>SDSmN{8_& z?(3%luhLajHoQX@bS96*?gc-1Uo4bGpW`eq@Df~;{YMyK_s$O{NKX}i8Bi{SKLadT z{W)R-xn86l#o8r&&!cj&{I;d&88Cq}!i)rKB(9e}$XpST^Qc@$LAzVhJ}Mm-G7gy; z_oMRv#Y-8%!L_A06qwy*OX<=>UdplU`nW38-h7Tqmp;I8V+x2KLk^4>em(5bBRzIc zk5EDSCutBGf()P_-?rqAm2h;SgcHsMH2tw~xoj%3Pw5Ltd7`Cg72(ONFzAxv4$~>$ zZEEITQ!|eWr`&TjPdFfAL@e_dMj6Iq1T4gSLZmk-8+T-H#NJZfN;M<%;fadDtb#9IhZ*lp#9y?3=1IwcnslN#NC<%Mf}9fqQOe5E3{cCZp-AxhhI${la@3UpniqR;)cT(Bv}I zsmJJrpE@?a1%`B&nP@@pJd?A|jC9sL^I9%pdKGZ%jXHpp?)a7YnXpm*%IbiAuNHaf6hb!P;`bvsE!j3 z$F*%Z%c|&Ho>E^?__||L6|f$U$XW~^+^6ZT@7MG%VGE(Aw*X;p^u8?Xz8}j+VSpi) z_t6@Av9CJ}^$6YUg(kj-ZWizq&(uw+(dT7-1^njwvAi;}&zAss%mD^H7Nkl7pSTW{ zbi8>y@M6cVn2JtYVP(KJt*r3LwvT95^%Y&VVY>Qc&lqg!PD?vO&{lTYl1P?>Rphi} zVV0RD%eiM_8K%`u+Gfyp&CaCx-wX@<4^1pHt8v$=_wK9^UM}!y#|fOOT_bdNY-b-! zJ+|{yLwys5`U#vvXfWOpKMVAAn6Q+v!yNn$Em=;qo`cv9mWX-!7*=VeXD@b0Vp-_< z8BRk>0tcw~!_Yg;e3?*w+|0^A-1M@-U2Q#3=wR$l#4ph1)W#2CRp1n{$|ELY;Ra-K z&c_(%jp%NS{zz)IkAK$YvXrHnXsilhWNJ&BlT}(74{c1j9>q#e6DBS8 z$5($Hgv4TXuLyi>23h69u{qptm4*6n98>SJNu+%Ev0(Ds*n+$auV+7NJcN;ZPoVKr zfdUSh3n&)*(HF^_3GIN`&DcCD?!=r35lxN^n@v z$dLFYq|KJiAU0x`p>vl(8ZL0h0YkftFRjcp_XlE^aTw)tmw_-DyNn0LM&v=U`_Q?| z_)IJ~`$C7Kv&_v#>i{yl9NVX(Z=gdsXcKF(I2gxixv>)Kofh#UK%?lBvCwyxVr|=K z93k*WhmFP&Lae^Ol*6X%E5%VlAFYZrhK}Q^=eiH_R&-sS(u&jK;JdF=2;&4qI56`_LTsoI2M23} zod4HTi(-RBj{j+QC!-A#X`~EU&4#*#PSDU-hAdl(~c7@>7UDz zyUkONJIqs$du4$A8^|YqkCP!-S8R0 zc>8XldqyJ=44>CBqUjefWMj5|j~FBe{6fp#*<>E(j^9&Yvtq2xV2!_*a}~=J!P)>| zJ;`{OzsH^?!ulG6|2^cHPfeOJQ3;Sf@{s?Ez5xqkO zqffsKoBldZ9I@$NjGEl(`>~8;n_o-Q>X^-KK70u07UF#4v~&aKCVj@#SMYNg0*P1@ zR~03mjTL{>Q;b=G^Y_VQMg{eK`Y!^($LLFU6yp(`AvP8`1?Ghsx;1_fM9?oOdd*R? zS|)xP^yh&SeJMi_&ognqDuvHcx_>pokuQeJq{vGG+g zLlBJaxD*XMR*gq+`@1x`dj%nW3o*R4$`ZCi(gM?fJmA@FJ|Cib8@D>^Q1la;ET9w zgLr_nD{!BZ7XbqMgYh7DcjCqouG+Xe@30A1xak$g#-||RhRX^R{{+WlzS&1+oBmIz zaWSR~tS>Rxj9J=K4zbwuvuHx^wBnY{+}E&}3Bin8Hk+P6%lPFt__u$Oc0Y}jKa7Pg zOF1_Eiz>N#4}VL$(EP3bqMmrc^AzHHN!(R*F-}*5JIL}>egR1`og}xMo`hRta7iYK z|MVoh(*%+)pfM551S>=b-jLUYCb8$IHk}|Vb)!;n)am&i5hGFbOOl*;;j~;12ofVG z?J8;msXPmL;`H>l8uSMx>r#V0Irxjy(YH4S&lRG2S zMucjvXU#4{QE>S1zX-y}(<68y6eqIKKtw;v4Wu|YU8MS1n16GR8)Iv>^;a{|z=SY( zBd2Fgn5^eGynvbin{ZlmxaU{>Gad?O9GPZRlcYDGgnbZWar^V9vyP4LfTriSco?JM zKRwysNOmP2=KN(t;_eiFoW})$&&0K^j*~bZI7GV%9CZht#}8*S9Gl((UePt>3jj>r zkAn|9$Hw00iQIm8kKjV$T}v``-o@Epo=7?!mz0*_zGy{PW#W+`B3|qqrU&pFCs@a@ zbehgX8oe{Gvm{3U@-ugr?RnlO+SJ?r02@@!b1*(xWjTTP~jT`<*C6kG-V7Djj3I<{6??~FdR-|{TKQbx6@pQ zcuNo3`WiY;EbGju=$wn&p`lyCh-jdwK+ydqf{f^ju9O!jySI}1b*T|Rd?ZY?bC5?3X=BM+?@mUuF^Q%m++s> zYhJvJnk23=J2o8ybKHay7gBi>idX8&aN&jH7X0V4G_pm>de>#nN8r6MT6^{VfCyqb zqx4Q+%>Htox+no&?3~Vk zm&f%q&|TtIF{U(cA))WI1Wo_a7h`rm%%y#YxV{)z4Vx$zmx<#$i_vpZ>wzh_SvEV- z4Ka>v6_*cjuY=<`!yV`qR|-2mz*cz- zFLU%6EFJfNyZC!JuW$<$A>pJ>n3F0Ja6XAZU~C&^F}J`hE@q;l@Q7pMD8$9MVyJgD z;+993KP4{080CDK4sGK~@L#ZgR?vJt2G_XY-B4JskrBKFNJoLiaZ@+1jX1V-m#BMq zd1Tk#e=U8d5|X<+qxbB*aMIIzKRZ8u5=I!8a@;$=wL3OnfxXk-XP17sXXkU1_U`@c z;)4hy&c{!_B8)+3a4y0bXh?{MOLtek5Iph>XTjPS_vCyQFqWui7JiJyq(<0K+4*SH zQFM<_SgRAzCPC>9P)MK&)Q?q#4t zc}$wdFwJY=Y{pBKoezq5sdCdX$Hw1LmgL z9_pe+e+ut!%c_fwCZ8t6F-&4GORNw$H3>}($EFX!1WsX@d9|wl^+?3GQ>0uKnvg5_ zD*1KVC!9v4O--ENh+QLF_%T}$op}p2>$Zf9;Wt3t@GV_KhQo*Ui555R7VFxVGRWEn zBy<_c&A=j{Z1f} z?Hl#qewy;L{`sfWkBzMVE%rT;^@AlH|5o=tvGkb!Y_MWLaL=1hP3qqJ^|J1sCJ;hD z!M&d>eF83`XD;x*>TI7SWxoY&_bZtoORivvbcLmK&wWP2UmA=*wdN67bM~nv@Ufh> zX(%z>=WjTFZbgQvPt$)^bmb1j52Er~HZNLte2^@TvS8C2a4?B+4{m*m64`s;ERFq! za2&YNi;EsO2;+XkvGElu+W{HTWMcEP1J0UUXBb?+Ax)>9zmJ|GV_b+UU+rpeEqN3-+?3!uPe@6Zqkix` zAaMU;#dHVuN4WSc?#?E7=Zh4*@Q8mr;ssm?6#kx$Jjfp!v24ew2kG;9TmNuL@6+v1 z1#c$z9nXBZ=+0&|~chu0{uUkQPk+V2aD09HBjw5Su@^DLwK}OkM)1{F9B7@Q~)8m~1;B zwUvQdZv171yR#CN$HHi-ge1|F z7?&xcsZ+}m_OE&}V7$=!sfL}h?z*{Wqv`?OZZa{8mDm;5Xg|w90 zf1x?op5G_cQ^8stdy+BV!i!ALwZ~ZcM(|F-lSc+gaL0Xp_&4Iv#@K0pERkSSr~>_O zWCec!45i1uT*R3l2a5$U)Z8`Xp?=hkjq#F5)=&iUMld17e&Z<>`1hruCcF{}zQ%5f zGmk~5RCorfK&ZklfqWdiS5y!(jXkBtoAmhR-y%IPkT-&thMG7Ej~Cfx$HvPeb<|?$ z$Q`Qi_$d{>zzJ4Jrl3Gx;zYt)#JMCFqCcW#^IXXXpU2UEXD>FA_n?KnCzf`*Ug^0G zG(iVi3NLM;zaLyu68Nkl@UL^aa>nqc^y0FvyZ*fDyrGLqI=;qjhzDR+f#)i^&O2Jx zbxms7c>J~7@v^QTuYK~!CJ-*T_CPh`;D$tIVCE;5sk?UWiZ5%}_2>2ZcQ#agE(p~p zMc$J#?>O_+myy-*vdsBLQoSXp-eR7+aF_27?v5k)abl^8)<1D~yp7${p&f~k$IU;P za+K~WdA7S`=g#PzyW`5$10_43PSDl;W$Nw{_0@{5xwbO(&5FW(ZFv=eU7>iQq4b-g zKRvJue*|Mw59~bPXgDzS$n$68?|6Lw*1P6>qr+8q9R3D>Q3Q|wrEj!jTQn|?s14mz z2r6`I4F@QlUU;(o?Z5$?eC-T6E^-}c=w=53yLP@G?>gAf%_fK>;u6068)Ug}H~$J9 zUHIYi|B438H&hlC6*(`+cItRVt8-3!bB({DrP*29-q2Xx@~Je`uTV}tj}5P_j{W~!>Kci&QO>2Pb+_wx2>+Ft*N@X#_KG>8%@{y z8hlRKfyEFOf;!hW`0M-jWo=8_>c*DpT4yWUZfo|Dy%L+Ap6-m~SLv zttc;3X16r8HZ*$MoRQ_eX-=hlz94X>rkBkxD=%F#H%(dNt?{?CO`GQ7i;BgYh>e#6 zD{Js#XC>9RWRhCljFFh>T<1|D-vK>sntac*;>=9rK&|&EPFH4HTAGqtgu!iV0=}lY zvEA!Y(wxd%Z!@bGV5(QSimDb=NC&PNy6eA4gCI@GC%yx%*=FUW@Tn)=49q(=4Iw*7GxH>GWq&! zSGFt1mFvoL<+}=8g;|++19nzcc2-VSZdP7aepW$NVRmM=D?2MYJ3A*kH#;voKf55i zFefv|m6Mf|os*N3o0FH5pHq-in46jF%FW8n&dtfq&CScr&n?I;%*)Jk+R()*iOJyz@v}%_TG;O+u7aQdpV%8 z6I(@qqkxN1e*doC-pznp_Vo4^18xO;5HJyID0kdj0U3X7L3FqUup1%u-GG@`uDb!9 z2n?KvJrBPRet^Xv^!DBac=W^G-d6!LKkMzyM7zcKRqr6%$0tbwMZI*PqOMC+N5)0R zY(ZPhXK0)XStpXFESd|Rc=s#*v`s1gYj5vi&?yOta}tuzacFB}HYl@36i&)c8Am$S z$IBFypRFFN7uM;|bk^IXO60c>Q4r^6{)AB{Epe;#= zS)?gBC{{r84)pG2dQM;dmIaa;oabnvMx5o_$1?d6zL?y_RY+w zNJ#9kTo{`WvtHv^#i7Z1lpSRm7~R0OyV&;iwsR6vuVvdEQLK;({f8Q>)GYJ+WzEy{ zzBFPiZIlQ6x8u%;?PDN9Z?og0s&2I2VC%A9AJq|UJ#SC)sppOF_4Y0T zv|T54(nYzhrwv?dD@#c2u+tEpkRo81qzWoEr404gq2ArW-rjpyzed)N?APp2zs^Z0 zwgh5@DkFP0S5vCMryKR-Fs}*_*V?9@IyU8f$EGY{i)#Jk^n+8yzUla0j&VNz5&ldN zJEe%RcAs{vtE_Q0jCI*5V_mLso~(dKcVJFFi?r=m5H`{#Z*^8A96Z}{7YuW@Fw7E- z_IMNO6rc_dNNnp-2Sgp#YmqB$k!Q~JpZE5zM3LlI86Q=8J^ldDW=&HuN+iUm_x7>s zu&Y)39ntDG%e$!bNVNT#Xywgl=!#YOK`-~HZ(HrX)0JP^?Z>7ougBPrPg6b^VE=Hs z@`Pr;db+YF&c1nuvcX~h#|-7`B+}eEgy~~LS^Cmg``>0LFORdoI79hkiv6$Cl=~;x z@13DMG||3whI0KR=KM9obrU#b{#t!vnzAR`4&?7ScBFrmi@DyF$K-8!cn8H#^2z4G zd{%lfpKN;b$>uu#jC@}KD;_GKG}jce?FR}e<&%YflD+A@eYiTX@I7^_MSa*}f7GJ< z!xHK#`kDBU3iN%oDu}XNcr>Bavhfn=uMsA;!---si!`%-@WkYWOkb7HcYSoF|Hp**=y+@iFOeQX={X zJ&P=y7YV%HP$c4RftzyT?|ucIWRxSc>r-y9|9=da|6f{vhM7*8Q*6L01FkS&s{uC{ zaEk%A8t{Gtb{p`Z0S_DSr~#F+iufcN&}qO-0~Q;w%77~j*lNHH2Hax6tp>c`fZYZ> zXu!h;JZeDM`geaKD(>^a|KTysnYv_Ud$YgY>B`3cw2_&f*DlbkE3!ClzA%t{^gF?iYbBj28uL?vh<1bv01@{BI)eGr zW77G4AlvWQ-@Rj*6-@=&%0V9$Jvf<#xm0oNpcJIF#mu-Kg)zypbGM>q%y8MECm>nO z2-%6-Ni$LiKJNFhlEeX8%->Mi`Z#($ATf^I6l*2AI$+3|a)=rnZYYzpu^a#E>D ztCBGT?b{x-I^INH^t*V>;8=Wxgc^D%(fnWQ(uo(%#DAotII>jj12koc?a*34Zi(Hf z-6PFkuudn2mzBz~EvQFkuwTt3*LJ@U<*p!YG(qh=OU* z$rctcVH6bc>If(FJuDD2TS`?>je@&Sz|cWuLP@M`Sfj)~^f{^VJ!}@pQcGO1cGDpA zKCVm45%5N>4C}EaZi{xIfIrdJ3iwm)76E^z{YAi=v}XkTxpqXro3&`H`Lf z;Qweh33!k8h=BKMuM7Am&5F3e5_i9LmVggvGX?yMcCmmDYU>4jNV`eEZQ6YTKCC?{ z;CAib0zRVs8F7RqZilvCz`ttm3HYcMjX28^_c!fq0Uy&A3i!CzB;Zc%1_5_#e-Lnw z_N0J&wT}hdrzIf{v&8M!as)h}%@gnmtx>=ywd)0ZO1oFUr?saA{JZwHfd9~X4S3c_ z@_9xpGT?Fn4{Dbg@HPRT)gCe6O9CF!zBJ&dQLyGXO&wYy5^?I#i$o$`9eRyOj8qfY zm$ zkGukIETJfV96Z>ptLV}asgkb`<>DEL5hxhq+#V40Zp4yhlR$B_E)HgdfFUj$$%+79}sTbTGYsG8=1q z7XtMl@8eJ{k?%i(wTw%C9KKS7c^eW$3B#RV{Z{4sY zEJ>V%9+t6@gm>+K#`p-%l0C{xN06?3HW{58QvnrFBPuhMj7Ok*M}a!}O*B2{Es$uH zD6}MeHX;^qIJ8PwT@wrL!yDRt?|QdL(>Cy zTZbeqL1Iu@ypl8ziNRCjM=~S+C-KqXKjb-(Ctfx5Lo_&K0a{PIT&B;Ie*hMel$j*x z&yZGz@#4VXLQA}B6nZuIHd~TqNUoL+eOZR&X+CT?EJO0O8vv8w#FU{~@kw7m?ZYxP zOY%ysfDSUbMk~Obe@n7gn=fFUwnD&F8vi!Xl3cHK3D}_BE#Qwd{*8bodA0VefQ{Ox z0yb%boXo#O%Mh?lTO^=g^9$In{anB`+BN~#X@3`Rz4nfPS87KE?9eP@$!DXMEZ`*2w0#U8^`iO%|bq-rfCTRPS-{V zSft%7%4ceK2{=pplYqq&jsHqtsMBUt(bym zjZov2sI!r>y>5xCSKylwZK!-G(J^?s;~kh{wzn;V2uZ*gPZHQa!tjh4E&>z=De5s4 zBlxt%VbVl>jY8X-s>(Wy17&HHf+4iMtBNRuVWG^nKa3T@nIv33gT!z=s%D_Rd@z(% z&S6+%J8Vs80m3*^G$0=Mp9S%;*{un)LCM(CXwwDewzsT~dr-_!Q#3B)ps0})bD~Z3 zo#CgbBHB~z2QcTywhJVMMdHCu%JS$mWDc;|KT_e{n2!3j70l8kGsdp{YYex6qwPs6 z<5|&H*|7|=6up}_h}!h#aPoO*qQI$@a>K835Bj!|=I3P1GMzV7uKa6ven&5GeLR zNRGWx^h0MZ+f+p=0~M5Lz7x-`W6;Mg5RKJ`h^R58!izQ?OI1yV;!kUDBhwQ5s)4_! z$zVWu4)Wf zl6IrUxCvV2U>Iz)jruHd#SB6VX?Di%X{C6oX$#n-qR~0cKL?MZ+|+$2C7s2pL}hYF z-nE{^rYUVi(@}XW`%o2G?15C8;|R^*qoHpBP)_!#zrG!RKufmI#{3$9+dcNTKaKqa zRA{?Afm;WD!{snb7(6t;8V}o5N!)et8%dF9i$=FCkV|^ZwXm`Qlh;k!D$bAnXw>gB|)etf^BIKUMGJaZ| z*d&gh9w#=5<7dQ)P2%{XII&3_KPygb&H%ZUu>guq2cg{JC*rvp9ZH z9F5vCesNqS;DR@ytmG7hTch!pp!;I3jsIV0fGOMfu^?i288iMptoKaezf?VpT1sL%`gGrE6kHW#Rdr(uczK`cbM>JifVx5hdIx)#! z33~h|ts_A;afr2;*l48Bjv7LiV)JGTLPe?e;eSTPxEIm*OKGkc1|8PP81}SmgJCxM zl9o4sGc(4z1ffz|zCaSKH^MyA3IvjD{Ti~R6$->@-2o+~O%q6}bt&Xcn=X({YZ~T6 z+6;jdSa(3+v?75NTbITFDHe!s{TQO9l?bHD`Z(Ju705E{OvsT|HuMVwO)IQzlx-48jtYSS>K{Km4iM;+Z(Kx!G_c3J9s2@jdec7 zSrF3;ZXMP~Sm#^^?)NI2t5Uq-ZfDQFo!8 z$xBt0R>V!Uu}WahJoYk_P1!CGZslbWUHAwk{$&`& z$#$U>kjj>WD|4C*?{R1{Pd8H~Ai6+v7)=-tG5`7c8 z9(5hHRiZkmVjdOrTRbIc)N1l7QpGZKAF23IqPJ3czlD%fz7@^EBl#te%7s4U}=geX(&gUNi0&=LsVdmcq*g%^Ekzkd;R$VOb@S-33)o*(*44?=Q=RIPt460VcOt<1PlIBs_A7 zD7PoEJ0FOV;3HRIn;w~qD(`KEvtnFRb`$MeJ`Hp`kR!3 z^ynC-t?z+j`T)bbj>IyU9xD)=m48u{t_dW@Iu|mf#|b3P`g`;^JzgM*)>w>DdV)Zb ztXH#+bpFZK2hd=8q9_?1gX|EHaf&{3`nLTwg+|xEM)SR zqANVW65UknD^P1ngXkBJv%-22W24xALJe#ZD&;X(SUE;{G3(D4)p-2XzkXB~Z6r!g z?Mf1Gl~F}Xs8P;uj;uY4^ZO+sAWzQ1O({|F=+5Mysv?LDgvyvwq8W5Y@fW$tx2Pi0 z;W3-6EC}r5SoY~a((&XiLPSv>e;XQ~{JA>tCxFx*kLAMkg?TISX>==Jsw13$41sxO z*PqDF9!>t0=mF32B3fdJ61AEwT_m?WJmeD-T#1UK?;R;!7SH^`JvWrRiAqcs?06Q~ zpRau_)|4q@MK;d}Pbp{YKP5+G^XyQTi`gdRvX^rM$0w zHqS4^eNr6xw8=fA30RxQnvrdb;$6cCSevJvk!>HPwtGesur?1tBik0m?+qhhZJv!r zv>orG9Sl-O6S6wbOv8=K@sdP|>M#gv$++)Zrv1tClgd0J#JB-D!vxIuot;sEH%d7SCdG*MaU2YCL(yD7n#4 z@E=tN1OLQCWzlF*SszrbWR$r07LX25E%g|Djpu^{5~FVf{Qx!b36@wA&qccfY>9c` z70olfXdd0>@v$U^c%H~y2%kJ|G%Bvh$d2KGn6(>P$&eAIV%-NFX2=LL#_C7ijF}<~ zOtjuYvNC}rTQ4D5xj>xOM_DpQAgR_}ESW2iOlvC{=mIIQJ_!TJa0{f^nvR7i;~atL z)~7MJ8S`SkhU8V&gG4F>a;|j+k@*5yXnmCossysg%6nrO3k9;+>SM`bfh@7U0QF^D zD3J54JE6mjb@cnnZxyn{Q37{#^;YRpWqvhvbrG1zI76DFNN|D%tRKX()2 zr$a{0;-^Do22nEUD7Zu?A$Jlkd@9jrAteZTz9|R?E4Eh1;94?>B8YR(XzoXbzXx$$ z%dI^4RNZ(e_G`ewwOuScJO-7yQSlgU*Tph~<*BHV{V9ZVt&rI~BsF+wm_Du#1P>mW z8pJKINY^YG>hc8D$mS~uT}6_|hi10QloHJj*nft4S$o6+#)DS5lGUTwV9-v!F=_(k z&maL;UpYSZSE2u`XT;23#3Jq)1STJ%%Td$W3x{Oj@58`o;Sr3BOOqo0oCK^V534AL z66K@_vn9cwLj+7I(Pf~G$|J!*>%hB^^LLX#iQ?<&Y93zEe>20>xt zuR;aGB8a3yx4C0EeH!o4ByH$555aW4&To7 zAP7`AYB(>1i;K^NV}{?v^j3^qp>qUZ+hhAZ`HUU0hiTZ2QaEk|FF4y&4B@n?L%Ex_ zK_+FIYw%qFwluUgElZ~PpXE)%k$n$o!S$bHR`x+bxB!n|9&Q&ygND45OIxb8w!H7qp{~_FqEq=?g@l$ir`SF*3zN zvHu9|PhaF<&H)zjp+xiO+`a*QnO-4^-ewUWN;E0${LO9pgTk_SYA!>5`&G={E^?Dn zkjsY>y@D00F?iEA4JLOUtIHxgf1I2i5V<^Dm$^~bp^MWuNJFn?ws_QomlDmh_))__ zFk#a;Md9C{jXE3HL}L8Avr)Og&L+k`JR3C|SSm68Y1^oCfu)Ih_!G8)4?x=kALHXm zKK{waTYP-P$5(iqpNHLn+7|n%MIK=Fzr>{8@m`vuT!24}0@ZjrHYi@)Kg@pt=G5lm zk=5DA8jEj!4m#Ub%B&KgMfgr;_30NOg^vp1ly+xK!X!mmjARwQF;*ZANYoJd64aZJ zxEkLJNj+!;ivNJb%|yln`2va0h-3gsMpNGaS^rT8XLP9fhWU>$5r z%4gP!O=kmRrl0{K-%mlZg%v5El zTzi4-#@CR`tQ9*QIqosb(SXp`^B_6Iib5_i^p=YyYs(zK%2C&uq;G)iwbPT@&n0R0 z112d?jf1Brjag38b6zt^zW^CumMaCAOxrUB&{mOjrI1sxD$2puc1)0c5EAR&Kvy@ z8{`Bj0?BmNp+fn-8@`M{5&c?VD)tKGEFUGvH=y)NlbpMp0Lk&0!b=Hx1L?}t7O-+I zhj&-=vgiRPGOrKD>y*FS;Nz27$;x4x&G^gXj3NV)w6FGUmJ^29wA~;t8)exP9StX&Ib`$ zA>GULH_!yqBIHu=w-)Zfz+;qY+H|c@O9q19f~^S>bq_9pdTc`@GT@3c)LFyB6f=ga zs1y~-v=?gb!7?-2p=e`c*g%Y3aSgT%d$<(maRX8mO`EA%Art=+^bSZg?cV2&~uwFc#c+iy7m^_>WDQJ{Dub@lVN6`VKgZ z4oo98FcEct+oVQV>1UAYC7RZrFH~-J!7%%R@R$mtDIBOyNEobH$BZ1q5lzI*m}bn3 z82CC&9q^nn#L!|91BRKf5=x3zIZ(4K{YI`hWL{!U%otu{D5Rus0ZmzIs^7a}g_^nqma<%f?^-g90$;>Kk&7ewxCc8mI#s0$D~lcHKi6=zQ`N5%;t7B# zGGj~}77|6rw*lYl@qGy2UHBfsw-;Z=;idR4$G06{i#o>Qm^l_Ds(5rUZz~=+l*B^u z08wri?c8YE|4#H3rar_Y>I*!gdzp&DLKHO!kLYoD#AFc7CpwRhWkk94ieAl>503$t zF~vYN>c@OA9*w#UkLY`udXNtWYf+5PER4P^6v*;#q@tOMI);>@V(qiX@)5^JG9P34 z7{LecTHB`LVJRS5MwBwvP}Q^OEfIqpbPJvbqo02SokVeirfv zM9s4g60qH#6lGnn+6T=>X8T|x_fPit!RSw;;AFGdRcnK4w+@L?ZEVCkgpDPOdiKHg z0>xreqpZVJyQ9fIhKP0jIra(Gh8Z((@y=qiuqd9)ldV7cJ{*UulARySR)v@$*I-uv zeVC1mVCKy*B|~m})GA6=_kEa+j$l?3k_@?!%$`IQ3>He+!sj)7e2P9)pEKi}8TJ&Q z7VB6Q86M&TqKG70FQx!OuLIANn2xGeQpY1r~YqJJUWyx5w9^(z&Qa2~}&Rtd!ue+b^~!qI0VC1tr6tX#L|=GejEQN7@O=r-D7$ zp$XCrSawR5J?a9GB%<20N`^&+?^)%=dsEgZ?f45QPhGXo@5=M|6_2OZyRv;1pvZ5; zD@^=(IVf0L<6BqP)}-)F8rfOMxYE0>#)}t{v^0AdBzt`IEp7gl?RARJ>t93YUFWT7 zXSvd}8t*OfDyv#OEp>G$Ry-HXU*vb?dOUr2xU&18Ili^kt>p_BWqK6fdY>PEw&ic~ ztgo$JuXx-GJZQn=ZLTG&LXT%vbGxTz-MTCn<*%!5Z}fW_TWVH&T3Z?$YSx#dJ7}5R zyI_$&8~4>382<5e&eZfzUh^&-VHMN>R=ZC-Di*XQ9oaloKYU)ha$|5+t9YgU#= zjF=c02;J-#BN7rnBz;YLo2RCwvAwAoV`&iv#GjmHD0>HL1_|$f+A?69q$DqT|-kV)D$^5)O-25b>P-iz0QMI{;X>DNL9iB zg`tUF)Ou?g{p(x3sm<+;jj*gVR0!K*0lHumurr>PR-Z6Q=2P=x)cs0(GpxIYMqASg zdw~-0SBenF<${QKsgH-RBdVHL^P?a26{l8IsrD<4H7%GM=(ry*u))|hR^yFDVCQRX zmPUj>N22k;oR9*Ak%Gw>Da;`w)u;$7X$;ecd8|{KR>FeT)}SqnqbsYx+1~7fYP_{5 z5d~B*CJ`EMUD>u8T))Er&dw<>YgX#;k|MuS2UXxzIzl})El}?oDvsOh$Z_RcjzWX$ za)pNox@f^$ki^3j&B?!-l*2+oY8J+u-{$q>tvhSOru`ixEoa9tr^HPD&oclWTR@LM zr`7DCqAPelb5_ZPjfx za8~G#uX>GiGvri<*C2Un8&);=G1g+r2>(!n7TUaRZNhrtsO#1?)Orp5MG9E$_gvE6 z0H5hy*TBIwT%j~wrP;d*ubo0`RJj6I*3v2rNWATdx@KeYyNue5itO1xixj_Ko3`9jb0z6=D3)G1S)J_n3V)G$ia7zDoEZV-bb7RT}ZGF3ybaFbT?X z;AJmqZ}BTNbYRkY#qc++^a=OiQ}TuVajwzgF`8nz0S*%S2@bj;QJtxBGeZtyqe7>M zWk6^^u2FI-e5b`HD-&8-R~<1i=%yh!R&=iStzqp7yEJAQeYemGoS0`7Udq)9|EpB{ zuudQ*@ObLb8__GQ-!2zBVbIfW3BQQdACtM!^Lxdj)mmMfOBsv> zCt_LgNMD3ANwEr{3y`-~xZxV5PR^S(ezBOE;Sl>wAHXh)acq`Bmr#au5kiIjrq<@_ zCN|6IhVVtH!wb&P0)`*!e4|9o=`VwV?_z)Os+@I@LN;aw7BU(#3|v`b&JL_d4Zd2m zeu~2vmLUZ3zxh+En`zV%HjTST08 ziqR>wC9Gr(P1TK<4P=C6luH`EtNitJP}Q{x+eWAATE5#XtX?G778jyOPAaVY7!y3{ z5QUyOcPMEM`T)!2@`@Fk(@KO_a$do`dTOiv)yk?S!^Baz((t%GFP5M69$#y9jaR9I z^vVzo^+~}p6c4#HZLM9;Ulr)a=~3$&Se!^3hgc6-Nk~xmWrT_u9E8{ zR>5k-j!i46&ycS)TqShrZxPX-zXhu~Laqi8a`{_U6T7sfnZ61fIo|97w=wua6vP=Q zYW4XWmAUhmIA>3uoRw+3_`;dqRM*;6?XNGwTM2=Lo>@Tr?akhzReVQcLk&P71c z^3wBioaw8a=?g%EHvkl2Ya=+O*EP4Kw_r(0$3oxaO&4a5mp-P~Rk>&5xdyMxT-ngr z;9p-<-%wlY#hW7|^3ofc8ylLvzVuL8wQqeh?6{@5rQMg_-VANkrVFp+Lq!;W&FXZ# zPth;l7YRW?2%(IEnnna$X0dolWnE2O1P;$9V_5Ox#jvswFB$u)@3i9NNw*E(1jkp0 zS6qSu>Xlos0~_YbB@)Z+wO4^sVmu_N1Ro5)A(`-7~>t??UkKqPeRx0#r-sb<) z-L=QaRh98`Z!e`h%x+0|2!yOu5iFhEnb}TT0n^7$>DUL`-EAmna@n1kb_aJJotbU7 zq_GR~(qK@70g+@2Ml@)6C<&+mZM2qXj7T)rXwpg){6kGO5fTZ(-|su;o4s>86WfMA z2q(Muob#RU`_AK@=l6YcZXToG&TQycd*tNAs#P#a>2fXQh-{%``Q{FzUgT?Hhn%cV z*JT!LBGkavvcVDWCRVMx%&DUsY0GJ7})ET}VJFH{^J(-nh6<(hm_UHw=$*(r2u)5l{h0QOg zvy{xRnD|;}0#5&UF?}I+Y;x)jo8vp%V=Oh6rk&_os19GcNDA!wH(i;=U7{)JZWK4j zh9@&zf{RjO&5y&m@LA~;4+Ns>6vAiCi*A1^%s<>(nSBxeEvj~WLnAFc(p}Nq$1;f zHm75+CCD#b+Mi6f6I)oMEQ)+Wal2x=1ba+stFlXx$+lBMaR#%pJ>lb8-zIL+Efx}! z0AWJhVFPFy1f(+X-TsXb8QB&G0~Zr!vm!ByG-TZK5JD1g0~0b0arP&~uKu#!z^kAh+U3;~=gJ z8cS8GO5spd7Kz2dgaG;iC3Mn#$$*I1Fxmb04tJ3=blbLC%VbvrJQsDxO#pC|1!pWG zSZZsm_OG&=Ndii@1XYwc^9jo=%mokokNZe?+<(qrFui{+ zc+NkHIP>d4fVO33QLE;f8=*uw!h(Jpl?C$=VcxTA-vhzo7yk5%ukO37ZZ2m=Z+ktv zX4-*od$T?YHS6E)pOAL9Kj(wl9LlwL8h1`EdgtPEd5gSd_qhKg!29FiC;ey0@EO#i zL+W$>VX{2TstpH6;VrD0UFM_i4Tm}3)(L< z@YGW?m(8%1Mz;0TYVDwH+r6#i7lw{;7%n{Uf-(%J$PmemhD&ZV79Q9JD=o>dvEL=% z<=y2u1O^u#_=lq0<$c8?60{_*c&~VVa?S*2+Te;g+@WQI*Up)=lDBx zbC-h;$KVe+xZcyL_)h}vnM=&@?G}QlII6TgbD`0DH67Ue8E}^Kv^9#7?VE8wtaKf&Dr_~qa~OS4h9%N>9IOsEt7R=|7lYvYS%1-G>RY55mjHV29CFE)DLtmb~W3!lGqfnNxV$WGmB3yu!hM+lBvYUEsXwpi_A+Km(rV!>Y5-F?QaifV2JM{qsuVx1&nz z&Mxq0yTExPmbAa?Z?B=>)6D_iiT}U5z%M}iEXI7bdRE9yuNyB{OS@TE^f?VU$DMKb zns$f4FEQJ1SBUlR0lZT``CS+O|8)4rXt)f=``+njcE$I2z`a2EwgBK6z;L7q{{L&HslcrFj!Ytq^X z$O$%=&yJ4ckxix`g2AE39^rDs0PP+NM^}WS&C~$$*fU-)gsqb-N|7i**O?fwqNUW} zbfv_SP#6a7By*b(tB_nNo1e;oNxBSyY!RZ9u(=26kmEsyk7H)8ys4Z{WjB>GsX;u` zt5)!t#3QvlgRi2bGs)$MBncTz;Y%i&6{%H(5RczQS(RFu85|%Ap@Rb{d>Cb5#d5Mt zu9Qa-pIJ%cvnpA*(#TjivT+Lp;K>0Ty2r~Q571eyO&OA_1avF~gH~@er}0I@yn$%G zxYL#yQZ5|LAz{VqC{)9pQ`HIRCJN9#HNx@f85|p75CMyu0$ZjNMu?+z31Y_j_+B(X zv%VKf49I!I!gRSz6NX3(Z3#7G6tyK^3d8jyYc^-Y?3SSr+RqRY=`g#&0XGbd;H`AB zff%}J%bLx(br92Ux?$~_P2mme*NDVf-5sq<0*1(8QPeh8SuzlA zfXq$=;<;N#n}fCSQa!iv))Gg>XbSB+3XPppcEem|6e8w)6V@eJz>EB%6{OL*TM--N zyFqBn=wO&!8E&o?SjL@2F+st|lLY8ihn(G#Bo-u9lZNY*P1TF!q$W+mZpC~doya7& zX#zc7{*&z0l%HC{Y@wk)K?RVX|gzE=(rU7>G>72#49z zZAIIFVJeYIEH|83q|K;bw{2#Xm{wke29LHk1yWEuwQ)cZ$x0bQr5X+rL zN0Py_Jj`Z?Qfx8KcxW03Q@IR{*PAfQC{VQP4HIntT(sa9=KSy8ly;n?PNx(IMQW}w%=+FQi3=3ah>1s}bknM~Vlfy2&W5f})w zqnU7c<7hf`IobK&c9m#Vl4*15-p zp7u@7kA^(VbKB6+7Fcp%?&zk7`IQ>)skLBXs_C$%BnMIZ3T#zcD@M7kFD8;J(et=Q z+R=&yle+hJtMMbVsIx1Hbb4l!O5U92dNDk|x8*k)ldGVoE$!GVOD1gCWV(}KmduDb z7i@*0TtkoCQKgm3L<71~&NjB_r@9zA+gP#A$d=0;7evll$r9|Es50dIRv(8Ffg`i+ zWhJ1+JgpG{OG`}PyNlWO_v3~_bc!!@nc}S_SEbNlsp9*5->l5C&U9D{Pp)gF2cgr& z;inAU*JKek4KRR=pRDYJ-lcD*GGgFCOClV~F#XyOqRJq$grn7|Mz$0k>DW(=ZN|=0 zj~1B8d9WCx#h3}ViKRw3Qfy3@v5{D}4m)vo)@luJEb-&k%JsypYnoeE9C1!+$J%Yf z8g|{UGNr@RB6{&}QScX!kIe&6l^X-L^=GG#JH)Q%#eQy+Z=Q#7@|v zN`ST_3D`IwD%-V0y(*`qL~+s`Nhb^7rZHrb&pQ)Qh$Pr$g{wWSS{@ok=Hs*%Nmz!M zmvL)TwaoA30>+=A0MpvSxv1FkY0|_*y|`NuY22h?w5bLO#+#XsSMwZ!$jI`q!}LSq z?IM@cis3FZL(vb!@8bA_Hahh$wb9noiHTbAB?wX0s`UKb8=d-2d}V=nLY&#=GKfX# zCmp@|PHfwv30ff=$i?VYpQL_Y3_ng!u^T>WU)A#Kcg@t-@h{-zHRx;}YAGTiRs@Ba}bN9p_eEWY~3m>6-rF0B5y5RcMB zsA`?_70*E_85XDh(}+dsdzH@lypk#ElurF0#ORMLvDoT=@8eNw%F5f_j}eXLuX-Ex zU3X{^#oOR*KPD7~2#GGl7i z*KzKkt^7598HmYC^Itt{Q!Y~aSpKVRa_hOoo=H3w^`Uzwt4}w0@kPAE1lFh*|o&#pg|KQ5VPE)`kB1M=jNtV;we5Kkn$`^*r)T zOTTe(H23+kDxaw?^h=(zbpO>C>)0rr`uiMxdoH-F)fL-`ZZ3BaMah*U4j1#@!#tA1j0eB+UmOkaF2%$+rTp%+z}VgpUoSqqG0EK MZ;2j>5yYbAf9Tlh0{{R3