revert last two commits; MSVC doesn't like to statically allocate flexible arrays

Author: nunoplopes

src/ast/ast.h

@@ -707,8 +707,6 @@ 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;
 
@@ -722,10 +720,8 @@ 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(); }

src/smt/smt_enode.cpp

@@ -327,8 +327,10 @@ namespace smt {
     }
 
     tmp_enode::tmp_enode():
+        m_app(0),
         m_capacity(0),
         m_enode_data(nullptr) {
+        SASSERT(m_app.get_app()->get_decl() == 0);
         set_capacity(5);
     }
 
@@ -344,7 +346,7 @@ namespace smt {
         m_enode_data = alloc_svect(char, sz);
         memset(m_enode_data, 0, sz);
         enode * n = get_enode();
-        n->m_owner         = &m_app;
+        n->m_owner         = m_app.get_app();
         n->m_root          = n;
         n->m_next          = n;
         n->m_class_size    = 1;
@@ -356,11 +358,12 @@ namespace smt {
         if (num_args > m_capacity)
             set_capacity(num_args * 2);
         enode * r = get_enode();
-        m_app.m_decl = f;
-        m_app.m_num_args = num_args;
+        m_app.set_decl(f);
+        m_app.set_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;
     }
 
 };
+

src/smt/smt_enode.h

@@ -456,7 +456,7 @@ namespace smt {
     void unmark_enodes2(unsigned num_enodes, enode * const * enodes);
 
     class tmp_enode {
-        app m_app;
+        tmp_app  m_app;
         unsigned m_capacity;
         char *   m_enode_data;
         enode * get_enode() { return reinterpret_cast<enode*>(m_enode_data); }