From bb26f219fef9e2d4ca2142d36bdaf39931519b43 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Sun, 12 Jul 2020 17:41:57 +0100
Subject: [PATCH] remove unneeded constructors (last round)

---
 src/ast/ast.h                                |  5 --
 src/math/lp/ul_pair.h                        |  8 +--
 src/muz/rel/dl_bound_relation.h              |  2 -
 src/muz/spacer/spacer_context.cpp            |  4 --
 src/muz/spacer/spacer_context.h              |  1 -
 src/muz/spacer/spacer_manager.h              |  1 -
 src/muz/transforms/dl_mk_karr_invariants.cpp |  6 --
 src/muz/transforms/dl_mk_karr_invariants.h   |  1 -
 src/opt/opt_solver.cpp                       |  2 +-
 src/qe/qe.h                                  |  2 -
 src/sat/sat_clause.h                         | 10 ---
 src/sat/sat_cutset.h                         | 13 ----
 src/sat/sat_types.h                          |  6 --
 src/smt/smt_b_justification.h                |  4 --
 src/smt/theory_seq.h                         | 40 +----------
 src/smt/theory_str.h                         |  5 --
 src/smt/watch_list.h                         |  2 +-
 src/solver/parallel_tactic.cpp               |  3 -
 src/tactic/sls/bvsls_opt_engine.h            |  9 ---
 src/tactic/sls/sls_tracker.h                 | 21 +-----
 src/util/array_map.h                         |  1 -
 src/util/hwf.h                               |  5 +-
 src/util/inf_eps_rational.h                  | 19 +-----
 src/util/inf_int_rational.h                  | 15 ----
 src/util/inf_rational.h                      |  8 ---
 src/util/mpq.h                               |  1 -
 src/util/mpz.h                               |  6 --
 src/util/obj_ref.h                           | 10 +--
 src/util/optional.h                          | 72 ++++++++------------
 src/util/rational.h                          |  6 +-
 src/util/ref.h                               | 10 ++-
 src/util/ref_pair_vector.h                   |  6 +-
 src/util/ref_vector.h                        | 10 +--
 src/util/s_integer.h                         |  2 -
 src/util/stacked_value.h                     | 11 ---
 src/util/uint_set.h                          | 12 ----
 src/util/vector.h                            |  2 +-
 37 files changed, 65 insertions(+), 276 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 6e72a3fa3..30dd2a44d 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -264,7 +264,6 @@ public:
               unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_params = false);
 
     decl_info(decl_info const& other);
-    ~decl_info() {}
 
     void init_eh(ast_manager & m);
     void del_eh(ast_manager & m);
