mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

expr move semantics supported via ast (#5190)

Browse source
This commit is contained in:
Zachary Wimer 2021-04-15 13:37:31 -07:00 • committed by GitHub
parent 21e59f7c6e
commit 239ace4353
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/api/c++/z3++.h
View file

@ -497,6 +497,7 @@ namespace z3 {
ast(context & c):object(c), m_ast(0) {}
ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
ast(ast && s) noexcept : object(std::forward<object>(s)), m_ast(s.m_ast) { s.m_ast = nullptr; }
~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
operator Z3_ast() const { return m_ast; }
operator bool() const { return m_ast != 0; }
@ -508,6 +509,12 @@ namespace z3 {
m_ast = s.m_ast;
return *this;
}
ast & operator=(ast && s) noexcept {
object::operator=(std::forward<object>(s));
m_ast = s.m_ast;
s.m_ast = nullptr;
return *this;
}
Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
friend std::ostream & operator<<(std::ostream & out, ast const & n);