remove a few more copy constructors, though still not enough to enabl…

…e the assertion in vector

I give up for now; there are too many copies left for little return..

src/ast/justified_expr.h

@@ -39,7 +39,7 @@ class justified_expr {
         m.inc_ref(m_proof);
     }
 
-    justified_expr(justified_expr && other):
+    justified_expr(justified_expr && other) noexcept :
         m(other.m),
         m_fml(nullptr),
         m_proof(nullptr)

src/ast/recfun_decl_plugin.cpp

@@ -131,8 +131,6 @@ namespace recfun {
             path(nullptr), to_split(nullptr), to_unfold(to_unfold) {}
         branch(choice_lst const * path, ite_lst const * to_split, unfold_lst const * to_unfold) : 
             path(path), to_split(to_split), to_unfold(to_unfold) {}
-        branch(branch const & from) : 
-            path(from.path), to_split(from.to_split), to_unfold(from.to_unfold) {}
     };
 
     // state for computing cases from the RHS of a functions' definition

src/math/dd/dd_pdd.h

@@ -320,7 +320,7 @@ namespace dd {
     public:
         pdd(pdd_manager& pm): root(0), m(pm) { SASSERT(is_zero()); }
         pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); }
-        pdd(pdd && other): root(0), m(other.m) { std::swap(root, other.root); }
+        pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); }
         pdd& operator=(pdd const& other);
         ~pdd() { m.dec_ref(root); }
         pdd lo() const { return pdd(m.lo(root), m); }

src/math/lp/indexed_value.h

