From c9c53b7c6501c7ccd4657353061fbef05aa411b7 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Wed, 20 Dec 2023 18:19:20 +0000
Subject: [PATCH] tmp_enode: don't heap allocate an app. store it inline
 instead. Saves heap allocations and double indirections

---
 src/ast/ast.h         |  4 ++++
 src/smt/smt_enode.cpp | 18 ++++--------------
 src/smt/smt_enode.h   |  3 +--
 3 files changed, 9 insertions(+), 16 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 9618c7e12..a42d894ae 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -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(); }
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index 86b83af4c..4bcb4a41c 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -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;
-    }
-
 };
-
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 92902ea0b..7229dab29 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -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); }