mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

simplifications to refs

Browse source
This commit is contained in:
Nuno Lopes 2019-02-19 13:18:20 +00:00
parent 8e4ef19f45
commit edf0df634d
5 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ackermannization/lackr.cpp
View file

@ -122,7 +122,7 @@ bool lackr::ackr(app * const t1, app * const t2) {
TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";); TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
if (m_m.is_true(cga)) return false; if (m_m.is_true(cga)) return false;
m_st.m_ackrs_sz++; m_st.m_ackrs_sz++;
m_ackrs.push_back(cga); m_ackrs.push_back(std::move(cga));
return true; return true;
} }

10
src/ackermannization/lackr_model_constructor.cpp
View file

@ -237,7 +237,7 @@ struct lackr_model_constructor::imp {
// handle functions // handle functions
if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted
app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m); app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m);
if (!make_value_uninterpreted_function(a, values, key.get(), result)) { if (!make_value_uninterpreted_function(a, key.get(), result)) {
return false; return false;
} }
} }
@ -284,7 +284,6 @@ struct lackr_model_constructor::imp {
} }
bool make_value_uninterpreted_function(app* a, bool make_value_uninterpreted_function(app* a,
expr_ref_vector& values,
app* key, app* key,
expr_ref& result) { expr_ref& result) {
// get ackermann constant // get ackermann constant
@ -370,15 +369,12 @@ lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref i
{} {}
lackr_model_constructor::~lackr_model_constructor() { lackr_model_constructor::~lackr_model_constructor() {
if (m_imp) dealloc(m_imp); dealloc(m_imp);
} }
bool lackr_model_constructor::check(model_ref& abstr_model) { bool lackr_model_constructor::check(model_ref& abstr_model) {
m_conflicts.reset(); m_conflicts.reset();
if (m_imp) { dealloc(m_imp);
dealloc(m_imp);
m_imp = nullptr;
}
m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts); m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts);
const bool rv = m_imp->check(); const bool rv = m_imp->check();
m_state = rv ? CHECKED : CONFLICT; m_state = rv ? CHECKED : CONFLICT;

6
src/util/obj_ref.h
View file

@ -94,10 +94,8 @@ public:
obj_ref & operator=(obj_ref && n) { obj_ref & operator=(obj_ref && n) {
SASSERT(&m_manager == &n.m_manager); SASSERT(&m_manager == &n.m_manager);
if (this != &n) { std::swap(m_obj, n.m_obj);
std::swap(m_obj, n.m_obj); n.reset();
n.reset();
}
return *this; return *this;
} }

6
src/util/ref_buffer.h
View file

@ -58,6 +58,12 @@ public:
inc_ref(n); inc_ref(n);
m_buffer.push_back(n); m_buffer.push_back(n);
} }
template <typename M>
void push_back(obj_ref<T,M> && n) {
m_buffer.push_back(n.get());
n.steal();
}
void pop_back() { void pop_back() {
SASSERT(!m_buffer.empty()); SASSERT(!m_buffer.empty());

4
src/util/ref_vector.h
View file

@ -99,8 +99,8 @@ public:
return *this; return *this;
} }
template <typename W, typename M> template <typename M>
ref_vector_core& push_back(obj_ref<W,M> && n) { ref_vector_core& push_back(obj_ref<T,M> && n) {
m_nodes.push_back(n.get()); m_nodes.push_back(n.get());
n.steal(); n.steal();
return *this; return *this;