@@ -35,19 +35,6 @@ class indexed_value {
         m_value(v), m_index(i), m_other(other) {
     }
 
-    indexed_value(const indexed_value & iv) {
-        m_value = iv.m_value;
-        m_index = iv.m_index;
-        m_other = iv.m_other;
-    }
-
-    indexed_value & operator=(const indexed_value & right_side) {
-        m_value = right_side.m_value;
-        m_index = right_side.m_index;
-        m_other = right_side.m_other;
-        return *this;
-    }
-
     const T & value() const {
         return m_value;
     }

src/math/lp/numeric_pair.h

@@ -144,8 +144,6 @@ struct numeric_pair {
     explicit numeric_pair(const X & n) : x(n), y(0) {
     }
 
-    numeric_pair(const numeric_pair<T> & n) : x(n.x), y(n.y) {}
-
     template <typename X, typename Y>
     numeric_pair(X xp, Y yp) : x(convert_struct<T, X>::convert(xp)), y(convert_struct<T, Y>::convert(yp)) {}
 

src/math/simplex/model_based_opt.h

@@ -67,7 +67,6 @@ namespace opt {
         struct def {
             def(): m_div(1) {}
             def(row const& r, unsigned x);
-            def(def const& other): m_vars(other.m_vars), m_coeff(other.m_coeff), m_div(other.m_div) {}
             vector<var> m_vars;
             rational    m_coeff;
             rational    m_div; 

src/opt/maxsmt.h

@@ -64,8 +64,6 @@ namespace opt {
             void set_value(lbool t) { value = t; }
             bool is_true() const { return value == l_true; }
             soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
-            soft(soft const& other):s(other.s), weight(other.weight), value(other.value) {}
-            soft& operator=(soft const& other) { s = other.s; weight = other.weight; value = other.value; return *this; }            
         };
         ast_manager&     m;
         maxsat_context&  m_c;        

src/opt/pb_sls.cpp

@@ -77,16 +77,6 @@ namespace smt {
                 m_value(m),
                 m_eq(true)
             {}
-            clause(clause const& cls):
-                m_lits(cls.m_lits),
-                m_weights(cls.m_weights.m()),
-                m_k(cls.m_k),
-                m_value(cls.m_value),
-                m_eq(cls.m_eq) {
-                for (unsigned i = 0; i < cls.m_weights.size(); ++i) {
-                    m_weights.push_back(cls.m_weights[i]);
-                }
-            }
         };
 
         struct stats {

src/qe/qe_arrays.cpp

@@ -899,12 +899,8 @@ namespace qe {
             expr_ref_vector idx;
             expr_ref_vector val;
             vector<rational> rval;
-            idx_val(expr_ref_vector & idx, expr_ref_vector & val, vector<rational> const& rval): idx(idx), val(val), rval(rval) {}
-            idx_val& operator=(idx_val const& o) {
-                idx.reset(); val.reset(); rval.reset();
-                idx.append(o.idx); val.append(o.val); rval.append(o.rval);
-                return *this;
-            }
+            idx_val(expr_ref_vector && idx, expr_ref_vector && val, vector<rational> && rval):
+              idx(std::move(idx)), val(std::move(val)), rval(std::move(rval)) {}
         };
         ast_manager&                m;
         array_util                  m_arr_u;
@@ -1049,8 +1045,7 @@ namespace qe {
                 }
                 if (is_new) {
                     // new repr, val, and sel const
-                    vector<rational> rvals = to_num(vals);
-                    m_idxs.push_back(idx_val(idxs, vals, rvals));
+                    m_idxs.push_back(idx_val(std::move(idxs), std::move(vals), to_num(vals)));
                     app_ref c (m.mk_fresh_const ("sel", val_sort), m);
                     m_sel_consts.push_back (c);
                     // substitute sel term with new const

src/util/array_map.h

@@ -16,8 +16,7 @@ Module Name:
 Revision History:
 
 --*/
-#ifndef ARRAY_MAP_H_
-#define ARRAY_MAP_H_
+#pragma once
 
 #include "util/vector.h"
 #include "util/optional.h"
@@ -40,9 +39,9 @@ class array_map {
         entry(Key const & k, Data const & d, unsigned t): m_key(k), m_data(d), m_timestamp(t) {}
     };
 
-    unsigned                 m_timestamp;
-    unsigned                 m_garbage;
-    unsigned                 m_non_garbage;
+    unsigned                 m_timestamp = 0;
+    unsigned                 m_garbage = 0;
+    unsigned                 m_non_garbage = 0;
     static const unsigned    m_gc_threshold = 10000;
     vector<optional<entry>, CallDestructors > m_map;
     Plugin                   m_plugin;
@@ -76,7 +75,10 @@ class array_map {
 
 public:
 
-    array_map(Plugin const & p = Plugin()):m_timestamp(0), m_garbage(0), m_non_garbage(0), m_plugin(p) {}
+    array_map() = default;
+    array_map(array_map&&) noexcept = default;
+    array_map(Plugin const & p) : m_plugin(p) {}
+
     ~array_map() { really_flush(); }
 
     bool contains(Key const & k) const {
@@ -155,5 +157,3 @@ class array_map {
     }
 
 };
-
-#endif /* ARRAY_MAP_H_ */

src/util/inf_rational.h

@@ -17,8 +17,8 @@ Module Name:
 Revision History:
 
 --*/
-#ifndef INF_RATIONAL_H_
-#define INF_RATIONAL_H_
+#pragma once
+
 #include<stdlib.h>
 #include<string>
 #include "util/debug.h"
@@ -67,11 +67,6 @@ class inf_rational {
 
     inf_rational() {}
 
-    inf_rational(const inf_rational & r): 
-        m_first(r.m_first),
-        m_second(r.m_second)
-     {}
-
     explicit inf_rational(int n):
         m_first(rational(n)),
         m_second(rational())
@@ -470,5 +465,3 @@ inline inf_rational abs(const inf_rational & r) {
     }
     return result;
 }
-
-#endif /* INF_RATIONAL_H_ */

src/util/inf_s_integer.h

@@ -16,8 +16,7 @@ Module Name:
 Revision History:
 
 --*/
-#ifndef INF_S_INTEGER_H_
-#define INF_S_INTEGER_H_
+#pragma once
 
 #include "util/s_integer.h"
 #include "util/rational.h"
@@ -47,8 +46,6 @@ class inf_s_integer {
 
     inf_s_integer():m_first(0), m_second(0) {}
 
-    inf_s_integer(const inf_s_integer & r):m_first(r.m_first), m_second(r.m_second) {}
-
     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); }
     explicit inf_s_integer(s_integer const& r, bool pos_inf):m_first(r.get_int()), m_second(pos_inf ? 1 : -1) {}
@@ -345,7 +342,3 @@ inline inf_s_integer abs(const inf_s_integer & r) {
     }
     return result;
 }
-
-
-#endif /* INF_S_INTEGER_H_ */
-

src/util/obj_ref.h

@@ -16,8 +16,7 @@ Module Name:
 Revision History:
 
 --*/
-#ifndef OBJ_REF_H_
-#define OBJ_REF_H_
+#pragma once
 
 /**
    Smart pointer for T objects.
@@ -53,7 +52,7 @@ class obj_ref {
         inc_ref();
     }
 
-    obj_ref(obj_ref && other) : m_obj(nullptr), m_manager(other.m_manager) {
+    obj_ref(obj_ref && other) noexcept : m_obj(nullptr), m_manager(other.m_manager) {
         std::swap(m_obj, other.m_obj);
     }
 
@@ -146,5 +145,3 @@ inline void dec_range_ref(IT const & begin, IT const & end, TManager & m) {
         }
     }
 }
-
-#endif /* OBJ_REF_H_ */

src/util/ref_vector.h

@@ -191,6 +191,13 @@ class ref_vector_core : public Ref {
             push_back(data[i]);
     }
 
+    void operator=(ref_vector_core && other) {
+        if (this != &other) {
+            reset();
+            m_nodes = std::move(other.m_nodes);
+        }
+    }
+
     void swap(unsigned idx1, unsigned idx2) {
         std::swap(m_nodes[idx1], m_nodes[idx2]);
     }
@@ -234,7 +241,7 @@ class ref_vector : public ref_vector_core<T, ref_manager_wrapper<T, TManager> >
         this->append(other);
     }
 
-    ref_vector(ref_vector && other) : super(std::move(other)) {}
+    ref_vector(ref_vector &&) = default;
 
     ref_vector(TManager & m, unsigned sz, T * const * data):
         super(ref_manager_wrapper<T, TManager>(m)) {
@@ -320,6 +327,11 @@ class ref_vector : public ref_vector_core<T, ref_manager_wrapper<T, TManager> >
     // prevent abuse:
     ref_vector & operator=(ref_vector const & other) = delete;
 
+    ref_vector & operator=(ref_vector && other) {
+        super::operator=(std::move(other));
+        return *this;
+    }
+
     bool operator==(ref_vector const& other) const {
         if (other.size() != this->size()) return false;
         for (unsigned i = this->size(); i-- > 0; ) {

src/util/scoped_numeral.h

@@ -17,8 +17,7 @@ Module Name:
 Revision History:
 
 --*/
-#ifndef SCOPED_NUMERAL_H_
-#define SCOPED_NUMERAL_H_
+#pragma once
 
 template<typename Manager>
 class _scoped_numeral {
@@ -30,6 +29,7 @@ class _scoped_numeral {
 public:
     _scoped_numeral(Manager & m):m_manager(m) {}
     _scoped_numeral(_scoped_numeral const & n):m_manager(n.m_manager) { m().set(m_num, n.m_num); }
+    _scoped_numeral(_scoped_numeral &&) = default;
     ~_scoped_numeral() { m_manager.del(m_num); }
 
     Manager & m() const { return m_manager; }
@@ -189,5 +189,3 @@ class _scoped_numeral {
     }
 
 };
-
-#endif

src/util/scoped_numeral_vector.h

@@ -16,17 +16,24 @@ Module Name:
 Revision History:
 
 --*/
-#ifndef SCOPED_NUMERAL_VECTOR_H_
-#define SCOPED_NUMERAL_VECTOR_H_
+#pragma once
 
 #include "util/vector.h"
 
 template<typename Manager>
 class _scoped_numeral_vector : public svector<typename Manager::numeral> {
     Manager & m_manager;
-    _scoped_numeral_vector(_scoped_numeral_vector const & v);
 public:
     _scoped_numeral_vector(Manager & m):m_manager(m) {}
+
+    _scoped_numeral_vector(const _scoped_numeral_vector & other) : m_manager(other.m_manager) {
+        for (unsigned i = 0, e = other.size(); i != e; ++i) {
+            push_back((*this)[i]);
+        }
+    }
+
+    _scoped_numeral_vector(_scoped_numeral_vector&&) = default;
+
     ~_scoped_numeral_vector() {
         reset();
     }
@@ -66,5 +73,3 @@ class _scoped_numeral_vector : public svector<typename Manager::numeral> {
         svector<typename Manager::numeral>::resize(sz, 0);
     }
 };
-
-#endif

src/util/uint_set.h

@@ -16,8 +16,7 @@ Module Name:
 Revision History:
 
 --*/
-#ifndef UINT_SET_H_
-#define UINT_SET_H_
+#pragma once
 
 #include "util/util.h"
 #include "util/vector.h"
@@ -29,16 +28,6 @@ class uint_set : unsigned_vector {
 
     typedef unsigned data;
 
-    uint_set() {}
-
-    uint_set(const uint_set & source) {
-        for (unsigned i = 0; i < source.size(); ++i) {
-            push_back(source[i]);
-        }
-    }
-
-    ~uint_set() {}
-
     void swap(uint_set & other) {
         unsigned_vector::swap(other);
     }
@@ -384,6 +373,3 @@ inline std::ostream& operator<<(std::ostream& out, indexed_uint_set const& s) {
     for (unsigned i : s) out << i << " ";
     return out;
 }
-
-#endif /* UINT_SET_H_ */
-