Merge branch 'master' into polysat

.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

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 $<$<CONFIG:Debug>:_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
 ################################################################################

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.
   #

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@
 */

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

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

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);
 };
 

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<mpq>()),
-        m_var_register(0) {}
+        m_var_register(false) {}
     
     bool hnf_cutter::is_full() const {
         return

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;
     };
 
 

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> 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);

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:

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*, app*> app_pair;
         typedef pair_hash<obj_ptr_hash<app>, obj_ptr_hash<app> > app_pair_hash;

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);

src/util/array.h

@@ -37,8 +37,6 @@ private:
 
     char * raw_ptr() const { return reinterpret_cast<char*>(reinterpret_cast<size_t*>(m_data) - 1); }
 
-    array & operator=(array const & source);
-
     void set_data(void * mem, unsigned sz) {
         size_t * _mem = static_cast<size_t*>(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<typename Allocator>
     void finalize(Allocator & a) {

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

src/util/mpz.h

@@ -44,7 +44,7 @@ typedef unsigned digit_t;
 template<bool SYNCH> class mpz_manager;
 template<bool SYNCH> 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<bool SYNCH> 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;

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; }
     
         

src/util/scoped_numeral_buffer.h

@@ -24,13 +24,14 @@ template<typename Manager, unsigned INITIAL_SIZE = 16>
 class _scoped_numeral_buffer : public sbuffer<typename Manager::numeral, INITIAL_SIZE> {
     typedef sbuffer<typename Manager::numeral, INITIAL_SIZE> 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++) {