merge from replay branch

1 files changed, 21 insertions, 1 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 03840e670..d67bc2e2b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -225,6 +225,14 @@ public:
   NodeTemplate(const NodeTemplate& node);
 
   /**
+   * Allow Exprs to become Nodes.  This permits flexible translation of
+   * Exprs -> Nodes inside the CVC4 library without exposing a toNode()
+   * function in the public interface, or requiring lots of "friend"
+   * relationships.
+   */
+  NodeTemplate(const Expr& e);
+
+  /**
    * Assignment operator for nodes, copies the relevant information from node
    * to this node.
    * @param node the node to copy
@@ -915,6 +923,18 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
 }
 
 template <bool ref_count>
+NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
+  Assert(e.d_node != NULL, "Expecting a non-NULL expression value!");
+  Assert(e.d_node->d_nv != NULL, "Expecting a non-NULL expression value!");
+  d_nv = e.d_node->d_nv;
+  // shouldn't ever fail
+  Assert(d_nv->d_rc > 0, "Node constructed from Expr with rc == 0");
+  if(ref_count) {
+    d_nv->inc();
+  }
+}
+
+template <bool ref_count>
 NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   if(ref_count) {