diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index e7ca0f1b5..04d13b1e8 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -41,7 +41,7 @@ jobs: type=edge type=sha,prefix=ubuntu-20.04-bare-z3-sha- - name: Build and push Bare Z3 Docker Image - uses: docker/build-push-action@v3.0.0 + uses: docker/build-push-action@v3.1.0 with: context: . push: true diff --git a/CMakeLists.txt b/CMakeLists.txt index 14bc1bfc2..a6a72ff13 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -188,9 +188,6 @@ set(CMAKE_CXX_STANDARD_REQUIRED ON) if (CMAKE_SYSTEM_NAME STREQUAL "Linux") message(STATUS "Platform: Linux") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_") - if (TARGET_ARCHITECTURE STREQUAL "x86_64") - list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") - endif() elseif (CMAKE_SYSTEM_NAME STREQUAL "Android") message(STATUS "Platform: Android") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_ANDROID_") @@ -348,14 +345,6 @@ endif() option(Z3_BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON) -################################################################################ -# Symbol visibility -################################################################################ -if (NOT MSVC) - z3_add_cxx_flag("-fvisibility=hidden" REQUIRED) - z3_add_cxx_flag("-fvisibility-inlines-hidden" REQUIRED) -endif() - ################################################################################ # Tracing ################################################################################ @@ -367,20 +356,6 @@ else() list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_TRACE>) endif() -################################################################################ -# Position independent code -################################################################################ -# This is required because code built in the components will end up in a shared -# library. - -# Avoid adding -fPIC compiler switch if we compile with MSVC (which does not -# support the flag) or if we target Windows, which generally does not use -# position independent code for native code shared libraries (DLLs). -if (NOT (MSVC OR MINGW OR WIN32)) - z3_add_cxx_flag("-fPIC" REQUIRED) -endif() - - ################################################################################ # Link time optimization ################################################################################ diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index c4b2dfbfe..47ecb04aa 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -206,6 +206,12 @@ macro(z3_add_component component_name) foreach (flag ${Z3_COMPONENT_CXX_FLAGS}) target_compile_options(${component_name} PRIVATE ${flag}) endforeach() + set_target_properties(${component_name} PROPERTIES + # Position independent code needed in shared libraries + POSITION_INDEPENDENT_CODE ON + # Symbol visibility + CXX_VISIBILITY_PRESET hidden + VISIBILITY_INLINES_HIDDEN ON) # It's unfortunate that we have to manage dependencies ourselves. # diff --git a/doc/website.dox.in b/doc/website.dox.in index 5249f2ae0..651652ce4 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -8,5 +8,5 @@ This website hosts the automatically generated documentation for the Z3 APIs. - - \ref @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ + @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ */ diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index dcc21f255..07a53f8f0 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -1,11 +1,4 @@ include(ExternalProject) -# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject -# that shipped with CMake >= 3.1. -if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1")) - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1) -else() - set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") -endif() option(Z3_C_EXAMPLES_FORCE_CXX_LINKER "Force C++ linker when building C example projects" OFF) @@ -43,7 +36,7 @@ ExternalProject_Add(c_example "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -62,7 +55,7 @@ ExternalProject_Add(c_maxsat_example "${EXTERNAL_C_PROJ_USE_CXX_LINKER_ARG}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_maxsat_example_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -81,7 +74,7 @@ ExternalProject_Add(cpp_example "-DZ3_DIR=${PROJECT_BINARY_DIR}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -99,7 +92,7 @@ ExternalProject_Add(z3_tptp5 "-DZ3_DIR=${PROJECT_BINARY_DIR}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command @@ -117,7 +110,7 @@ ExternalProject_Add(userPropagator "-DZ3_DIR=${PROJECT_BINARY_DIR}" "${EXTERNAL_PROJECT_CMAKE_BUILD_TYPE_ARG}" # Build step - ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BUILD_ALWAYS ON BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/userPropagator_build_dir" # Install Step INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 54242dfe6..781961259 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2640,8 +2640,6 @@ def mk_config(): if is64(): if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'): CXXFLAGS = '%s -fPIC' % CXXFLAGS - if sysname == 'Linux' or sysname == 'FreeBSD': - CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS elif not LINUX_X64: CXXFLAGS = '%s -m32' % CXXFLAGS LDFLAGS = '%s -m32' % LDFLAGS diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index d036ad789..28218ee17 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -48,14 +48,14 @@ class smaller_pattern { void save(expr * p1, expr * p2); bool process(expr * p1, expr * p2); - smaller_pattern & operator=(smaller_pattern const &); - public: smaller_pattern(ast_manager & m): m(m) { } + smaller_pattern & operator=(smaller_pattern const &) = delete; + bool operator()(unsigned num_bindings, expr * p1, expr * p2); }; diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 70a9222e4..c1f93c9d8 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -20,7 +20,7 @@ namespace lp { lra(lia.lra), m_settings(lia.settings()), m_abs_max(zero_of_type()), - m_var_register(0) {} + m_var_register(false) {} bool hnf_cutter::is_full() const { return diff --git a/src/muz/base/dl_costs.h b/src/muz/base/dl_costs.h index 333dac996..ea3efcda9 100644 --- a/src/muz/base/dl_costs.h +++ b/src/muz/base/dl_costs.h @@ -80,10 +80,8 @@ namespace datalog { bool passes_output_thresholds(context & ctx) const; void output_profile(std::ostream & out) const; - private: - //private and undefined copy constructor and operator= to avoid the default ones - accounted_object(const accounted_object &); - accounted_object& operator=(const accounted_object &); + accounted_object(const accounted_object &) = delete; + accounted_object& operator=(const accounted_object &) = delete; }; diff --git a/src/muz/base/dl_rule_subsumption_index.h b/src/muz/base/dl_rule_subsumption_index.h index 02f373377..9c29683b3 100644 --- a/src/muz/base/dl_rule_subsumption_index.h +++ b/src/muz/base/dl_rule_subsumption_index.h @@ -25,10 +25,6 @@ Revision History: namespace datalog { class rule_subsumption_index { - //private and undefined copy constroctor - rule_subsumption_index(rule_subsumption_index const&); - //private and undefined operator= - rule_subsumption_index& operator=(rule_subsumption_index const&); typedef obj_hashtable app_set; @@ -53,6 +49,8 @@ namespace datalog { reset_dealloc_values(m_unconditioned_heads); } + rule_subsumption_index(rule_subsumption_index const&) = delete; + rule_subsumption_index& operator=(rule_subsumption_index const&) = delete; void add(rule * r); bool is_subsumed(rule * r); bool is_subsumed(app * query); diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index f0634f0d5..1a4125ed4 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -180,10 +180,9 @@ namespace datalog { public: base_fn() = default; virtual ~base_fn() {} - private: - //private and undefined copy constructor and operator= to avoid copying - base_fn(const base_fn &); - base_fn& operator=(const base_fn &); + + base_fn(const base_fn &) = delete; + base_fn& operator=(const base_fn &) = delete; }; class join_fn : public base_fn { @@ -1098,6 +1097,9 @@ namespace datalog { iterator_core() : m_ref_cnt(0) {} virtual ~iterator_core() {} + iterator_core(const iterator_core &) = delete; + iterator_core & operator=(const iterator_core &) = delete; + void inc_ref() { m_ref_cnt++; } void dec_ref() { SASSERT(m_ref_cnt>0); @@ -1116,10 +1118,6 @@ namespace datalog { //the equality with the end() iterator return is_finished() && it.is_finished(); } - private: - //private and undefined copy constructor and assignment operator - iterator_core(const iterator_core &); - iterator_core & operator=(const iterator_core &); }; struct row_iterator_core { @@ -1128,6 +1126,9 @@ namespace datalog { row_iterator_core() : m_ref_cnt(0) {} virtual ~row_iterator_core() {} + row_iterator_core(const row_iterator_core &) = delete; + row_iterator_core & operator=(const row_iterator_core &) = delete; + void inc_ref() { m_ref_cnt++; } void dec_ref() { SASSERT(m_ref_cnt>0); @@ -1146,10 +1147,6 @@ namespace datalog { //the equality with the end() iterator return is_finished() && it.is_finished(); } - private: - //private and undefined copy constructor and assignment operator - row_iterator_core(const row_iterator_core &); - row_iterator_core & operator=(const row_iterator_core &); }; public: diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index 3fa52ae2f..37fd3ef36 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -56,6 +56,7 @@ namespace datalog { pair_info() {} + pair_info & operator=(const pair_info &) = delete; bool can_be_joined() const { return m_consumers > 0; } @@ -110,8 +111,6 @@ namespace datalog { SASSERT(!m_rules.empty() || m_consumers == 0); return m_rules.empty(); } - private: - pair_info & operator=(const pair_info &); //to avoid the implicit one }; typedef std::pair app_pair; typedef pair_hash, obj_ptr_hash > app_pair_hash; diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 28cbf638e..eda00b64d 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -111,8 +111,6 @@ namespace datalog { rule_unifier m_unifier; - slice_proof_converter(slice_proof_converter const& other); - void init_form2rule() { if (!m_sliceform2rule.empty()) { return; @@ -271,6 +269,8 @@ namespace datalog { m_renaming.insert(orig_rule, unsigned_vector(sz, renaming)); } + slice_proof_converter(slice_proof_converter const& other) = delete; + proof_ref operator()(ast_manager& m, unsigned num_source, proof * const * source) override { SASSERT(num_source == 1); proof_ref result(source[0], m); diff --git a/src/util/array.h b/src/util/array.h index 6c04c10d2..a4c2aa2c7 100644 --- a/src/util/array.h +++ b/src/util/array.h @@ -37,8 +37,6 @@ private: char * raw_ptr() const { return reinterpret_cast(reinterpret_cast(m_data) - 1); } - array & operator=(array const & source); - void set_data(void * mem, unsigned sz) { size_t * _mem = static_cast(mem); *_mem = sz; @@ -115,6 +113,8 @@ public: destroy_elements(); } + array & operator=(array const & source) = delete; + // Free the memory used to store the array. template void finalize(Allocator & a) { diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 15646f216..67f5b82b3 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -215,7 +215,7 @@ void * memory::allocate(char const* file, int line, char const* obj, size_t s) { } #endif -#if !defined(SINGLE_THREAD) && (defined(_WINDOWS) || defined(_USE_THREAD_LOCAL)) +#if !defined(SINGLE_THREAD) // ================================== // ================================== // THREAD LOCAL VERSION diff --git a/src/util/mpz.h b/src/util/mpz.h index 1a7b6f55e..a1bb19395 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -44,7 +44,7 @@ typedef unsigned digit_t; template class mpz_manager; template class mpq_manager; -#if !defined(_MP_GMP) && !defined(_MP_MSBIGNUM) && !defined(_MP_INTERNAL) +#if !defined(_MP_GMP) && !defined(_MP_INTERNAL) #ifdef _WINDOWS #define _MP_INTERNAL #else @@ -52,13 +52,8 @@ template class mpq_manager; #endif #endif -#if defined(_MP_MSBIGNUM) -typedef size_t digit_t; -#elif defined(_MP_INTERNAL) -typedef unsigned int digit_t; -#endif - #ifndef _MP_GMP +typedef unsigned int digit_t; class mpz_cell { unsigned m_size; unsigned m_capacity; diff --git a/src/util/params.h b/src/util/params.h index da05dff90..7ad152a59 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -35,13 +35,14 @@ class params_ref { params * m_params; void init(); void copy_core(params const * p); - params_ref& operator=(params_ref const& p) = delete; void set(params_ref const& p); public: params_ref():m_params(nullptr) {} params_ref(params_ref const & p); ~params_ref(); + params_ref& operator=(params_ref const& p) = delete; + static params_ref const & get_empty() { return g_empty_params_ref; } diff --git a/src/util/scoped_numeral_buffer.h b/src/util/scoped_numeral_buffer.h index 86181f761..81d10ba40 100644 --- a/src/util/scoped_numeral_buffer.h +++ b/src/util/scoped_numeral_buffer.h @@ -24,13 +24,14 @@ template class _scoped_numeral_buffer : public sbuffer { typedef sbuffer super; Manager & m_manager; - _scoped_numeral_buffer(_scoped_numeral_buffer const & v); public: _scoped_numeral_buffer(Manager & m):m_manager(m) {} ~_scoped_numeral_buffer() { reset(); } + _scoped_numeral_buffer(_scoped_numeral_buffer const & v) = delete; + void reset() { unsigned sz = this->size(); for (unsigned i = 0; i < sz; i++) {