1 files changed, 16 insertions, 2 deletions
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index c511c580a..250803281 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -18,12 +18,12 @@
 
 namespace CVC4 {
 
+size_t ExprValue::next_id = 1;
+
 ExprValue::ExprValue() :
   d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
 }
 
-size_t ExprValue::next_id = 1;
-
 uint64_t ExprValue::hash() const {
   uint64_t hash = d_kind;
 
@@ -82,4 +82,18 @@ ExprValue::const_iterator ExprValue::rend() const {
   return d_children - 1;
 }
 
+void ExprValue::toString(std::ostream& out) const {
+  out << "(" << Kind(d_kind);
+  if(d_kind == VARIABLE) {
+    out << ":" << this;
+  } else {
+    for(const_iterator i = begin(); i != end(); ++i) {
+      if(i != end())
+        out << " ";
+      out << *i;
+    }
+  }
+  out << ")";
+}
+
 }/* CVC4 namespace */