@@ -314,7 +313,6 @@ class sort_size {
 public:
     sort_size():m_kind(SS_INFINITE) {}
     sort_size(uint64_t const & sz):m_kind(SS_FINITE), m_size(sz) {}
-    sort_size(sort_size const& other): m_kind(other.m_kind), m_size(other.m_size) {}
     explicit sort_size(rational const& r) {
         if (r.is_uint64()) {
             m_kind = SS_FINITE;
@@ -371,8 +369,6 @@ public:
     sort_info(decl_info const& di, sort_size const& num_elements) : 
         decl_info(di), m_num_elements(num_elements) {}
 
-    ~sort_info() {}
-
     bool is_infinite() const { return m_num_elements.is_infinite(); }
     bool is_very_big() const { return m_num_elements.is_very_big(); }
     sort_size const & get_num_elements() const { return m_num_elements; }
@@ -403,7 +399,6 @@ struct func_decl_info : public decl_info {
     bool m_lambda:1;
 
     func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = nullptr);
-    ~func_decl_info() {}
 
     bool is_associative() const { return m_left_assoc && m_right_assoc; }
     bool is_left_associative() const { return m_left_assoc; }
diff --git a/src/math/lp/ul_pair.h b/src/math/lp/ul_pair.h
index 371b507ac..abfb4483b 100644
--- a/src/math/lp/ul_pair.h
+++ b/src/math/lp/ul_pair.h
@@ -70,16 +70,12 @@ public:
         m_lower_bound_witness(UINT_MAX),
         m_upper_bound_witness(UINT_MAX),
         m_associated_with_row(false) {}
-    
+
     ul_pair(bool associated_with_row) :
         m_lower_bound_witness(UINT_MAX),
         m_upper_bound_witness(UINT_MAX),
         m_associated_with_row(associated_with_row) {}
-    
-    ul_pair(const ul_pair & o):
-        m_lower_bound_witness(o.m_lower_bound_witness),
-        m_upper_bound_witness(o.m_upper_bound_witness),
-        m_associated_with_row(o.m_associated_with_row) {}
+
     bool associated_with_row() const { return m_associated_with_row; }
 };
 
diff --git a/src/muz/rel/dl_bound_relation.h b/src/muz/rel/dl_bound_relation.h
index 7c6b1225b..69459e920 100644
--- a/src/muz/rel/dl_bound_relation.h
+++ b/src/muz/rel/dl_bound_relation.h
@@ -94,7 +94,6 @@ namespace datalog {
     struct uint_set2 {
         uint_set lt;
         uint_set le;
-        uint_set2(uint_set2 const& other):lt(other.lt), le(other.le) {}
         uint_set2() {}
         bool operator==(const uint_set2& other) const {
             return other.lt == lt && other.le == le;
@@ -120,7 +119,6 @@ namespace datalog {
 
     public:
         bound_relation(bound_relation_plugin& p, relation_signature const& s, bool is_empty);
-        bound_relation& operator=(bound_relation const& other);
 
         bool empty() const override { return m_empty; }
         void add_fact(const relation_fact & f) override;
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index e54453d38..423f0a71c 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -442,10 +442,6 @@ derivation::premise::premise (pred_transformer &pt, unsigned oidx,
             m_ovars.push_back(m.mk_const(sm.n2o(v->get_decl(), m_oidx))); 
 }
 
-derivation::premise::premise (const derivation::premise &p) :
-    m_pt (p.m_pt), m_oidx (p.m_oidx), m_summary (p.m_summary), m_must (p.m_must),
-    m_ovars (p.m_ovars) {}
-
 /// \brief Updated the summary.
 /// The new summary is over n-variables.
 void derivation::premise::set_summary (expr * summary, bool must,
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 89a183dfb..85eadc96b 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -756,7 +756,6 @@ class derivation {
     public:
         premise (pred_transformer &pt, unsigned oidx, expr *summary, bool must,
                  const ptr_vector<app> *aux_vars = nullptr);
-        premise (const premise &p);
 
         bool is_must() {return m_must;}
         expr * get_summary() {return m_summary.get ();}
diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h
index a8b1d57b4..46702efce 100644
--- a/src/muz/spacer/spacer_manager.h
+++ b/src/muz/spacer/spacer_manager.h
@@ -47,7 +47,6 @@ struct relation_info {
     expr_ref              m_body;
     relation_info(ast_manager& m, func_decl* pred, ptr_vector<func_decl> const& vars, expr* b):
         m_pred(pred, m), m_vars(m, vars.size(), vars.c_ptr()), m_body(b, m) {}
-    relation_info(relation_info const& other): m_pred(other.m_pred), m_vars(other.m_vars), m_body(other.m_body) {}
 };
 
 class unknown_exception {};
diff --git a/src/muz/transforms/dl_mk_karr_invariants.cpp b/src/muz/transforms/dl_mk_karr_invariants.cpp
index ac5dbab02..7476156b9 100644
--- a/src/muz/transforms/dl_mk_karr_invariants.cpp
+++ b/src/muz/transforms/dl_mk_karr_invariants.cpp
@@ -60,12 +60,6 @@ namespace datalog {
 
     mk_karr_invariants::~mk_karr_invariants() { }
 
-    matrix& matrix::operator=(matrix const& other) {
-        reset();
-        append(other);
-        return *this;
-    }
-
     void matrix::display_row(
         std::ostream& out, vector<rational> const& row, rational const& b, bool is_eq) {
         for (unsigned j = 0; j < row.size(); ++j) {
diff --git a/src/muz/transforms/dl_mk_karr_invariants.h b/src/muz/transforms/dl_mk_karr_invariants.h
index 061ecdb3c..ac1015d14 100644
--- a/src/muz/transforms/dl_mk_karr_invariants.h
+++ b/src/muz/transforms/dl_mk_karr_invariants.h
@@ -36,7 +36,6 @@ namespace datalog {
         bool_vector             eq;
         unsigned size() const { return A.size(); }
         void reset() { A.reset(); b.reset(); eq.reset(); }
-        matrix& operator=(matrix const& other);
         void append(matrix const& other) { A.append(other.A); b.append(other.b); eq.append(other.eq); }
         void display(std::ostream& out) const;
         static void display_row(
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index d7a27fbb7..d70b5b254 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -374,7 +374,7 @@ namespace opt {
         smt::theory_var v = get_optimizer().add_objective(term);
         TRACE("opt", tout << v << " " << mk_pp(term, m) << "\n";);
         m_objective_vars.push_back(v);
-        m_objective_values.push_back(inf_eps(rational(-1), inf_rational()));
+        m_objective_values.push_back(inf_eps(rational::minus_one(), inf_rational()));
         m_objective_terms.push_back(term);
         m_valid_objectives.push_back(true);
         m_models.push_back(nullptr);
diff --git a/src/qe/qe.h b/src/qe/qe.h
index 9bb8da08f..6a50c0a71 100644
--- a/src/qe/qe.h
+++ b/src/qe/qe.h
@@ -229,10 +229,8 @@ namespace qe {
     class def_vector {
         func_decl_ref_vector m_vars;
         expr_ref_vector      m_defs;
-        def_vector& operator=(def_vector const& other);
     public:
         def_vector(ast_manager& m): m_vars(m), m_defs(m) {}
-        def_vector(def_vector const& other): m_vars(other.m_vars), m_defs(other.m_defs) {}
         void push_back(func_decl* v, expr* e) {
             m_vars.push_back(v);
             m_defs.push_back(e);
diff --git a/src/sat/sat_clause.h b/src/sat/sat_clause.h
index 4b5ddf618..045ba9a95 100644
--- a/src/sat/sat_clause.h
+++ b/src/sat/sat_clause.h
@@ -163,16 +163,6 @@ namespace sat {
     public:
         explicit clause_wrapper(literal l1, literal l2):m_l1_idx(l1.to_uint()), m_l2_idx(l2.to_uint()) {}
         explicit clause_wrapper(clause & c):m_cls(&c), m_l2_idx(null_literal.to_uint()) {}
-        clause_wrapper& operator=(clause_wrapper const& other) {
-            if (other.is_binary()) {
-                m_l1_idx = other.m_l1_idx;
-            }
-            else {
-                m_cls = other.m_cls;
-            }
-            m_l2_idx = other.m_l2_idx;
-            return *this;
-        }
 
         bool is_binary() const { return m_l2_idx != null_literal.to_uint(); }
         unsigned size() const { return is_binary() ? 2 : m_cls->size(); }
diff --git a/src/sat/sat_cutset.h b/src/sat/sat_cutset.h
index fdc1366d9..cb97c41d4 100644
--- a/src/sat/sat_cutset.h
+++ b/src/sat/sat_cutset.h
@@ -50,19 +50,6 @@ namespace sat {
             m_elems[1] = m_elems[2] = m_elems[3] = m_elems[4] = 0;
         }
 
-        cut(cut const& other) {
-            *this = other;
-        }
-
-        cut& operator=(cut const& other) { 
-            m_filter = other.m_filter;
-            m_size = other.m_size;
-            m_table = other.m_table;
-            m_dont_care = other.m_dont_care;
-            for (unsigned i = 0; i < m_size; ++i) m_elems[i] = other.m_elems[i];
-            return *this;
-        }
-
         cut_val eval(cut_eval const& env) const;
 
         unsigned size() const { return m_size; }
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index 88a2ad935..7ebbf5339 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -176,12 +176,6 @@ namespace sat {
             for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
             return *this;
         }
-        literal_set& operator=(literal_set const& other) {
-            if (this != &other) {
-                m_set = other.m_set;
-            }
-            return *this;
-        }
 
         void insert(literal l) { m_set.insert(l.index()); }
         void remove(literal l) { m_set.remove(l.index()); }
diff --git a/src/smt/smt_b_justification.h b/src/smt/smt_b_justification.h
index 826587353..ae01a389d 100644
--- a/src/smt/smt_b_justification.h
+++ b/src/smt/smt_b_justification.h
@@ -41,10 +41,6 @@ namespace smt {
         b_justification():
             m_data(reinterpret_cast<void*>(static_cast<size_t>(AXIOM))) {}
 
-        b_justification(b_justification const & source):
-            m_data(source.m_data) {
-        }
-
         explicit b_justification(clause * c):
             m_data(TAG(void*, c, CLAUSE)) {
         }
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index b6b810b5f..482209596 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -157,18 +157,6 @@ namespace smt {
             
             eq(unsigned id, expr_ref_vector& l, expr_ref_vector& r, dependency* d):
                 m_id(id), m_lhs(l), m_rhs(r), m_dep(d) {}
-            eq(eq const& other): m_id(other.m_id), m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {}
-            eq& operator=(eq const& other) {
-                if (this != &other) {
-                    m_lhs.reset(); 
-                    m_rhs.reset();
-                    m_lhs.append(other.m_lhs); 
-                    m_rhs.append(other.m_rhs); 
-                    m_dep = other.m_dep;
-                    m_id = other.m_id;
-                } 
-                return *this; 
-            }
             expr_ref_vector const& ls() const { return m_lhs; }
             expr_ref_vector const& rs() const { return m_rhs; }
             dependency* dep() const { return m_dep; }
@@ -205,21 +193,6 @@ namespace smt {
                 m_dep(dep) {
                 }
 
-            ne(ne const& other): 
-                m_l(other.m_l), m_r(other.m_r),
-                m_eqs(other.m_eqs), 
-                m_lits(other.m_lits), m_dep(other.m_dep) {}
-
-            ne& operator=(ne const& other) { 
-                if (this != &other) {
-                    m_l = other.m_l;
-                    m_r = other.m_r;
-                    m_eqs.reset();  m_eqs.append(other.m_eqs);
-                    m_lits.reset(); m_lits.append(other.m_lits); 
-                    m_dep = other.m_dep; 
-                }
-                return *this; 
-            }            
             vector<decomposed_eq> const& eqs() const { return m_eqs; }
             decomposed_eq const& operator[](unsigned i) const { return m_eqs[i]; }
 
@@ -239,18 +212,7 @@ namespace smt {
                 m_contains(c), 
                 m_len_gt(len_gt),
                 m_dep(dep) {}
-            nc(nc const& other):
-                m_contains(other.m_contains), 
-                m_len_gt(other.m_len_gt),
-                m_dep(other.m_dep) {}
-            nc& operator=(nc const& other) {
-                if (this != &other) {
-                    m_contains = other.m_contains;
-                    m_dep = other.m_dep;
-                    m_len_gt = other.m_len_gt;
-                }
-                return *this;
-            }
+
             dependency* deps() const { return m_dep; }
             expr_ref const& contains() const { return m_contains; }
             literal len_gt() const { return m_len_gt; }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index b80a5e3e7..9cb92f4cc 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -212,11 +212,6 @@ public:
     eautomaton * get_automaton() const { return aut; }
     expr * get_regex_term() const { return re_term; }
     bool get_polarity() const { return polarity; }
-
-    virtual ~regex_automaton_under_assumptions() {
-        // don't free str_in_re or aut;
-        // they are managed separately
-    }
 };
 
 class char_union_find {
diff --git a/src/smt/watch_list.h b/src/smt/watch_list.h
index 9c05fa6ce..0b49f0cca 100644
--- a/src/smt/watch_list.h
+++ b/src/smt/watch_list.h
@@ -85,7 +85,7 @@ namespace smt {
             m_data(nullptr) {
         }
 
-        watch_list(watch_list && other) : m_data(nullptr) {
+        watch_list(watch_list && other) noexcept : m_data(nullptr) {
             std::swap(m_data, other.m_data);
         }
         
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 1cb71e99b..76c31b1fd 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -173,9 +173,6 @@ class parallel_tactic : public tactic {
         cube_var(expr_ref_vector const& c, expr_ref_vector const& vs):
             m_vars(vs), m_cube(c) {}
 
-        cube_var(cube_var const& other):
-            m_vars(other.m_vars), m_cube(other.m_cube) {}
-
         cube_var operator()(ast_translation& tr) {
             expr_ref_vector vars(tr(m_vars));
             expr_ref_vector cube(tr(m_cube));
diff --git a/src/tactic/sls/bvsls_opt_engine.h b/src/tactic/sls/bvsls_opt_engine.h
index 1f082823f..c6b3857af 100644
--- a/src/tactic/sls/bvsls_opt_engine.h
+++ b/src/tactic/sls/bvsls_opt_engine.h
@@ -38,15 +38,6 @@ public:
         lbool is_sat;
         expr_ref optimum;
         optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {}
-        optimization_result& operator=(optimization_result const& other) {
-            is_sat = other.is_sat;
-            optimum = other.optimum;
-            return *this;
-        }
-        optimization_result(optimization_result const& other):
-            is_sat(other.is_sat),
-            optimum(other.optimum) {
-        }
     };
 
     optimization_result optimize(expr_ref const & objective, model_ref initial_model = model_ref(), bool maximize=true);
diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h
index 82ba38c21..5e12faf96 100644
--- a/src/tactic/sls/sls_tracker.h
+++ b/src/tactic/sls/sls_tracker.h
@@ -37,27 +37,10 @@ class sls_tracker {
     unsigned              m_random_bits;
     unsigned              m_random_bits_cnt;
     mpz                   m_zero, m_one, m_two;
-        
-    struct value_score { 
+
+    struct value_score {
     value_score() : m(nullptr), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {};
-        value_score(value_score && other) :
-            m(other.m),
-            value(std::move(other.value)),
-            score(other.score),
-            score_prune(other.score_prune),
-            has_pos_occ(other.has_pos_occ),
-            has_neg_occ(other.has_neg_occ),
-            distance(other.distance),
-            touched(other.touched) {}
         ~value_score() { if (m) m->del(value); }
-        void operator=(value_score && other) {
-            this->~value_score();
-            new (this) value_score(std::move(other));
-        }
-        value_score& operator=(value_score& other) {
-            UNREACHABLE();
-            return *this;
-        }
         unsynch_mpz_manager * m;
         mpz value;
         double score;
diff --git a/src/util/array_map.h b/src/util/array_map.h
index 91d226dab..6fefbfcc8 100644
--- a/src/util/array_map.h
+++ b/src/util/array_map.h
@@ -76,7 +76,6 @@ class array_map {
 public:
 
     array_map() = default;
-    array_map(array_map&&) noexcept = default;
     array_map(Plugin const & p) : m_plugin(p) {}
 
     ~array_map() { really_flush(); }
diff --git a/src/util/hwf.h b/src/util/hwf.h
index f2afbee63..4e1081ebf 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -27,7 +27,6 @@ Revision History:
 class hwf {
     friend class hwf_manager;
     double value;
-    hwf & operator=(hwf const & other) { UNREACHABLE(); return *this; }
     uint64_t get_raw() const {
       uint64_t n;
       SASSERT(sizeof(n) == sizeof(value));
@@ -35,8 +34,8 @@ class hwf {
       return n;
     }
 
-public:    
-    void swap(hwf & other) { double t = value; value = other.value; other.value = t; }
+public:
+    void swap(hwf & other) { std::swap(value, other.value); }
 };
 
 
diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h
index d29aa629e..b28a6d794 100644
--- a/src/util/inf_eps_rational.h
+++ b/src/util/inf_eps_rational.h
@@ -68,15 +68,7 @@ class inf_eps_rational {
         return s;
     }
 
-    inf_eps_rational():
-        m_infty(),
-        m_r()
-    {}
-
-    inf_eps_rational(const inf_eps_rational & r): 
-        m_infty(r.m_infty),
-        m_r(r.m_r)
-     {}
+    inf_eps_rational() = default;
 
     explicit inf_eps_rational(int n):
         m_infty(),
@@ -93,8 +85,6 @@ class inf_eps_rational {
         m_r(r) {
     }
 
-    ~inf_eps_rational() {}
-
     /**
        \brief Set inf_eps_rational to 0.
     */
@@ -163,13 +153,6 @@ class inf_eps_rational {
         return inf_eps_rational(rational::one(), Numeral::zero());
     }
 
-
-    inf_eps_rational & operator=(const inf_eps_rational & r) {
-        m_infty = r.m_infty;
-        m_r = r.m_r;
-        return *this;
-    }
-
     inf_eps_rational & operator=(const Numeral & r) {
         m_infty.reset();
         m_r = r;
diff --git a/src/util/inf_int_rational.h b/src/util/inf_int_rational.h
index c77617320..458843cb0 100644
--- a/src/util/inf_int_rational.h
+++ b/src/util/inf_int_rational.h
@@ -55,11 +55,6 @@ class inf_int_rational {
         m_second(0)
      {}
 
-    inf_int_rational(const inf_int_rational & r): 
-        m_first(r.m_first),
-        m_second(r.m_second)
-     {}
-
     explicit inf_int_rational(int n):
         m_first(rational(n)),
         m_second(0)
@@ -84,8 +79,6 @@ class inf_int_rational {
         m_second(i) {
     }
 
-    ~inf_int_rational() {}
-
     /**
        \brief Set inf_int_rational to 0.
     */
@@ -128,12 +121,6 @@ class inf_int_rational {
 
     rational const & get_first() const { return m_first; }
 
-    inf_int_rational & operator=(const inf_int_rational & r) {
-        m_first = r.m_first;
-        m_second = r.m_second;
-        return *this;
-    }
-
     inf_int_rational & operator=(const rational & r) {
         m_first = r;
         m_second = 0;
@@ -165,8 +152,6 @@ class inf_int_rational {
         return *this; 
     }
 
-
-
     inf_int_rational & operator-=(const inf_int_rational & r) { 
         m_first  -= r.m_first;
         m_second -= r.m_second;
diff --git a/src/util/inf_rational.h b/src/util/inf_rational.h
index 86e04543c..fb8a71e5f 100644
--- a/src/util/inf_rational.h
+++ b/src/util/inf_rational.h
@@ -93,8 +93,6 @@ class inf_rational {
         m_second(i) {
     }
 
-    ~inf_rational() {}
-
     /**
        \brief Set inf_rational to 0.
     */
@@ -137,12 +135,6 @@ class inf_rational {
 
     rational const & get_first() const { return m_first; }
 
-    inf_rational & operator=(const inf_rational & r) {
-        m_first = r.m_first;
-        m_second = r.m_second;
-        return *this;
-    }
-
     inf_rational & operator=(const rational & r) {
         m_first = r;
         m_second.reset();
diff --git a/src/util/mpq.h b/src/util/mpq.h
index a9e6063a3..513dac36e 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -29,7 +29,6 @@ class mpq {
 public:
     mpq(int v):m_num(v), m_den(1) {}
     mpq():m_den(1) {}
-    mpq(mpq &&) = default;
     mpq & operator=(mpq const &) = delete;
     void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
     mpz const & numerator() const { return m_num; }
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 248048888..65380d281 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -98,16 +98,10 @@ class mpz {
     friend class mpbq;
     friend class mpbq_manager;
     friend class mpz_stack;
-    mpz & operator=(mpz const & other) { UNREACHABLE(); return *this; }
 public:
     mpz(int v):m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {}
     mpz():m_val(0), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {}
     mpz(mpz_type* ptr): m_val(0), m_kind(mpz_small), m_owner(mpz_ext), m_ptr(ptr) { SASSERT(ptr);}
-    mpz(mpz && other) noexcept : m_val(other.m_val), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {
-        std::swap(m_ptr, other.m_ptr);
-        m_owner = other.m_owner;
-        m_kind = other.m_kind;
-    }
     void swap(mpz & other) { 
         std::swap(m_val, other.m_val);
         std::swap(m_ptr, other.m_ptr);
diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h
index 6b00f894f..04ae9e412 100644
--- a/src/util/obj_ref.h
+++ b/src/util/obj_ref.h
@@ -83,11 +83,13 @@ public:
         return *this;
     }
     
-    obj_ref & operator=(obj_ref & n) {
+    obj_ref & operator=(const obj_ref & n) {
         SASSERT(&m_manager == &n.m_manager);
-        n.inc_ref();
-        dec_ref();
-        m_obj = n.m_obj;
+        if (m_obj != n.m_obj) {
+            dec_ref();
+            m_obj = n.m_obj;
+            inc_ref();
+        }
         return *this;
     }
 
diff --git a/src/util/optional.h b/src/util/optional.h
index b9687df8c..50a2148d1 100644
--- a/src/util/optional.h
+++ b/src/util/optional.h
@@ -22,39 +22,31 @@ Revision History:
 
 template<class T>
 class optional {
-    T* m_obj;
-    char m_initialized;
-
-    void construct(const T & val) {
-        m_initialized = 1;
-        m_obj = alloc(T, val);
-    }
+    T* m_obj = nullptr;
 
     void destroy() {
-        if (m_initialized == 1) {
-            dealloc(m_obj);
-            m_obj = nullptr;
-        }
-        m_initialized = 0;
+        dealloc(m_obj);
+        m_obj = nullptr;
     }
 
 public:
-    optional():
-        m_obj(nullptr), m_initialized(0) {}
+    optional() {}
 
     explicit optional(const T & val) {
-        construct(val);
+        m_obj = alloc(T, val);
     }
 
-    optional(T && val) noexcept : m_obj(nullptr), m_initialized(0) {
+    explicit optional(T && val) {
+        m_obj = alloc(T, std::move(val));
+    }
+
+    optional(optional<T> && val) noexcept {
         std::swap(m_obj, val.m_obj);
-        std::swap(m_initialized, val.m_initialized);
     }
 
-    optional(const optional<T> & val):
-        m_initialized(0) {
-        if (val.m_initialized == 1) {
-            construct(*val);
+    optional(const optional<T> & val) {
+        if (val.m_obj) {
+            m_obj = alloc(T, *val);
         }
     }
 
@@ -64,56 +56,54 @@ public:
     
     static optional const & undef() { static optional u;  return u; }
  
-    bool initialized() const { return m_initialized == 1; }
-    operator bool() const { return m_initialized == 1; }
-    bool operator!() const { return m_initialized == 0; }
+    bool initialized() const { return m_obj; }
+    operator bool() const { return m_obj; }
+    bool operator!() const { return !m_obj; }
     
     T * get() const { 
-        if (m_initialized == 1) {
-            return m_obj;
-        }
-        else {
-            return 0;
-        }
+        return m_obj;
     }
 
     void set_invalid() {
-        if (m_initialized == 1) {
-            destroy();
-        }
+        destroy();
     }
 
     T * operator->() {
-        SASSERT(m_initialized==1);
+        SASSERT(m_obj);
         return m_obj;
     }
 
     T const * operator->() const {
-        SASSERT(m_initialized==1);
+        SASSERT(m_obj);
         return m_obj;
     }
 
     const T & operator*() const {
-        SASSERT(m_initialized==1);
+        SASSERT(m_obj);
         return *m_obj;
     }
     
     T & operator*() {
-        SASSERT(m_initialized==1);
+        SASSERT(m_obj);
         return *m_obj;
     }
 
     optional & operator=(const T & val) {
         destroy();
-        construct(val);
+        m_obj = alloc(T, val);
         return * this;
     }
 
+    optional & operator=(optional && val) {
+        std::swap(m_obj, val.m_obj);
+        return *this;
+    }
+
     optional & operator=(const optional & val) {
         if (&val != this) {
             destroy();
-            if (val.m_initialized) {
-                construct(*val);
+            if (val.m_obj) {
+                m_obj = alloc(T, *val);
             }
         }
         return *this;
@@ -135,8 +125,6 @@ public:
     optional():m_ptr(nullptr) {}
 
     explicit optional(T * val):m_ptr(val) {}
-    
-    optional(const optional & val):m_ptr(val.m_ptr) {}
 
     static optional const & undef() { return m_undef; }
 
diff --git a/src/util/rational.h b/src/util/rational.h
index f37336e4d..cd627d27f 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -40,7 +40,7 @@ public:
     rational() {}
     
     rational(rational const & r) { m().set(m_val, r.m_val); }
-    rational(rational&&) = default;
+    rational(rational&&) noexcept = default;
 
     explicit rational(int n) { m().set(m_val, n); }
 
@@ -131,7 +131,9 @@ public:
     rational const & get_rational() const { return *this; }
 
     rational const & get_infinitesimal() const { return m_zero; }
-    
+
+    rational & operator=(rational&&) = default;
+
     rational & operator=(rational const & r) {
         m().set(m_val, r.m_val);
         return *this;
diff --git a/src/util/ref.h b/src/util/ref.h
index c9ba6697f..764eb416b 100644
--- a/src/util/ref.h
+++ b/src/util/ref.h
@@ -17,18 +17,19 @@ Revision History:
 
 --*/
 #pragma once
+#include <utility>
 
 template<typename T>
 class ref {
     T * m_ptr;
 
-    void inc_ref() { 
+    void inc_ref() {
         if (m_ptr) {
             m_ptr->inc_ref();
         }
     }
 
-    void dec_ref() { 
+    void dec_ref() {
         if (m_ptr) {
             m_ptr->dec_ref();
         }
@@ -49,7 +50,10 @@ public:
         inc_ref();
     }
 
-   ref (ref && r): m_ptr (r.detach ()) {}
+   ref (ref && r) noexcept : m_ptr(nullptr) {
+       std::swap(m_ptr, r.m_ptr);
+   }
+
     ~ref() {
         dec_ref();
     }
diff --git a/src/util/ref_pair_vector.h b/src/util/ref_pair_vector.h
index 3e2adde6e..fb8769a53 100644
--- a/src/util/ref_pair_vector.h
+++ b/src/util/ref_pair_vector.h
@@ -49,14 +49,10 @@ public:
 
     ref_pair_vector_core(Ref const & r = Ref()):Ref(r) {}
 
-    ref_pair_vector_core(ref_pair_vector_core && other) :
-        Ref(std::move(other)),
-        m_nodes(std::move(other.m_nodes)) {}
-    
     ~ref_pair_vector_core() {
         dec_range_ref(m_nodes.begin(), m_nodes.end());
     }
-    
+
     void reset() {
         dec_range_ref(m_nodes.begin(), m_nodes.end());
         m_nodes.reset();
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index fd8ce43d9..8edb41c3f 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -55,7 +55,7 @@ public:
         append(other);
     }
 
-    ref_vector_core(ref_vector_core &&) = default;
+    ref_vector_core(ref_vector_core &&) noexcept = default;
     
     ~ref_vector_core() {
         dec_range_ref(m_nodes.begin(), m_nodes.end());
@@ -241,7 +241,7 @@ public:
         this->append(other);
     }
 
-    ref_vector(ref_vector &&) = default;
+    ref_vector(ref_vector &&) noexcept = default;
 
     ref_vector(TManager & m, unsigned sz, T * const * data):
         super(ref_manager_wrapper<T, TManager>(m)) {
@@ -324,8 +324,10 @@ public:
         return *this;
     }
     
-    // prevent abuse:
-    ref_vector & operator=(ref_vector const & other) = delete;
+    ref_vector & operator=(ref_vector const & other) {
+        set(other);
+        return *this;
+    }
 
     ref_vector & operator=(ref_vector && other) = default;
 
diff --git a/src/util/s_integer.h b/src/util/s_integer.h
index 775384a5d..506b4f0a3 100644
--- a/src/util/s_integer.h
+++ b/src/util/s_integer.h
@@ -42,7 +42,6 @@ public:
 
 public:
     s_integer(): m_val(0) {}
-    s_integer(const s_integer & r):m_val(r.m_val) {}
     explicit s_integer(int n):m_val(n) {}
     struct i64 {};
     explicit s_integer(int64_t i, i64):m_val(static_cast<int>(i)) {}
@@ -67,7 +66,6 @@ public:
     s_integer const& get_infinitesimal() const { return zero(); }
     static bool is_rational() { return true; }
     s_integer const& get_rational() const { return *this; } 
-    s_integer & operator=(const s_integer & r) { m_val = r.m_val; return *this; }
     friend inline s_integer numerator(const s_integer & r) { return r; }
     friend inline s_integer denominator(const s_integer & r) { return one(); }
     s_integer & operator+=(const s_integer & r) { m_val += r.m_val; return *this; }
diff --git a/src/util/stacked_value.h b/src/util/stacked_value.h
index 5c1580770..478f64d43 100644
--- a/src/util/stacked_value.h
+++ b/src/util/stacked_value.h
@@ -58,17 +58,6 @@ public:
     stacked_value(const T&& m) {
         m_value = std::move(m);
     }
-    
-    T& operator=(T arg) { // copy/move constructor
-        m_value = arg;
-        return m_value;
-    }
-
-    stacked_value& operator=(stacked_value const& other) {
-        m_value = other.m_value;
-        m_stack = other.m_stack;
-        return *this;
-    }
 
     operator T&() {
         return m_value;
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index 46a606e8f..3f0d45856 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -198,12 +198,6 @@ public:
         bool operator!=(iterator const& it) const { return m_index != it.m_index; }
         iterator & operator++() { ++m_index; scan(); return *this; }
         iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
-        iterator & operator=(iterator const& other) { 
-            m_set = other.m_set;
-            m_index = other.m_index;
-            m_last = other.m_last;
-            return *this;
-        }
     };
 
     iterator const begin() const { return iterator(*this, false); }
@@ -267,12 +261,6 @@ public:
         }
     }
     
-    tracked_uint_set& operator=(tracked_uint_set const& other) {
-        m_in_set = other.m_in_set;
-        m_set = other.m_set;
-        return *this;
-    }
-    
     bool contains(unsigned v) const {
         return v < m_in_set.size() && m_in_set[v] != 0;
     }
diff --git a/src/util/vector.h b/src/util/vector.h
index 010c8d7ac..1df5472f1 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -69,7 +69,7 @@ class vector {
             m_data            = reinterpret_cast<T *>(mem);
         }
         else {
-            //static_assert(std::is_nothrow_move_constructible<T>::value, "");
+            static_assert(std::is_nothrow_move_constructible<T>::value, "");
             SASSERT(capacity() > 0);
             SZ old_capacity = reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX];
             SZ old_capacity_T = sizeof(T) * old_capacity + sizeof(SZ) * 2;