mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
remove a bunch of constructors to avoid copies
still not enough to guarantee that vector::expand doesnt copy (WIP)
This commit is contained in:
parent
98b5abb1d4
commit
7ac2791482
16 changed files with 66 additions and 83 deletions
|
@ -1,6 +1,5 @@
|
|||
|
||||
#ifndef JUSTIFIED_EXPR_H_
|
||||
#define JUSTIFIED_EXPR_H_
|
||||
#pragma once
|
||||
|
||||
#include "ast/ast.h"
|
||||
|
||||
|
@ -40,6 +39,15 @@ public:
|
|||
m.inc_ref(m_proof);
|
||||
}
|
||||
|
||||
justified_expr(justified_expr && other):
|
||||
m(other.m),
|
||||
m_fml(nullptr),
|
||||
m_proof(nullptr)
|
||||
{
|
||||
std::swap(m_fml, other.m_fml);
|
||||
std::swap(m_proof, other.m_proof);
|
||||
}
|
||||
|
||||
~justified_expr() {
|
||||
m.dec_ref(m_fml);
|
||||
m.dec_ref(m_proof);
|
||||
|
@ -50,5 +58,3 @@ public:
|
|||
expr* get_fml() const { return m_fml; }
|
||||
proof* get_proof() const { return m_proof; }
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -221,16 +221,6 @@ struct nnf::imp {
|
|||
m_cache_result(cache_res),
|
||||
m_spos(spos) {
|
||||
}
|
||||
frame(frame && other):
|
||||
m_curr(std::move(other.m_curr)),
|
||||
m_i(other.m_i),
|
||||
m_pol(other.m_pol),
|
||||
m_in_q(other.m_in_q),
|
||||
m_new_child(other.m_new_child),
|
||||
m_cache_result(other.m_cache_result),
|
||||
m_spos(other.m_spos) {
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
// There are four caches:
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue