Disable "-Wnoctad-maybe-unsupported", add and fix "-Wdeprecated-copy-with-user-provided-copy". (#10332)

This is another PR towards the goal of getting Z3 to compile cleanly
when included via FetchContents into clang-tidy, which uses a pretty
strict set of warnings. (2 more flags after this!)

The first of these was -Wctad-maybe-unsupported. That has to do with
"class template argument deduction" -- the flag requires template
deduction guides to be explicitly provided if templated types are used
in situations that requires argument deduction. This fired for various
uses of templated types in the utils directory.

I decided that this should be a case of if it ain't broke, don't fix it,
and explicitly disabled the warning in the Z3 build (which will override
the setting if the flag is enabled in a larger build including Z3, like
clang).

-----

The second flag has to do with the C++ "rule of 3". Here is Google's AI
summary (inf_s_integer is a class in Z3 that triggered the warning):

_This warning means your inf_s_integer class defines a custom copy
assignment operator but lacks a user-defined copy constructor, which the
C++ standard deprecates to encourage the "Rule of Three". To fix this,
explicitly declare and = default the copy constructor in your class
definition._

_...example of how to fix..._

_This updates your code to modern C++ standards, cleanly silencing the
warning._

This seemed like a good standard to follow, and didn't require too many
changes, so I propose them.

cmake/compiler_warnings.cmake

@@ -28,6 +28,8 @@ set(CLANG_ONLY_WARNINGS
   "-Wimplicit-fallthrough"
   "-Wextra-semi"
   "-Wignored-qualifiers"
+  "-Wnoctad-maybe-unsupported"
+  "-Wdeprecated-copy-with-user-provided-copy"
 )
 
 set(MSVC_WARNINGS "/W3")

src/ast/seq_decl_plugin.h

@@ -458,6 +458,7 @@ public:
               Default constructor of invalid info.
             */
             info() = default;
+            info(const info&) = default;
 
             /*
               Used for constructing either an invalid info that is only used to indicate uninitialized entry, or valid but unknown info value.

src/math/lp/dense_matrix.h

@@ -45,6 +45,7 @@ public:
     unsigned m_n; // number of const
     vector<T> m_values;
     dense_matrix(unsigned m, unsigned n);
+    dense_matrix(const dense_matrix &) = default;
 
     dense_matrix operator*=(matrix<T, X> const & a) {
         SASSERT(column_count() == a.row_count());

src/math/subpaving/subpaving_t.h

@@ -120,7 +120,9 @@ public:
         justification(justification const & source) { m_data = source.m_data; }
         explicit justification(clause * c) { m_data = TAG(void*, c, CLAUSE); }
         explicit justification(var x) { m_data = BOXTAGINT(void*, x, VAR_DEF);  }
-        
+
+        justification &operator=(justification const &) = default;
+
         kind get_kind() const { return static_cast<kind>(GET_TAG(m_data)); }
         bool is_clause() const { return get_kind() == CLAUSE; }
         bool is_axiom() const { return get_kind() == AXIOM; }

src/tactic/aig/aig.cpp

@@ -32,6 +32,7 @@ class aig_lit {
 public:
     aig_lit(aig * n = nullptr):m_ref(n) {}
     aig_lit(aig_ref const & r):m_ref(static_cast<aig*>(r.m_ref)) {}
+    aig_lit(const aig_lit &) = default;
     bool is_inverted() const { return (reinterpret_cast<size_t>(m_ref) & static_cast<size_t>(1)) == static_cast<size_t>(1); }
     void invert() { m_ref = reinterpret_cast<aig*>(reinterpret_cast<size_t>(m_ref) ^ static_cast<size_t>(1)); }
     aig * ptr() const { return reinterpret_cast<aig*>(reinterpret_cast<size_t>(m_ref) & ~static_cast<size_t>(1)); }

src/util/inf_s_integer.h

@@ -45,6 +45,7 @@ class inf_s_integer {
     std::string to_string() const;
 
     inf_s_integer() = default;
+    inf_s_integer(const inf_s_integer&) = default;
 
     explicit inf_s_integer(int n):m_first(n), m_second(0) {}
     explicit inf_s_integer(int n, int d): m_first(n), m_second(0) { SASSERT(d == 1); }

src/util/params.cpp

@@ -361,7 +361,8 @@ class params {
             rational *    m_rat_value;
         };
         value() : m_kind(CPK_BOOL), m_bool_value(false) {}
-        value& operator=(value const& other) {
+        value(const value &) = default;
+        value &operator=(value const &other) {
             m_kind = other.m_kind;
             switch (m_kind) {
             case CPK_BOOL: m_bool_value = other.m_bool_value; break;

src/util/ref_buffer.h

@@ -174,7 +174,9 @@ public:
         super(ref_manager_wrapper<T, TManager>(other.m_manager)) {
         SASSERT(this->m_buffer.size() == 0);
         append(other);
-    }        
+    }
+
+    ref_buffer &operator=(const ref_buffer &) = default;
 };
 
 /**