mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

tmp_enode: don't heap allocate an app. store it inline instead.

Browse source 
Saves heap allocations and double indirections
This commit is contained in:
Nuno Lopes 2023-12-20 18:19:20 +00:00
parent 4898a156d8
commit c9c53b7c65
3 changed files with 9 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast.h
View file

@ -707,6 +707,8 @@ struct app_flags {
app_flags() : m_depth(1), m_ground(1), m_has_quantifiers(0), m_has_labels(0) {}
};
namespace smt { class tmp_enode; }
class app : public expr {
friend class ast_manager;
@ -720,8 +722,10 @@ class app : public expr {
}
friend class tmp_app;
friend class smt::tmp_enode;
app(func_decl * decl, unsigned num_args, expr * const * args);
app() : expr(AST_APP) {}
public:
func_decl * get_decl() const { return m_decl; }
family_id get_family_id() const { return get_decl()->get_family_id(); }

18
src/smt/smt_enode.cpp
View file

@ -327,7 +327,6 @@ namespace smt {
}
tmp_enode::tmp_enode():
m_app(0),
m_capacity(0),
m_enode_data(nullptr) {
SASSERT(m_app.get_app()->get_decl() == 0);
@ -340,14 +339,13 @@ namespace smt {
void tmp_enode::set_capacity(unsigned new_capacity) {
SASSERT(new_capacity > m_capacity);
if (m_enode_data)
dealloc_svect(m_enode_data);
dealloc_svect(m_enode_data);
m_capacity = new_capacity;
unsigned sz = sizeof(enode) + m_capacity * sizeof(enode*);
m_enode_data = alloc_svect(char, sz);
memset(m_enode_data, 0, sz);
enode * n = get_enode();
n->m_owner = m_app.get_app();
n->m_owner = &m_app;
n->m_root = n;
n->m_next = n;
n->m_class_size = 1;
@ -359,19 +357,11 @@ namespace smt {
if (num_args > m_capacity)
set_capacity(num_args * 2);
enode * r = get_enode();
if (m_app.get_app()->get_decl() != f) {
r->m_func_decl_id = UINT_MAX;
}
m_app.set_decl(f);
m_app.set_num_args(num_args);
m_app.m_decl = f;
m_app.m_num_args = num_args;
r->m_commutative = num_args == 2 && f->is_commutative();
memcpy(get_enode()->m_args, args, sizeof(enode*)*num_args);
return r;
}
void tmp_enode::reset() {
get_enode()->m_func_decl_id = UINT_MAX;
}
};

3
src/smt/smt_enode.h
View file

@ -456,7 +456,7 @@ namespace smt {
void unmark_enodes2(unsigned num_enodes, enode * const * enodes);
class tmp_enode {
tmp_app m_app;
app m_app;
unsigned m_capacity;
char * m_enode_data;
enode * get_enode() { return reinterpret_cast<enode*>(m_enode_data); }
@ -465,7 +465,6 @@ namespace smt {
tmp_enode();
~tmp_enode();
enode * set(func_decl * f, unsigned num_args, enode * const * args);
void reset();
};
inline mk_pp pp(enode* n, ast_manager& m) { return mk_pp(n->get_expr(), m); }