Use noexcept more. (#7058)

src/ast/recfun_decl_plugin.cpp

@@ -602,15 +602,6 @@ namespace recfun {
         m_args.append(n->get_num_args(), n->get_args());
     }
 
-    case_expansion::case_expansion(case_expansion const & from)
-        : m_lhs(from.m_lhs),
-          m_def(from.m_def),
-          m_args(from.m_args) {}
-    case_expansion::case_expansion(case_expansion && from)
-        : m_lhs(from.m_lhs),
-          m_def(from.m_def),
-          m_args(std::move(from.m_args)) {}
-
     std::ostream& case_expansion::display(std::ostream & out) const {
         return out << "case_exp(" << m_lhs << ")";
     }

src/ast/recfun_decl_plugin.h

@@ -301,8 +301,6 @@ namespace recfun {
         recfun::def *       m_def;
         expr_ref_vector     m_args;
         case_expansion(recfun::util& u, app * n);
-        case_expansion(case_expansion const & from);
-        case_expansion(case_expansion && from);
         std::ostream& display(std::ostream& out) const;
     };
 
@@ -323,10 +321,6 @@ namespace recfun {
         }
         body_expansion(app_ref & pred, recfun::case_def const & d, expr_ref_vector & args) : 
             m_pred(pred), m_cdef(&d), m_args(args) {}
-        body_expansion(body_expansion const & from): 
-            m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {}
-        body_expansion(body_expansion && from) noexcept :
-            m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
 
         std::ostream& display(std::ostream& out) const;
     };

src/math/dd/dd_pdd.h

