diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index f68dcfbdd..ca33b48c1 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -216,23 +216,6 @@ namespace datatype { void log_axiom_definitions(symbol const& s, sort * new_sort); - friend class util; - obj_map*> m_datatype2constructors; - obj_map m_datatype2nonrec_constructor; - obj_map*> m_constructor2accessors; - obj_map m_constructor2recognizer; - obj_map m_recognizer2constructor; - obj_map m_accessor2constructor; - obj_map m_is_recursive; - obj_map m_is_enum; - mutable obj_map m_is_fully_interp; - mutable ast_ref_vector * m_asts = nullptr; - sref_vector m_refs; - ptr_vector > m_vectors; - unsigned m_start = 0; - mutable ptr_vector m_fully_interp_trail; - void add_ast(ast* a) const { if (!m_asts) m_asts = alloc(ast_ref_vector, *m_manager); m_asts->push_back(a); } - public: plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {} ~plugin() override; @@ -281,6 +264,23 @@ namespace datatype { void reset(); + + obj_map*> m_datatype2constructors; + obj_map m_datatype2nonrec_constructor; + obj_map*> m_constructor2accessors; + obj_map m_constructor2recognizer; + obj_map m_recognizer2constructor; + obj_map m_accessor2constructor; + obj_map m_is_recursive; + obj_map m_is_enum; + mutable obj_map m_is_fully_interp; + mutable ast_ref_vector* m_asts = nullptr; + sref_vector m_refs; + ptr_vector > m_vectors; + unsigned m_start = 0; + mutable ptr_vector m_fully_interp_trail; + void add_ast(ast* a) const { if (!m_asts) m_asts = alloc(ast_ref_vector, *m_manager); m_asts->push_back(a); } + private: bool is_value_visit(bool unique, expr * arg, ptr_buffer & todo) const; bool is_value_aux(bool unique, app * arg) const;