merge from replay branch

3 files changed, 70 insertions, 2 deletions

diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h
new file mode 100644
index 000000000..a6b99fb73
--- /dev/null
+++ b/src/expr/expr_stream.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file expr_stream.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ ** information.\endverbatim
+ **
+ ** \brief A stream interface for expressions
+ **
+ ** A stream interface for expressions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXPR_STREAM_H
+#define __CVC4__EXPR_STREAM_H
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+/**
+ * A pure-virtual stream interface for expressions.  Can be used to
+ * communicate streams of expressions between different parts of CVC4.
+ */
+class CVC4_PUBLIC ExprStream {
+public:
+  /** Virtual destructor; this implementation does nothing. */
+  virtual ~ExprStream() {}
+
+  /**
+   * Get the next expression in the stream (advancing the stream
+   * pointer as a side effect.)
+   */
+  virtual Expr nextExpr() = 0;
+};/* class ExprStream */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR_STREAM_H */
+
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 2e27b4f66..ba695355e 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -5,7 +5,7 @@
  ** Major contributors: mdeters
  ** 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
@@ -432,6 +432,7 @@ protected:
   friend class ExprManager;
   friend class TypeCheckingException;
   friend std::ostream& operator<<(std::ostream& out, const Expr& e);
+  template <bool ref_count> friend class NodeTemplate;
 
 };/* class Expr */
 
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) {