Minor mixed-bag commit. Expected performance impact negligible.

* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.

4 files changed, 19 insertions, 14 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 51a734757..74bfd3f2b 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -72,10 +72,8 @@ TypeCheckingException::~TypeCheckingException() throw () {
   delete d_expr;
 }
 
-std::string TypeCheckingException::toString() const {
-  std::stringstream ss;
-  ss << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
-  return ss.str();
+void TypeCheckingException::toStream(std::ostream& os) const {
+  os << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
 }
 
 Expr TypeCheckingException::getExpression() const {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index c45cc9b99..291016044 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -99,8 +99,12 @@ public:
    */
   Expr getExpression() const;
 
-  /** Returns the message corresponding to the type-checking failure */
-  std::string toString() const;
+  /**
+   * Returns the message corresponding to the type-checking failure.
+   * We prefer toStream() to toString() because that keeps the expr-depth
+   * and expr-language settings present in the stream.
+   */
+  void toStream(std::ostream& out) const;
 
   friend class ExprManager;
 };/* class TypeCheckingException */
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 445d91da8..586d0cb13 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: dejan
  ** 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)
+ ** 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
@@ -35,10 +35,8 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
   delete d_node;
 }
 
-string TypeCheckingExceptionPrivate::toString() const {
-  stringstream ss;
-  ss << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
-  return ss.str();
+void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const {
+  os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
 }
 
 Node TypeCheckingExceptionPrivate::getNode() const {
diff --git a/src/expr/node.h b/src/expr/node.h
index 6fe1e7d0e..a40b3fce5 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -80,9 +80,14 @@ public:
    */
   NodeTemplate<true> getNode() const;
 
-  /** Returns the message corresponding to the type-checking failure */
-  std::string toString() const;
-};
+  /**
+   * Returns the message corresponding to the type-checking failure.
+   * We prefer toStream() to toString() because that keeps the expr-depth
+   * and expr-language settings present in the stream.
+   */
+  void toStream(std::ostream& out) const;
+
+};/* class TypeCheckingExceptionPrivate */
 
 /**
  * \typedef NodeTemplate<true> Node;