From b33a35b720059370ffb1507f31603cdb5347503a Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 16 Dec 2009 19:51:02 +0000
Subject: [PATCH] Small refactoring changes for the expr package.

---
 src/expr/attr_type.h    |  5 ++++-
 src/expr/expr.cpp       | 13 +++++++++----
 src/expr/expr.h         |  1 +
 src/expr/expr_manager.h |  6 ++++--
 src/expr/node.cpp       |  2 +-
 src/expr/node.h         |  4 ++--
 src/expr/node_manager.h |  2 +-
 7 files changed, 22 insertions(+), 11 deletions(-)

diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 2e0a8b675..597be0fe7 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -23,7 +23,10 @@ class Type;
 // this is essentially a traits structure
 class Type_attr {
 public:
-  enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
+  
+  // could use typeid but then different on different machines/compiles
+  enum { hash_value = 11 };
+  
   typedef Type value_type;//Node?
   static const Type_attr marker;
 };
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index af685aced..eacd1cb24 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -46,8 +46,11 @@ Expr& Expr::operator=(const Expr& e) {
 }
 
 bool Expr::operator==(const Expr& e) const {
-  if(d_em != e.d_em)
-    return false;Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  if(d_em != e.d_em){
+    return false;
+  }
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
   return *d_node == *e.d_node;
 }
 
@@ -56,9 +59,11 @@ bool Expr::operator!=(const Expr& e) const {
 }
 
 bool Expr::operator<(const Expr& e) const {
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
-  if(d_em != e.d_em)
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  if(d_em != e.d_em){
     return false;
+  }
   return *d_node < *e.d_node;
 }
 
diff --git a/src/expr/expr.h b/src/expr/expr.h
index 34a94ee66..a0a646900 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -95,6 +95,7 @@ public:
 
   /**
    * Returns the string representation of the expression.
+   * @return a string representation of the expression
    */
   std::string toString() const;
 
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 4a7f359e9..645193ecf 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -23,7 +23,7 @@ class CVC4_PUBLIC ExprManager {
 public:
 
   /**
-   * Creates an expressio manager.
+   * Creates an expression manager.
    */
   ExprManager();
 
@@ -49,8 +49,10 @@ public:
   Expr mkExpr(Kind kind, const Expr& child1);
 
   /**
-   * Make a ternary expression of a given kind (AND, PLUS, ...).
+   * Make a binary expression of a given kind (AND, PLUS, ...).
    * @param kind the kind of expression
+   * @param child1 the first child of the new expression
+   * @param child2 the second child of the new expression
    * @return the expression
    */
   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 1a549973f..f1b3c5980 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -67,7 +67,7 @@ void Node::assignNodeValue(NodeValue* ev) {
 
 Node& Node::operator=(const Node& e) {
   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
-  if(this != &e && d_ev != e.d_ev) {
+  if((this != &e) && (d_ev != e.d_ev)) {
     d_ev->dec();
     d_ev = e.d_ev;
     d_ev->inc();
diff --git a/src/expr/node.h b/src/expr/node.h
index 5415a5b3c..aad0689bb 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -74,8 +74,8 @@ class Node {
   NodeValue const* operator->() const;
 
   /**
-   * Assigns the expression value and does reference counting. No assumptions are
-   * made on the expression, and should only be used if we know what we are
+   * Assigns the expression value and does reference counting. No assumptions
+   * are made on the expression, and should only be used if we know what we are
    * doing.
    *
    * @param ev the expression value to assign
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3a28a22ff..bdbedbb4a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_manager.h
+/** node_manager.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
-- 
2.30.2