Small refactoring changes for the expr package.

diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 2e0a8b6754f286f357e042589e525fea559b2194..597be0fe71bd52d27aae91327829cf7b76693fdb 100644 (file)
--- 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 af685aced65f66f88452346023d10ba887c1896b..eacd1cb2409f5935f4c34cfe969177ab064b0e9c 100644 (file)
--- 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 34a94ee668989593fc2d92c749bb1eee3c099a7a..a0a64690015dc1c29ea9ced8287d26a3d038fcdd 100644 (file)
--- 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 4a7f359e9852034afec04da10662270b8c42581a..645193ecfe9133cf6d31107e663c5e03d38209f1 100644 (file)
--- 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 1a549973fa9890fe7d7a52c85ef1ad753d0ad155..f1b3c5980d29e1250e18aedd8d919605aeda4ebf 100644 (file)
--- 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 5415a5b3c5eae85b4f9af29a821224b0cbaeb564..aad0689bbe7bb300f0cdac2a325c048570c14672 100644 (file)
--- 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 3a28a22ff2d156d8d6bb5bd81749db2782886240..bdbedbb4a1e3e55e13acb4b2e807cee655b2c2da 100644 (file)
--- 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