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

shrink ast's app by 8 bytes on 64-bit platforms when number of args > 0

Browse source
This commit is contained in:
Nuno Lopes 2023-12-20 16:58:45 +00:00
parent b2d5c24c1d
commit 4898a156d8
2 changed files with 13 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/ast/ast.cpp
View file

@ -319,26 +319,6 @@ func_decl::func_decl(symbol const & name, unsigned arity, sort * const * domain,
//
// -----------------------------------
static app_flags mk_const_flags() {
app_flags r;
r.m_depth = 1;
r.m_ground = true;
r.m_has_quantifiers = false;
r.m_has_labels = false;
return r;
}
static app_flags mk_default_app_flags() {
app_flags r;
r.m_depth = 1;
r.m_ground = true;
r.m_has_quantifiers = false;
r.m_has_labels = false;
return r;
}
app_flags app::g_constant_flags = mk_const_flags();
app::app(func_decl * decl, unsigned num_args, expr * const * args):
expr(AST_APP),
m_decl(decl),
@ -1762,8 +1742,7 @@ ast * ast_manager::register_node_core(ast * n) {
inc_ref(t->get_decl());
unsigned num_args = t->get_num_args();
if (num_args > 0) {
app_flags * f = t->flags();
*f = mk_default_app_flags();
app_flags * f = &t->m_flags;
SASSERT(t->is_ground());
SASSERT(!t->has_quantifiers());
SASSERT(!t->has_labels());
@ -1776,13 +1755,13 @@ ast * ast_manager::register_node_core(ast * n) {
unsigned arg_depth = 0;
switch (arg->get_kind()) {
case AST_APP: {
app_flags * arg_flags = to_app(arg)->flags();
arg_depth = arg_flags->m_depth;
if (arg_flags->m_has_quantifiers)
app *app = to_app(arg);
arg_depth = app->get_depth();
if (app->has_quantifiers())
f->m_has_quantifiers = true;
if (arg_flags->m_has_labels)
if (app->has_labels())
f->m_has_labels = true;
if (!arg_flags->m_ground)
if (!app->is_ground())
f->m_ground = false;
break;
}

17
src/ast/ast.h
View file

@ -704,6 +704,7 @@ struct app_flags {
unsigned m_ground:1; // application does not have free variables or nested quantifiers.
unsigned m_has_quantifiers:1; // application has nested quantifiers.
unsigned m_has_labels:1; // application has nested labels.
app_flags() : m_depth(1), m_ground(1), m_has_quantifiers(0), m_has_labels(0) {}
};
class app : public expr {
@ -711,19 +712,15 @@ class app : public expr {
func_decl * m_decl;
unsigned m_num_args;
app_flags m_flags;
expr * m_args[0];
static app_flags g_constant_flags;
// remark: store term depth in the end of the app. the depth is only stored if the num_args > 0
static unsigned get_obj_size(unsigned num_args) {
return num_args == 0 ? sizeof(app) : sizeof(app) + num_args * sizeof(expr *) + sizeof(app_flags);
return sizeof(app) + num_args * sizeof(expr *);
}
friend class tmp_app;
app_flags * flags() const { return m_num_args == 0 ? &g_constant_flags : reinterpret_cast<app_flags*>(const_cast<expr**>(m_args + m_num_args)); }
app(func_decl * decl, unsigned num_args, expr * const * args);
public:
func_decl * get_decl() const { return m_decl; }
@ -744,10 +741,10 @@ public:
expr * const * end() const { return m_args + m_num_args; }
sort * _get_sort() const { return get_decl()->get_range(); }
unsigned get_depth() const { return flags()->m_depth; }
bool is_ground() const { return flags()->m_ground; }
bool has_quantifiers() const { return flags()->m_has_quantifiers; }
bool has_labels() const { return flags()->m_has_labels; }
unsigned get_depth() const { return m_flags.m_depth; }
bool is_ground() const { return m_flags.m_ground; }
bool has_quantifiers() const { return m_flags.m_has_quantifiers; }
bool has_labels() const { return m_flags.m_has_labels; }
};
// -----------------------------------