part of review (bug #197): coding conventions, file-level documentation, re-ran update-copyright.pl, etc.

14 files changed, 219 insertions, 169 deletions

diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h
index f347105e3..f336237a4 100644
--- a/src/theory/arith/arith_activity.h
+++ b/src/theory/arith/arith_activity.h
@@ -2,7 +2,7 @@
 /*! \file arith_activity.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** 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)
@@ -17,7 +17,6 @@
  ** \todo document this file
  **/
 
-
 #include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H
diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
index 4a8fec56f..27abd8873 100644
--- a/src/theory/arith/arith_constants.h
+++ b/src/theory/arith/arith_constants.h
@@ -17,16 +17,16 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
 
+#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
+#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
 
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "util/rational.h"
 #include "theory/arith/delta_rational.h"
 
-#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
-#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H
-
 namespace CVC4 {
 namespace theory {
 namespace arith {
diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp
index 0f417bc41..bf14e882e 100644
--- a/src/theory/arith/arith_propagator.cpp
+++ b/src/theory/arith/arith_propagator.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h
index 7ffcec747..8ea628f25 100644
--- a/src/theory/arith/arith_propagator.h
+++ b/src/theory/arith/arith_propagator.h
@@ -2,7 +2,7 @@
 /*! \file arith_propagator.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** 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)
@@ -17,8 +17,6 @@
  ** \todo document this file
  **/
 
-
-
 #include "cvc4_private.h"
 
 #ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6706ad76a..d2c07900d 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -2,8 +2,8 @@
 /*! \file arith_utilities.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
diff --git a/src/theory/arith/next_arith_rewriter.cpp b/src/theory/arith/next_arith_rewriter.cpp
index c14f806c9..29fae233b 100644
--- a/src/theory/arith/next_arith_rewriter.cpp
+++ b/src/theory/arith/next_arith_rewriter.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file arith_rewriter.cpp
+/*! \file next_arith_rewriter.cpp
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
diff --git a/src/theory/arith/next_arith_rewriter.h b/src/theory/arith/next_arith_rewriter.h
index 7f1ec0fbd..1fb743f71 100644
--- a/src/theory/arith/next_arith_rewriter.h
+++ b/src/theory/arith/next_arith_rewriter.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file arith_rewriter.h
+/*! \file next_arith_rewriter.h
  ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 6e476bb7f..7baacd4f5 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -1,3 +1,21 @@
+/*********************                                                        */
+/*! \file normal_form.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include "theory/arith/normal_form.h"
 #include <list>
@@ -7,57 +25,57 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
-bool VarList::isSorted(iterator start, iterator end){
+bool VarList::isSorted(iterator start, iterator end) {
   return __gnu_cxx::is_sorted(start, end);
 }
 
-bool VarList::isMember(Node n){
-  if(n.getNumChildren() == 0){
+bool VarList::isMember(Node n) {
+  if(n.getNumChildren() == 0) {
     return Variable::isMember(n);
-  }else if(n.getKind() == kind::MULT){
+  } else if(n.getKind() == kind::MULT) {
     Node::iterator curr = n.begin(), end = n.end();
     Node prev = *curr;
     if(!Variable::isMember(prev)) return false;
 
-    while( (++curr) != end){
+    while( (++curr) != end) {
       if(!Variable::isMember(*curr)) return false;
       if(!(prev <= *curr)) return false;
       prev = *curr;
     }
     return true;
-  }else{
+  } else {
     return false;
   }
 }
-int VarList::cmp(const VarList& vl) const{
+int VarList::cmp(const VarList& vl) const {
   int dif = this->size() - vl.size();
-  if (dif == 0){
+  if (dif == 0) {
     return this->getNode().getId() - vl.getNode().getId();
-  }else if(dif < 0){
+  } else if(dif < 0) {
     return -1;
-  }else{
+  } else {
     return 1;
   }
 }
 
-VarList VarList::parseVarList(Node n){
-  if(n.getNumChildren() == 0){
+VarList VarList::parseVarList(Node n) {
+  if(n.getNumChildren() == 0) {
     return VarList(Variable(n));
-  }else{
+  } else {
     Assert(n.getKind() == kind::MULT);
-    for(Node::iterator i=n.begin(), end = n.end(); i!=end; ++i){
+    for(Node::iterator i=n.begin(), end = n.end(); i!=end; ++i) {
       Assert(Variable::isMember(*i));
     }
     return VarList(n);
   }
 }
 
-VarList VarList::operator*(const VarList& vl) const{
-  if(this->empty()){
+VarList VarList::operator*(const VarList& vl) const {
+  if(this->empty()) {
     return vl;
-  }else if(vl.empty()){
+  } else if(vl.empty()) {
     return *this;
-  }else{
+  } else {
     vector<Node> result;
     back_insert_iterator< vector<Node> > bii(result);
 
@@ -74,21 +92,21 @@ VarList VarList::operator*(const VarList& vl) const{
   }
 }
 
-Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl){
-  if(c.isZero() || vl.empty() ){
+Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl) {
+  if(c.isZero() || vl.empty() ) {
     return Monomial(c);
-  }else if(c.isOne()){
+  } else if(c.isOne()) {
     return Monomial(vl);
-  }else{
+  } else {
     return Monomial(c, vl);
   }
 }
-Monomial Monomial::parseMonomial(Node n){
-  if(n.getKind() == kind::CONST_RATIONAL){
+Monomial Monomial::parseMonomial(Node n) {
+  if(n.getKind() == kind::CONST_RATIONAL) {
     return Monomial(Constant(n));
-  }else if(multStructured(n)){
+  } else if(multStructured(n)) {
     return Monomial::mkMonomial(Constant(n[0]),VarList::parseVarList(n[1]));
-  }else{
+  } else {
     return Monomial(VarList::parseVarList(n));
   }
 }
@@ -100,22 +118,22 @@ Monomial Monomial::operator*(const Monomial& mono) const {
   return Monomial::mkMonomial(newConstant, newVL);
 }
 
-vector<Monomial> Monomial::sumLikeTerms(const vector<Monomial> & monos){
+vector<Monomial> Monomial::sumLikeTerms(const vector<Monomial> & monos) {
   Assert(isSorted(monos));
 
   Debug("blah") << "start sumLikeTerms" << std::endl;
   printList(monos);
   vector<Monomial> outMonomials;
   typedef vector<Monomial>::const_iterator iterator;
-  for(iterator rangeIter = monos.begin(), end=monos.end(); rangeIter != end;){
+  for(iterator rangeIter = monos.begin(), end=monos.end(); rangeIter != end;) {
     Rational constant = (*rangeIter).getConstant().getValue();
     VarList varList  = (*rangeIter).getVarList();
     ++rangeIter;
-    while(rangeIter != end && varList == (*rangeIter).getVarList()){
+    while(rangeIter != end && varList == (*rangeIter).getVarList()) {
       constant += (*rangeIter).getConstant().getValue();
       ++rangeIter;
     }
-    if(constant != 0){
+    if(constant != 0) {
       Constant asConstant = Constant::mkConstant(constant);
       Monomial nonZero = Monomial::mkMonomial(asConstant, varList);
       outMonomials.push_back(nonZero);
@@ -129,14 +147,14 @@ vector<Monomial> Monomial::sumLikeTerms(const vector<Monomial> & monos){
   return outMonomials;
 }
 
-void Monomial::printList(const std::vector<Monomial>& monos){
+void Monomial::printList(const std::vector<Monomial>& monos) {
   typedef std::vector<Monomial>::const_iterator iterator;
-  for(iterator i = monos.begin(), end = monos.end(); i != end; ++i){
+  for(iterator i = monos.begin(), end = monos.end(); i != end; ++i) {
     Debug("blah") <<  ((*i).getNode()) << std::endl;
   }
 }
 
-Polynomial Polynomial::operator+(const Polynomial& vl) const{
+Polynomial Polynomial::operator+(const Polynomial& vl) const {
   this->printList();
   vl.printList();
 
@@ -151,12 +169,12 @@ Polynomial Polynomial::operator+(const Polynomial& vl) const{
   return result;
 }
 
-Polynomial Polynomial::operator*(const Monomial& mono) const{
-  if(mono.isZero()){
+Polynomial Polynomial::operator*(const Monomial& mono) const {
+  if(mono.isZero()) {
     return Polynomial(mono); //Don't multiply by zero
-  }else{
+  } else {
     std::vector<Monomial> newMonos;
-    for(iterator i = this->begin(), end = this->end(); i != end; ++i){
+    for(iterator i = this->begin(), end = this->end(); i != end; ++i) {
       newMonos.push_back(mono * (*i));
     }
 
@@ -169,9 +187,9 @@ Polynomial Polynomial::operator*(const Monomial& mono) const{
   }
 }
 
-Polynomial Polynomial::operator*(const Polynomial& poly) const{
+Polynomial Polynomial::operator*(const Polynomial& poly) const {
   Polynomial res = Polynomial::mkZero();
-  for(iterator i = this->begin(), end = this->end(); i != end; ++i){
+  for(iterator i = this->begin(), end = this->end(); i != end; ++i) {
     Monomial curr = *i;
     Polynomial prod = poly * curr;
     Polynomial sum  = res + prod;
@@ -181,10 +199,10 @@ Polynomial Polynomial::operator*(const Polynomial& poly) const{
 }
 
 
-Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r){
+Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r) {
   Assert(!l.isConstant());
   Assert(isRelationOperator(k));
-  switch(k){
+  switch(k) {
   case kind::GEQ:
   case kind::EQUAL:
   case kind::LEQ:
@@ -198,10 +216,10 @@ Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r){
   }
 }
 
-Comparison Comparison::parseNormalForm(TNode n){
-  if(n.getKind() == kind::CONST_BOOLEAN){
+Comparison Comparison::parseNormalForm(TNode n) {
+  if(n.getKind() == kind::CONST_BOOLEAN) {
     return Comparison(n.getConst<bool>());
-  }else{
+  } else {
     bool negated = n.getKind() == kind::NOT;
     Node relation = negated ? n[0] : n;
     Assert( !negated ||
@@ -212,10 +230,10 @@ Comparison Comparison::parseNormalForm(TNode n){
     Constant right(relation[1]);
 
     Kind newOperator = relation.getKind();
-    if(negated){
-      if(newOperator == kind::LEQ){
+    if(negated) {
+      if(newOperator == kind::LEQ) {
         newOperator = kind::GT;
-      }else{
+      } else {
         newOperator = kind::LT;
       }
     }
@@ -223,19 +241,19 @@ Comparison Comparison::parseNormalForm(TNode n){
   }
 }
 
-Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right){
+Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) {
   Assert(isRelationOperator(k));
-  if(left.isConstant()){
+  if(left.isConstant()) {
     const Rational& rConst =  left.getNode().getConst<Rational>();
     const Rational& lConst = right.getNode().getConst<Rational>();
     bool res = evaluateConstantPredicate(k, lConst, rConst);
     return Comparison(res);
-  }else{
+  } else {
     return Comparison(toNode(k, left, right), k, left, right);
   }
 }
 
-Comparison Comparison::addConstant(const Constant& constant) const{
+Comparison Comparison::addConstant(const Constant& constant) const {
   Assert(!isBoolean());
   Monomial mono(constant);
   Polynomial constAsPoly( mono );
@@ -244,7 +262,7 @@ Comparison Comparison::addConstant(const Constant& constant) const{
   return mkComparison(oper, newLeft, newRight);
 }
 
-Comparison Comparison::multiplyConstant(const Constant& constant) const{
+Comparison Comparison::multiplyConstant(const Constant& constant) const {
   Assert(!isBoolean());
   Kind newOper = (constant.getValue() < 0) ? negateRelationKind(oper) : oper;
 
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 0762868cf..a09437160 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -1,3 +1,26 @@
+/*********************                                                        */
+/*! \file normal_form.h
+ ** \verbatim
+ ** Original author: taking
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
+#define __CVC4__THEORY__ARITH__NORMAL_FORM_H
 
 #include "expr/node.h"
 #include "util/rational.h"
@@ -8,9 +31,6 @@
 #include <algorithm>
 #include <ext/algorithm>
 
-#ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
-#define __CVC4__THEORY__ARITH__NORMAL_FORM_H
-
 namespace CVC4 {
 namespace theory {
 namespace arith {
@@ -29,34 +49,34 @@ namespace arith {
  * variable := n
  *   where
  *     n.getMetaKind() == metakind::VARIABLE
-
+ *
  * constant := n
  *   where
  *     n.getKind() == kind::CONST_RATIONAL
-
+ *
  * var_list := variable | (* [variable])
  *   where
  *     len [variable] >= 2
  *     isSorted varOrder [variable]
-
+ *
  * monomial := constant | var_list | (* constant' var_list')
  *   where
  *     constant' \not\in {0,1}
-
+ *
  * polynomial := monomial' | (+ [monomial])
  *   where
  *     len [monomial] >= 2
  *     isStrictlySorted monoOrder [monomial]
  *     forall (\x -> x != 0) [monomial]
-
+ *
  * restricted_cmp := (|><| polynomial constant)
  *   where
  *     |><| is GEQ, EQ, or EQ
  *     not (exists constantMonomial (monomialList polynomial))
  *     monomialCoefficient (head (monomialList polynomial)) == 1
-
+ *
  * comparison := TRUE | FALSE | restricted_cmp | (not restricted_cmp)
-
+ *
  * Normal Form for terms := polynomial
  * Normal Form for atoms := comparison
  */
@@ -94,11 +114,11 @@ namespace arith {
  *  And if isMember(node) is false, this throws an assertion failure in debug
  *  mode and has undefined behaviour if not in debug mode.
  * -Only public facing constructors, parseClass(node), and mk*() functions are
- *  considered privledged functions for the helper class.
- * -Only privledged functions may use private constructors, and access
+ *  considered privileged functions for the helper class.
+ * -Only privileged functions may use private constructors, and access
  *  private data members.
- * -All non-privledges functions are considered utility functions and
- *  must use a privledged function in order to create an instance of the class.
+ * -All non-privileged functions are considered utility functions and
+ *  must use a privileged function in order to create an instance of the class.
  */
 
 /**
@@ -143,6 +163,7 @@ namespace arith {
  *      | (+ [monomial]) -> [monomial]
  */
 
+
 /**
  * A NodeWrapper is a class that is a thinly veiled container of a Node object.
  */
@@ -152,7 +173,8 @@ private:
 public:
   NodeWrapper(Node n) : node(n) {}
   const Node& getNode() const { return node; }
-};
+};/* class NodeWrapper */
+
 
 class Variable : public NodeWrapper {
 public:
@@ -166,10 +188,11 @@ public:
 
   bool isNormalForm() { return isMember(getNode()); }
 
-  bool operator<(const Variable& v) const{ return getNode() < v.getNode();}
-  bool operator==(const Variable& v) const{ return getNode() == v.getNode();}
+  bool operator<(const Variable& v) const { return getNode() < v.getNode();}
+  bool operator==(const Variable& v) const { return getNode() == v.getNode();}
+
+};/* class Variable */
 
-};
 
 class Constant : public NodeWrapper {
 public:
@@ -187,7 +210,7 @@ public:
     return Constant(coerceToRationalNode(n));
   }
 
-  static Constant mkConstant(const Rational& rat){
+  static Constant mkConstant(const Rational& rat) {
     return Constant(mkRationalNode(rat));
   }
 
@@ -195,30 +218,34 @@ public:
     return getNode().getConst<Rational>();
   }
 
-  bool isZero() const{ return getValue() == 0; }
-  bool isOne() const{ return getValue() == 1; }
+  bool isZero() const { return getValue() == 0; }
+  bool isOne() const { return getValue() == 1; }
 
-  Constant operator*(const Constant& other) const{
+  Constant operator*(const Constant& other) const {
     return mkConstant(getValue() * other.getValue());
   }
-  Constant operator+(const Constant& other) const{
+  Constant operator+(const Constant& other) const {
     return mkConstant(getValue() + other.getValue());
   }
-  Constant operator-() const{
+  Constant operator-() const {
     return mkConstant(-getValue());
   }
-};
+
+};/* class Constant */
+
 
 template <class GetNodeIterator>
-inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end){
+inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
   NodeBuilder<> nb(k);
 
-  while(start != end){
+  while(start != end) {
     nb << (*start).getNode();
     ++start;
   }
+
   return Node(nb);
-}
+}/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
+
 
 /**
  * A VarList is a sorted list of variables representing a product.
@@ -231,18 +258,19 @@ class VarList {
 private:
   Node backingNode;
 
-  static Node multList(const std::vector<Variable>& list){
+  static Node multList(const std::vector<Variable>& list) {
     Assert(list.size() >= 2);
 
     return makeNode(kind::MULT, list.begin(), list.end());
   }
-  static Node makeTuple(Node n){
+  static Node makeTuple(Node n) {
+    // MGD FOR REVIEW: drop IDENTITY kind ?
     return NodeManager::currentNM()->mkNode(kind::IDENTITY, n);
   }
 
-  VarList() : backingNode(Node::null()){}
+  VarList() : backingNode(Node::null()) {}
 
-  VarList(Node n){
+  VarList(Node n) {
     backingNode = (Variable::isMember(n)) ? makeTuple(n) : n;
 
     Assert(isSorted(begin(), end()));
@@ -255,15 +283,15 @@ public:
   public:
     explicit iterator(Node::iterator i) : d_iter(i) {}
 
-    inline Variable operator*(){
+    inline Variable operator*() {
       return Variable(*d_iter);
     }
 
-    bool operator==(const iterator& i){
+    bool operator==(const iterator& i) {
       return d_iter == i.d_iter;
     }
 
-    bool operator!=(const iterator& i){
+    bool operator!=(const iterator& i) {
       return d_iter != i.d_iter;
     }
 
@@ -277,52 +305,52 @@ public:
     }
   };
 
-  Node getNode() const{
-    if(singleton()){
+  Node getNode() const {
+    if(singleton()) {
       return backingNode[0];
-    }else{
+    } else {
       return backingNode;
     }
   }
 
-  iterator begin() const{
+  iterator begin() const {
     return iterator(backingNode.begin());
   }
-  iterator end() const{
+  iterator end() const {
     return iterator(backingNode.end());
   }
 
-  VarList(Variable v) : backingNode(makeTuple(v.getNode())){
+  VarList(Variable v) : backingNode(makeTuple(v.getNode())) {
     Assert(isSorted(begin(), end()));
   }
-  VarList(const std::vector<Variable>& l) : backingNode(multList(l)){
+  VarList(const std::vector<Variable>& l) : backingNode(multList(l)) {
     Assert(l.size() >= 2);
     Assert(isSorted(begin(), end()));
   }
 
   static bool isMember(Node n);
 
-  bool isNormalForm() const{
+  bool isNormalForm() const {
     return !empty();
   }
 
-  static VarList mkEmptyVarList(){
+  static VarList mkEmptyVarList() {
     return VarList();
   }
 
 
   /** There are no restrictions on the size of l */
-  static VarList mkVarList(const std::vector<Variable>& l){
-    if(l.size() == 0){
+  static VarList mkVarList(const std::vector<Variable>& l) {
+    if(l.size() == 0) {
       return mkEmptyVarList();
-    }else if(l.size() == 1){
+    } else if(l.size() == 1) {
       return VarList((*l.begin()).getNode());
-    }else{
+    } else {
       return VarList(l);
     }
   }
 
-  int size() const{ return backingNode.getNumChildren(); }
+  int size() const { return backingNode.getNumChildren(); }
   bool empty() const { return size() == 0; }
   bool singleton() const { return backingNode.getKind() == kind::IDENTITY; }
 
@@ -332,13 +360,15 @@ public:
 
   int cmp(const VarList& vl) const;
 
-  bool operator<(const VarList& vl) const{ return cmp(vl) < 0; }
+  bool operator<(const VarList& vl) const { return cmp(vl) < 0; }
 
-  bool operator==(const VarList& vl) const{ return cmp(vl) == 0; }
+  bool operator==(const VarList& vl) const { return cmp(vl) == 0; }
 
 private:
   bool isSorted(iterator start, iterator end);
-};
+
+};/* class VarList */
+
 
 class Monomial : public NodeWrapper {
 private:
@@ -353,14 +383,14 @@ private:
     Assert(!c.isOne() || !multStructured(n));
   }
 
-  static Node makeMultNode(const Constant& c, const VarList& vl){
+  static Node makeMultNode(const Constant& c, const VarList& vl) {
     Assert(!c.isZero());
     Assert(!c.isOne());
     Assert(!vl.empty());
     return NodeManager::currentNM()->mkNode(kind::MULT, c.getNode(), vl.getNode());
   }
 
-  static bool multStructured(Node n){
+  static bool multStructured(Node n) {
     return n.getKind() ==  kind::MULT &&
       n[0].getKind() == kind::CONST_RATIONAL &&
       n.getNumChildren() == 2;
@@ -394,20 +424,20 @@ public:
 
   static Monomial parseMonomial(Node n);
 
-  static Monomial mkZero(){
+  static Monomial mkZero() {
     return Monomial(Constant::mkConstant(0));
   }
-  static Monomial mkOne(){
+  static Monomial mkOne() {
     return Monomial(Constant::mkConstant(1));
   }
-  const Constant& getConstant() const{ return constant; }
-  const VarList& getVarList() const{ return varList; }
+  const Constant& getConstant() const { return constant; }
+  const VarList& getVarList() const { return varList; }
 
-  bool isConstant() const{
+  bool isConstant() const {
     return varList.empty();
   }
 
-  bool isZero() const{
+  bool isZero() const {
     return constant.isZero();
   }
 
@@ -418,23 +448,23 @@ public:
   Monomial operator*(const Monomial& mono) const;
 
 
-  int cmp(const Monomial& mono) const{
+  int cmp(const Monomial& mono) const {
     return getVarList().cmp(mono.getVarList());
   }
 
-  bool operator<(const Monomial& vl) const{
+  bool operator<(const Monomial& vl) const {
     return cmp(vl) < 0;
   }
 
-  bool operator==(const Monomial& vl) const{
+  bool operator==(const Monomial& vl) const {
     return cmp(vl) == 0;
   }
 
-  static bool isSorted(const std::vector<Monomial>& m){
+  static bool isSorted(const std::vector<Monomial>& m) {
     return __gnu_cxx::is_sorted(m.begin(), m.end());
   }
 
-  static bool isStrictlySorted(const std::vector<Monomial>& m){
+  static bool isStrictlySorted(const std::vector<Monomial>& m) {
     return isSorted(m) && std::adjacent_find(m.begin(),m.end()) == m.end();
   }
 
@@ -445,10 +475,12 @@ public:
   static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
 
   static void printList(const std::vector<Monomial>& monos);
-};
+};/* class Monomial */
+
 
 class Polynomial : public NodeWrapper {
 private:
+  // MGD FOR REVIEW: do not create this vector<>!
   std::vector<Monomial> monos;
 
   Polynomial(Node n, const std::vector<Monomial>& m):
@@ -458,7 +490,7 @@ private:
     Assert( Monomial::isStrictlySorted(monos) );
   }
 
-  static Node makePlusNode(const std::vector<Monomial>& m){
+  static Node makePlusNode(const std::vector<Monomial>& m) {
     Assert(m.size() >= 2);
 
     return makeNode(kind::PLUS, m.begin(), m.end());
@@ -467,8 +499,8 @@ private:
 public:
   typedef std::vector<Monomial>::const_iterator iterator;
 
-  iterator begin() const{ return monos.begin(); }
-  iterator end() const{ return monos.end(); }
+  iterator begin() const { return monos.begin(); }
+  iterator end() const { return monos.end(); }
 
   Polynomial(const Monomial& m):
     NodeWrapper(m.getNode()), monos()
@@ -483,51 +515,52 @@ public:
   }
 
 
-  static Polynomial mkPolynomial(const std::vector<Monomial>& m){
-    if(m.size() == 0){
+  static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
+    if(m.size() == 0) {
       return Polynomial(Monomial::mkZero());
-    }else if(m.size() == 1){
+    } else if(m.size() == 1) {
       return Polynomial((*m.begin()));
-    }else{
+    } else {
       return Polynomial(m);
     }
   }
 
-  static Polynomial parsePolynomial(Node n){
+  // MGD FOR REVIEW: make this constant time (for non-debug mode)
+  static Polynomial parsePolynomial(Node n) {
     std::vector<Monomial> monos;
-    if(n.getKind() == kind::PLUS){
-      for(Node::iterator i=n.begin(), end=n.end(); i != end; ++i){
+    if(n.getKind() == kind::PLUS) {
+      for(Node::iterator i=n.begin(), end=n.end(); i != end; ++i) {
         monos.push_back(Monomial::parseMonomial(*i));
       }
-    }else{
+    } else {
       monos.push_back(Monomial::parseMonomial(n));
     }
     return Polynomial(n,monos);
   }
 
-  static Polynomial mkZero(){
+  static Polynomial mkZero() {
     return Polynomial(Monomial::mkZero());
   }
-  static Polynomial mkOne(){
+  static Polynomial mkOne() {
     return Polynomial(Monomial::mkOne());
   }
-  bool isZero() const{
+  bool isZero() const {
     return (monos.size() == 1) && (getHead().isZero());
   }
 
-  bool isConstant() const{
+  bool isConstant() const {
     return (monos.size() == 1) && (getHead().isConstant());
   }
 
-  bool containsConstant() const{
+  bool containsConstant() const {
     return getHead().isConstant();
   }
 
-  Monomial getHead() const{
+  Monomial getHead() const {
     return *(begin());
   }
 
-  Polynomial getTail() const{
+  Polynomial getTail() const {
     Assert(monos.size() >= 1);
 
     iterator start = begin()+1;
@@ -535,10 +568,10 @@ public:
     return mkPolynomial(subrange);
   }
 
-  void printList() const{
-    Debug("blah") << "start list" << std::endl;
+  void printList() const {
+    Debug("normal-form") << "start list" << std::endl;
     Monomial::printList(monos);
-    Debug("blah") << "end list" << std::endl;
+    Debug("normal-form") << "end list" << std::endl;
   }
 
   Polynomial operator+(const Polynomial& vl) const;
@@ -547,7 +580,8 @@ public:
 
   Polynomial operator*(const Polynomial& poly) const;
 
-};
+};/* class Polynomial */
+
 
 class Comparison : public NodeWrapper {
 private:
@@ -578,18 +612,18 @@ public:
 
   static Comparison mkComparison(Kind k, const Polynomial& left, const Constant& right);
 
-  bool isBoolean() const{
+  bool isBoolean() const {
     return (oper == kind::CONST_BOOLEAN);
   }
 
-  bool isNormalForm() const{
-    if(isBoolean()){
+  bool isNormalForm() const {
+    if(isBoolean()) {
       return true;
-    }else if(left.containsConstant()){
+    } else if(left.containsConstant()) {
       return false;
-    }else if(left.getHead().getConstant().isOne()){
+    } else if(left.getHead().getConstant().isOne()) {
       return true;
-    }else{
+    } else {
       return false;
     }
   }
@@ -601,12 +635,11 @@ public:
   Comparison multiplyConstant(const Constant& constant) const;
 
   static Comparison parseNormalForm(TNode n);
-};
-
 
+};/* class Comparison */
 
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */
diff --git a/src/theory/arith/ordered_bounds_list.h b/src/theory/arith/ordered_bounds_list.h
index 4393a382e..f3bf3d58b 100644
--- a/src/theory/arith/ordered_bounds_list.h
+++ b/src/theory/arith/ordered_bounds_list.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 603eb5278..768d9f39d 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8f17b01a9..41882e87c 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): barrett, dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 03be7a77b..450d5c608 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: taking
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index b8fa85c03..8bfd2aef6 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_arith_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters
+ ** Major contributors: mdeters, cconway
  ** 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)