diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h index 732ce9251..132f6e7d9 100644 --- a/src/math/lp/explanation.h +++ b/src/math/lp/explanation.h @@ -124,14 +124,12 @@ public: struct equality { lp::lpvar i, j; lp::explanation e; - equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e):i(i),j(j),e(e) {} }; struct fixed_equality { lp::lpvar v; rational k; lp::explanation e; - fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e):v(v),k(k),e(e) {} }; } diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 66505c698..28dc9a9e7 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -423,8 +423,7 @@ namespace nla { c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, rational(0), dep); // propagate fixed equality - auto exp = get_explanation(dep); - c().add_fixed_equality(m.var(), rational(0), exp); + c().add_fixed_equality(m.var(), rational(0), get_explanation(dep)); } void monomial_bounds::propagate_fixed(monic const& m, rational const& k) { @@ -433,8 +432,7 @@ namespace nla { c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep); // propagate fixed equality - auto exp = get_explanation(dep); - c().add_fixed_equality(m.var(), k, exp); + c().add_fixed_equality(m.var(), k, get_explanation(dep)); } void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) { @@ -447,8 +445,7 @@ namespace nla { c().lra.update_column_type_and_bound(j, lp::lconstraint_kind::EQ, mpq(0), dep); if (k == 1) { - lp::explanation exp = get_explanation(dep); - c().add_equality(m.var(), w, exp); + c().add_equality(m.var(), w, get_explanation(dep)); } } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index fed6dfe72..5ccbc17e0 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -443,8 +443,8 @@ public: vector const& fixed_equalities() const { return m_fixed_equalities; } bool should_check_feasible() const { return m_check_feasible; } - void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); } - void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); } + void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation && e) { m_fixed_equalities.push_back({v, k, std::move(e)}); } + void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation && e) { m_equalities.push_back({i, j, std::move(e)}); } bool throttle_enabled() const { return m_throttle_enabled; } nla_throttle& throttle() { return m_throttle; } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index c5744e2b4..09f874e78 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -4651,7 +4651,6 @@ namespace sat { } add_assumption(lit); } - m_antecedents.insert(lit.var(), s); if (unfixed.contains(lit.var())) { literal_vector cons; cons.push_back(lit); @@ -4659,8 +4658,9 @@ namespace sat { cons.push_back(to_literal(idx)); } unfixed.remove(lit.var()); - conseq.push_back(cons); + conseq.push_back(std::move(cons)); } + m_antecedents.insert(lit.var(), std::move(s)); return true; } diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 7ea89b0df..bdb6c18e5 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -60,7 +60,7 @@ namespace smt { else { justify(lit, s); } - m_antecedents.insert(lit.var(), s); + m_antecedents.insert(lit.var(), std::move(s)); bool found = false; if (m_var2val.contains(e)) { found = true; @@ -478,7 +478,6 @@ namespace smt { else { justify(lit, s); } - m_antecedents.insert(lit.var(), s); if (_nasms.contains(lit.index())) { expr_ref_vector core(m); for (auto v : s) @@ -487,6 +486,7 @@ namespace smt { cores.push_back(core); min_core_size = std::min(min_core_size, core.size()); } + m_antecedents.insert(lit.var(), std::move(s)); } } diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp index 68f2142ec..1f0b3fb75 100644 --- a/src/test/hashtable.cpp +++ b/src/test/hashtable.cpp @@ -99,12 +99,15 @@ static void tst2() { } static void tst3() { - int_set h1; + int_set h1, h2; h1.insert(10); h1.insert(20); h1.insert(30); h1.erase(20); - int_set h2(h1); + h2.insert(10); + h2.insert(20); + h2.insert(30); + h2.erase(20); ENSURE(h1.contains(10)); ENSURE(!h1.contains(20)); ENSURE(h1.contains(30)); @@ -129,17 +132,11 @@ void test_hashtable_constructors() { VERIFY(ht.size() == 0); VERIFY(ht.capacity() == DEFAULT_HASHTABLE_INITIAL_CAPACITY); - // Copy constructor - hashtable ht_copy(ht); - VERIFY(ht_copy.empty()); - VERIFY(ht_copy.size() == 0); - VERIFY(ht_copy.capacity() == ht.capacity()); - // Move constructor hashtable ht_move(std::move(ht)); VERIFY(ht_move.empty()); VERIFY(ht_move.size() == 0); - VERIFY(ht_move.capacity() == ht_copy.capacity()); + VERIFY(ht_move.capacity() == DEFAULT_HASHTABLE_INITIAL_CAPACITY); } void test_hashtable_insert() { diff --git a/src/util/checked_int64.h b/src/util/checked_int64.h index 14d716b0d..41ac88ef7 100644 --- a/src/util/checked_int64.h +++ b/src/util/checked_int64.h @@ -43,6 +43,11 @@ public: checked_int64() = default; checked_int64(int64_t v): m_value(v) {} + checked_int64(checked_int64 const& other) = default; + checked_int64(checked_int64&&) = default; + + checked_int64& operator=(checked_int64 const& other) = default; + checked_int64& operator=(checked_int64&&) = default; bool is_zero() const { return m_value == 0; } bool is_pos() const { return m_value > 0; } diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 5807e2898..4bd371795 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -624,7 +624,12 @@ public: core_hashtable& operator=(core_hashtable && other) { if (this == &other) return *this; delete_table(); - std::swap(*this, other); + m_table = other.m_table; + m_capacity = other.m_capacity; + m_size = other.m_size; + m_num_deleted = other.m_num_deleted; + HS_CODE(m_st_collision = other.m_st_collision); + other.m_table = nullptr; return *this; } @@ -703,6 +708,10 @@ public: HashProc const & h = HashProc(), EqProc const & e = EqProc()): core_hashtable, HashProc, EqProc>(initial_capacity, h, e) {} + hashtable(const hashtable & source) = delete; + hashtable(hashtable && source) noexcept = default; + hashtable& operator=(const hashtable & other) = default; + hashtable& operator=(hashtable && other) noexcept = default; }; template @@ -712,6 +721,10 @@ public: HashProc const & h = HashProc(), EqProc const & e = EqProc()): core_hashtable, HashProc, EqProc>(initial_capacity, h, e) {} + ptr_hashtable(const ptr_hashtable & source) = delete; + ptr_hashtable(ptr_hashtable && source) noexcept = default; + ptr_hashtable& operator=(const ptr_hashtable & other) = delete; + ptr_hashtable& operator=(ptr_hashtable && other) noexcept = default; }; /** @@ -723,6 +736,10 @@ public: typedef typename core_hashtable, ptr_hash, ptr_eq >::iterator iterator; ptr_addr_hashtable(unsigned initial_capacity = DEFAULT_HASHTABLE_INITIAL_CAPACITY): core_hashtable, ptr_hash, ptr_eq >(initial_capacity) {} + ptr_addr_hashtable(const ptr_addr_hashtable & source) = delete; + ptr_addr_hashtable(ptr_addr_hashtable && source) noexcept = default; + ptr_addr_hashtable& operator=(const ptr_addr_hashtable & other) = delete; + ptr_addr_hashtable& operator=(ptr_addr_hashtable && other) noexcept = default; iterator begin() const { UNREACHABLE(); @@ -748,4 +765,8 @@ public: HashProc const & h = HashProc(), EqProc const & e = EqProc()): core_hashtable, HashProc, EqProc>(initial_capacity, h, e) {} + int_hashtable(const int_hashtable & source) = delete; + int_hashtable(int_hashtable && source) noexcept = default; + int_hashtable& operator=(const int_hashtable & other) = delete; + int_hashtable& operator=(int_hashtable && other) noexcept = default; };