mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Replace user-defined swap with C++11 move semantics for covert move patterns (#8543)

Browse source
This commit is contained in:
Copilot 2026-02-09 17:52:30 +00:00 • committed by Nikolaj Bjorner
parent c50d41a6e8
commit 58431ec158
6 changed files with 28 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/nlsat/nlsat_scoped_literal_vector.h
View file

@ -29,6 +29,24 @@ namespace nlsat {
public:
scoped_literal_vector(solver & s):m_solver(s) {}
~scoped_literal_vector() { reset(); }
scoped_literal_vector(scoped_literal_vector && other) noexcept = default;
// Move assignment operator
scoped_literal_vector & operator=(scoped_literal_vector && other) noexcept {
if (this != &other) {
SASSERT(&m_solver == &other.m_solver);
reset(); // dec_ref our current literals
m_lits = std::move(other.m_lits); // take ownership of other's literals
// other.m_lits is now empty
}
return *this;
}
// Delete copy operations to prevent accidental copies
scoped_literal_vector(scoped_literal_vector const &) = delete;
scoped_literal_vector & operator=(scoped_literal_vector const &) = delete;
unsigned size() const { return m_lits.size(); }
bool empty() const { return m_lits.empty(); }
literal operator[](unsigned i) const { return m_lits[i]; }