Changes needed to compile at Google, plus some bug fixes from Google.

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();
   }
 
   /**