diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node.h | 8 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_value.h | 8 | ||||
-rw-r--r-- | src/expr/pickler.h | 2 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 2 | ||||
-rw-r--r-- | src/expr/type_node.h | 4 |
7 files changed, 14 insertions, 18 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 080034e70..2a884d35a 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -261,7 +261,7 @@ public: std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; /** Default constructor, makes a null expression. */ - NodeTemplate() : d_nv(&expr::NodeValue::s_null) { } + NodeTemplate() : d_nv(&expr::NodeValue::null()) { } /** * Conversion between nodes that are reference-counted and those that are @@ -322,7 +322,7 @@ public: */ bool isNull() const { assertTNodeNotExpired(); - return d_nv == &expr::NodeValue::s_null; + return d_nv == &expr::NodeValue::null(); } /** @@ -1026,7 +1026,7 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { } template <bool ref_count> -NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null); +NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null()); // FIXME: escape from type system convenient but is there a better // way? Nodes conceptually don't change their expr values but of @@ -1039,7 +1039,7 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) : if(ref_count) { d_nv->inc(); } else { - Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::s_null, + Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null(), "TNode constructed from NodeValue with rc == 0"); } } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 48aacddf2..4eb5dd680 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -112,7 +112,7 @@ NodeManager::NodeManager(ExprManager* exprManager, } void NodeManager::init() { - poolInsert( &expr::NodeValue::s_null ); + poolInsert( &expr::NodeValue::null() ); for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { Kind k = Kind(i); @@ -163,7 +163,7 @@ NodeManager::~NodeManager() { reclaimZombies(); } - poolRemove( &expr::NodeValue::s_null ); + poolRemove( &expr::NodeValue::null() ); if(Debug.isOn("gc:leaks")) { Debug("gc:leaks") << "still in pool:" << endl; diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 8af056f62..6b48fd9b7 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -32,12 +32,10 @@ using namespace std; namespace CVC4 { namespace expr { -NodeValue NodeValue::s_null(0); - string NodeValue::toString() const { stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO : options::outputLanguage(); toStream(ss, -1, false, false, outlang); return ss.str(); } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index a6e7a6053..785f8909f 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -74,9 +74,6 @@ namespace expr { */ class NodeValue { - /** A convenient null-valued expression value */ - static NodeValue s_null; - static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT; static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID; @@ -278,8 +275,9 @@ public: return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } - static inline const NodeValue& null() { - return s_null; + static inline NodeValue& null() { + static NodeValue* s_null = new NodeValue(0); + return *s_null; } /** diff --git a/src/expr/pickler.h b/src/expr/pickler.h index f1cdd1c65..8c3da5f40 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -74,7 +74,7 @@ protected: public: Pickler(ExprManager* em); - ~Pickler(); + virtual ~Pickler(); /** * Constructs a new Pickle of the node n. diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 9dbcb628f..1f2963e18 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -24,7 +24,7 @@ using namespace std; namespace CVC4 { -TypeNode TypeNode::s_null( &expr::NodeValue::s_null ); +TypeNode TypeNode::s_null( &expr::NodeValue::null() ); TypeNode TypeNode::substitute(const TypeNode& type, const TypeNode& replacement, diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 5129b7581..4f9e497ea 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -107,7 +107,7 @@ private: public: /** Default constructor, makes a null expression. */ - TypeNode() : d_nv(&expr::NodeValue::s_null) { } + TypeNode() : d_nv(&expr::NodeValue::null()) { } /** Copy constructor */ TypeNode(const TypeNode& node); @@ -404,7 +404,7 @@ public: * @return true if null */ bool isNull() const { - return d_nv == &expr::NodeValue::s_null; + return d_nv == &expr::NodeValue::null(); } /** |