@@ -503,7 +503,7 @@ namespace dd {
         unsigned max_pow2_divisor() const { return m->max_pow2_divisor(root); }
         unsigned_vector const& free_vars() const { return m->free_vars(*this); }
 
-        void swap(pdd& other) { VERIFY_EQ(m, other.m); std::swap(root, other.root); }
+        void swap(pdd& other) noexcept { VERIFY_EQ(m, other.m); std::swap(root, other.root); }
 
         pdd_iterator begin() const;
         pdd_iterator end() const;
@@ -547,7 +547,7 @@ namespace dd {
     inline pdd& operator-=(pdd & p, rational const& q) { p = p - q; return p; }
     inline pdd& operator+=(pdd & p, rational const& q) { p = p + q; return p; }
 
-    inline void swap(pdd& p, pdd& q) { p.swap(q); }
+    inline void swap(pdd& p, pdd& q) noexcept { p.swap(q); }
 
     std::ostream& operator<<(std::ostream& out, pdd const& b);
 

src/math/lp/lp_core_solver_base.h

@@ -517,7 +517,7 @@ class lp_core_solver_base {
 
 
     template <typename K>
-    static void swap(vector<K> &v, unsigned i, unsigned j) {
+    static void swap(vector<K> &v, unsigned i, unsigned j) noexcept {
         auto t = v[i];
         v[i] = v[j];
         v[j] = t;

src/math/polynomial/algebraic_numbers.cpp

@@ -358,7 +358,7 @@ namespace algebraic_numbers {
             return a.to_algebraic()->m_p_sz - 1;
         }
 
-        void swap(numeral & a, numeral & b) {
+        void swap(numeral & a, numeral & b) noexcept {
             std::swap(a.m_cell, b.m_cell);
         }
 
@@ -2935,7 +2935,7 @@ namespace algebraic_numbers {
         return m_imp->to_rational(const_cast<numeral&>(a), r);
     }
 
-    void manager::swap(numeral & a, numeral & b) {
+    void manager::swap(numeral & a, numeral & b) noexcept {
         return m_imp->swap(a, b);
     }
 

src/math/polynomial/algebraic_numbers.h

@@ -129,7 +129,7 @@ namespace algebraic_numbers {
         void set(numeral & a, mpq const & n);
         void set(numeral & a, numeral const & n);
 
-        void swap(numeral & a, numeral & b);
+        void swap(numeral & a, numeral & b) noexcept;
 
         /**
            \brief Store in b an integer value smaller than 'a'.

src/math/polynomial/polynomial.cpp

@@ -447,7 +447,7 @@ namespace polynomial {
         }
     };
 
-    inline void swap(monomial * & m1, monomial * & m2) { std::swap(m1, m2); }
+    inline void swap(monomial * & m1, monomial * & m2) noexcept { std::swap(m1, m2); }
 
     typedef chashtable<monomial*, monomial::hash_proc, monomial::eq_proc> monomial_table;
 

src/math/polynomial/upolynomial.cpp

@@ -126,7 +126,7 @@ namespace upolynomial {
         m_factors[i].swap(p);
     }
 
-    void core_manager::factors::swap(factors & other) {
+    void core_manager::factors::swap(factors & other) noexcept {
         m_factors.swap(other.m_factors);
         m_degrees.swap(other.m_degrees);
         nm().swap(m_constant, other.m_constant);

src/math/polynomial/upolynomial.h

@@ -89,7 +89,7 @@ namespace upolynomial {
             void push_back_swap(numeral_vector & p, unsigned degree);
 
             void swap_factor(unsigned i, numeral_vector & p);
-            void swap(factors & other);
+            void swap(factors & other) noexcept;
             void multiply(numeral_vector & out) const; 
 
             void display(std::ostream & out) const;

src/math/polynomial/upolynomial_factorization_int.h

@@ -85,7 +85,7 @@ namespace upolynomial {
 
         unsigned max_degree() const { return m_set.size() - 1; }
 
-        void swap(factorization_degree_set & other) {
+        void swap(factorization_degree_set & other) noexcept {
             m_set.swap(other.m_set);
         }
 

src/math/realclosure/mpz_matrix.h

@@ -50,7 +50,7 @@ class mpz_matrix {
         SASSERT(j < n); 
         return a_ij[i*n + j]; }
     mpz & operator()(unsigned i, unsigned j) { SASSERT(i < m); SASSERT(j < n); return a_ij[i*n + j]; }
-    void swap(mpz_matrix & B) { std::swap(m, B.m); std::swap(n, B.n); std::swap(a_ij, B.a_ij); }
+    void swap(mpz_matrix & B) noexcept { std::swap(m, B.m); std::swap(n, B.n); std::swap(a_ij, B.a_ij); }
     mpz * row(unsigned i) const { SASSERT(i < m); return a_ij + i*n; }
 };
 
@@ -136,7 +136,7 @@ class scoped_mpz_matrix {
     mpz_matrix const & get() const { return A; }
     mpz_matrix & get() { return A; }
 
-    void swap(mpz_matrix & B) { A.swap(B); }
+    void swap(mpz_matrix & B) noexcept { A.swap(B); }
 
     void set(unsigned i, unsigned j, mpz const & v) { nm().set(A(i, j), v); }
     void set(unsigned i, unsigned j, int v) { nm().set(A(i, j), v); }

src/math/realclosure/realclosure.cpp

@@ -135,7 +135,7 @@ namespace realclosure {
     typedef interval_manager<mpbq_config> mpbqi_manager;
     typedef mpbqi_manager::interval       mpbqi;
 
-    void swap(mpbqi & a, mpbqi & b) {
+    void swap(mpbqi & a, mpbqi & b) noexcept {
         swap(a.m_lower, b.m_lower);
         swap(a.m_upper, b.m_upper);
         std::swap(a.m_lower_inf, b.m_lower_inf);
@@ -2534,7 +2534,7 @@ namespace realclosure {
             return depends_on_infinitesimals(a.m_value);
         }
 
-        static void swap(mpbqi & a, mpbqi & b) {
+        static void swap(mpbqi & a, mpbqi & b) noexcept {
             realclosure::swap(a, b);
         }
 
@@ -6313,7 +6313,7 @@ namespace realclosure {
         m_imp->set(a, n);
     }
 
-    void manager::swap(numeral & a, numeral & b) {
+    void manager::swap(numeral & a, numeral & b) noexcept {
         std::swap(a.m_value, b.m_value);
     }
 

src/math/realclosure/realclosure.h

@@ -164,7 +164,7 @@ namespace realclosure {
         void set(numeral & a, mpq const & n);
         void set(numeral & a, numeral const & n);
 
-        void swap(numeral & a, numeral & b);
+        void swap(numeral & a, numeral & b) noexcept;
 
         /**
            \brief Return a^{1/k}

src/muz/rel/dl_base.h

@@ -484,7 +484,7 @@ namespace datalog {
 
             virtual bool can_swap(const base_object & o) const { return false; }
 
-            virtual void swap(base_object & o) {
+            virtual void swap(base_object & o) noexcept {
                 std::swap(m_kind, o.m_kind);
 #if DL_LEAK_HUNTING
                 m_leak_guard = get_plugin().get_ast_manager().mk_fresh_sort(get_plugin().get_name().bare_str());
@@ -910,7 +910,7 @@ namespace datalog {
     public:
         table_signature() : m_functional_columns(0) {}
 
-        void swap(table_signature & s) {
+        void swap(table_signature & s) noexcept {
             signature_base::swap(s);
             std::swap(m_functional_columns, s.m_functional_columns);
         }

src/muz/rel/dl_finite_product_relation.cpp

@@ -1835,7 +1835,7 @@ namespace datalog {
         }
     }
 
-    void finite_product_relation::swap(relation_base & r0) {
+    void finite_product_relation::swap(relation_base & r0) noexcept {
         SASSERT(can_swap(r0));
         finite_product_relation & r = finite_product_relation_plugin::get(r0);
         SASSERT(get_signature()==r.get_signature());

src/muz/rel/dl_finite_product_relation.h

@@ -316,7 +316,7 @@ namespace datalog {
 
            Both relations must come from the same plugin and be of the same signature.
         */
-        void swap(relation_base & r) override;
+        void swap(relation_base & r) noexcept override;
 
         /**
            \brief Create a \c finite_product_relation object.

src/muz/rel/dl_vector_relation.h

@@ -59,7 +59,7 @@ namespace datalog {
             dealloc(m_elems);
         }
 
-        void swap(relation_base& other) override {
+        void swap(relation_base& other) noexcept override {
             vector_relation& o = dynamic_cast<vector_relation&>(other);
             if (&o == this) return;
             std::swap(o.m_eqs, m_eqs);

src/nlsat/nlsat_assignment.h

@@ -33,7 +33,7 @@ namespace nlsat {
     public:
         assignment(anum_manager & _m):m_values(_m) {}
         anum_manager & am() const { return m_values.m(); }
-        void swap(assignment & other) {
+        void swap(assignment & other) noexcept {
             m_values.swap(other.m_values);
             m_assigned.swap(other.m_assigned);
         }
@@ -67,7 +67,7 @@ namespace nlsat {
         anum_manager & m() const override { return am(); }
         bool contains(var x) const override { return is_assigned(x); }
         anum const & operator()(var x) const override { SASSERT(is_assigned(x)); return value(x); }
-        void swap(var x, var y) {
+        void swap(var x, var y) noexcept {
             SASSERT(x < m_values.size() && y < m_values.size());
             std::swap(m_assigned[x], m_assigned[y]);
             std::swap(m_values[x], m_values[y]);

src/nlsat/nlsat_scoped_literal_vector.h

@@ -67,7 +67,7 @@ namespace nlsat {
         void append(scoped_literal_vector const& ls) {
             append(ls.size(), ls.data());
         }
-        void swap(scoped_literal_vector& other) {
+        void swap(scoped_literal_vector& other) noexcept {
             SASSERT(&m_solver == &other.m_solver);
             m_lits.swap(other.m_lits);
         }

src/nlsat/nlsat_solver.cpp

@@ -48,7 +48,7 @@ namespace nlsat {
     typedef chashtable<root_atom*, root_atom::hash_proc, root_atom::eq_proc> root_atom_table;
 
     // for apply_permutation procedure
-    void swap(clause * & c1, clause * & c2) {
+    void swap(clause * & c1, clause * & c2) noexcept {
         std::swap(c1, c2);
     }
 

src/sat/sat_cutset.h

@@ -183,7 +183,7 @@ namespace sat {
         void reset(on_update_t& on_del) { shrink(on_del, 0); }
         cut const & operator[](unsigned idx) const { return m_cuts[idx]; }
         void shrink(on_update_t& on_del, unsigned j); 
-        void swap(cut_set& other) { 
+        void swap(cut_set& other) noexcept {
             std::swap(m_var, other.m_var);
             std::swap(m_size, other.m_size); 
             std::swap(m_max_size, other.m_max_size); 

src/sat/sat_model_converter.cpp

@@ -369,7 +369,7 @@ namespace sat {
         return result;
     }
 
-    void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) {
+    void model_converter::swap(bool_var v, unsigned sz, literal_vector& clause) noexcept {
         for (unsigned j = 0; j < sz; ++j) {
             if (v == clause[j].var()) {
                 std::swap(clause[0], clause[j]);

src/sat/sat_model_converter.h

@@ -91,7 +91,7 @@ namespace sat {
 
         bool legal_to_flip(bool_var v) const;
 
-        void swap(bool_var v, unsigned sz, literal_vector& clause);
+        void swap(bool_var v, unsigned sz, literal_vector& clause) noexcept;
 
         void add_elim_stack(entry & e);
 

src/sat/smt/pb_card.h

@@ -33,7 +33,7 @@ namespace pb {
         literal const* begin() const { return m_lits; }
         literal const* end() const { return static_cast<literal const*>(m_lits) + m_size; }
         void negate() override;
-        void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); }
+        void swap(unsigned i, unsigned j) noexcept override { std::swap(m_lits[i], m_lits[j]); }
         literal_vector literals() const override { return literal_vector(m_size, m_lits); }
         bool is_watching(literal l) const override;
         literal get_lit(unsigned i) const override { return m_lits[i]; }

src/sat/smt/pb_constraint.h

@@ -102,7 +102,7 @@ namespace pb {
 
         virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
         virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
-        virtual void swap(unsigned i, unsigned j) { UNREACHABLE(); }
+        virtual void swap(unsigned i, unsigned j) noexcept { UNREACHABLE(); }
         virtual literal get_lit(unsigned i) const { UNREACHABLE(); return sat::null_literal; }
         virtual void set_lit(unsigned i, literal l) { UNREACHABLE(); }
         virtual void negate() { UNREACHABLE(); }

src/sat/smt/pb_pb.h

@@ -46,7 +46,7 @@ namespace pb {
         bool is_cardinality() const;
         void negate() override;
         void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); }
-        void swap(unsigned i, unsigned j) override { std::swap(m_wlits[i], m_wlits[j]); }
+        void swap(unsigned i, unsigned j) noexcept override { std::swap(m_wlits[i], m_wlits[j]); }
         literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; }
         bool is_watching(literal l) const override;
         literal get_lit(unsigned i) const override { return m_wlits[i].second; }

src/smt/old_interval.cpp

@@ -238,7 +238,7 @@ interval & interval::operator=(interval const & other) {
     return *this;
 }
 
-interval & interval::operator=(interval && other) {
+interval & interval::operator=(interval && other) noexcept {
     SASSERT(&m_manager == &other.m_manager);
     m_lower = std::move(other.m_lower);
     m_upper = std::move(other.m_upper);

src/smt/old_interval.h

@@ -92,7 +92,7 @@ class old_interval {
     rational const & get_lower_value() const { SASSERT(!minus_infinity()); return m_lower.to_rational(); }
     rational const & get_upper_value() const { SASSERT(!plus_infinity()); return m_upper.to_rational(); }
     old_interval & operator=(old_interval const & other);
-    old_interval & operator=(old_interval && other);
+    old_interval & operator=(old_interval && other) noexcept;
     old_interval & operator+=(old_interval const & other);
     old_interval & operator-=(old_interval const & other);
     old_interval & operator*=(old_interval const & other);

src/util/array.h

@@ -184,7 +184,7 @@ class array {
     T const * data() const { return m_data; }
     T * data() { return m_data; }
 
-    void swap(array & other) {
+    void swap(array & other) noexcept {
         std::swap(m_data, other.m_data);
     }
 

src/util/basic_interval.h

@@ -52,8 +52,8 @@ class basic_interval_manager {
         interval const & get() const { return m_interval; }
         interval & get() { return m_interval; }
         void reset() { m().reset(m_interval); }
-        void swap(scoped_interval & a) { m().swap(m_interval, a.m_interval); }
-        void swap(interval & a) { m().swap(m_interval, a); }
+        void swap(scoped_interval & a) noexcept { m().swap(m_interval, a.m_interval); }
+        void swap(interval & a) noexcept { m().swap(m_interval, a); }
         bound const & lower() const { return m_interval.lower(); }
         bound const & upper() const { return m_interval.upper(); }
         bound & lower() { return m_interval.lower(); }
@@ -146,7 +146,7 @@ class basic_interval_manager {
         m().set(a.m_upper, n);
     }
 
-    void swap(interval & a, interval & b) {
+    void swap(interval & a, interval & b) noexcept {
         m().swap(a.m_lower, b.m_lower);
         m().swap(a.m_upper, b.m_upper);
     }

src/util/bit_vector.h

@@ -98,7 +98,7 @@ class bit_vector {
         m_num_bits = 0;
     }
 
-    void swap(bit_vector & other) {
+    void swap(bit_vector & other) noexcept {
         std::swap(m_data, other.m_data);
         std::swap(m_num_bits, other.m_num_bits);
         std::swap(m_capacity, other.m_capacity);

src/util/chashtable.h

@@ -553,7 +553,7 @@ class chashtable : private HashProc, private EqProc {
     iterator begin() const { return iterator(m_table, m_table + m_slots); }
     iterator end() const { return iterator(); }
 
-    void swap(chashtable & other) {
+    void swap(chashtable & other) noexcept {
         std::swap(m_table,       other.m_table);
         std::swap(m_capacity,    other.m_capacity);
         std::swap(m_init_slots,  other.m_init_slots);

src/util/double_manager.h

@@ -76,7 +76,7 @@ class double_manager {
     static void set(double & a, unsigned val) { a = static_cast<double>(val); }
     static void set(double & a, int64_t val) { a = static_cast<double>(val); }
     static void set(double & a, uint64_t val) { a = static_cast<double>(val); }
-    static void swap(double & a, double & b) { std::swap(a, b); }
+    static void swap(double & a, double & b) noexcept { std::swap(a, b); }
     bool is_pos(double a) const { return a > m_zero_tolerance; }
     bool is_neg(double a) const { return a < m_zero_tolerance; }
     bool is_zero(double a) const { return  -m_zero_tolerance <= a && a <= m_zero_tolerance; }