Removing the throw specifiers from SExpr.

2 files changed, 202 insertions, 232 deletions

diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index efb90302f..a34689d1e 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -17,9 +17,9 @@
  ** this being implemented on SExpr and not on the Printer class is that the
  ** Printer class lives in libcvc4. It has to currently as it prints fairly
  ** complicated objects, like Model, which in turn uses SmtEngine pointers.
- ** However, SExprs need to be printed by Statistics. To get the output consistent
- ** with the previous version, the printing of SExprs in different languages is
- ** handled in the SExpr class and the libexpr library.
+ ** However, SExprs need to be printed by Statistics. To get the output
+ ** consistent with the previous version, the printing of SExprs in different
+ ** languages is handled in the SExpr class and the libexpr library.
  **/
 
 #include "util/sexpr.h"
@@ -41,9 +41,8 @@ std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
   return out;
 }
 
-
 SExpr::~SExpr() {
-  if(d_children != NULL){
+  if (d_children != NULL) {
     delete d_children;
     d_children = NULL;
   }
@@ -56,98 +55,88 @@ SExpr& SExpr::operator=(const SExpr& other) {
   d_rationalValue = other.d_rationalValue;
   d_stringValue = other.d_stringValue;
 
-  if(d_children == NULL && other.d_children == NULL){
+  if (d_children == NULL && other.d_children == NULL) {
     // Do nothing.
-  } else if(d_children == NULL){
+  } else if (d_children == NULL) {
     d_children = new SExprVector(*other.d_children);
-  } else if(other.d_children == NULL){
+  } else if (other.d_children == NULL) {
     delete d_children;
     d_children = NULL;
   } else {
     (*d_children) = other.getChildren();
   }
-  Assert( isAtom() == other.isAtom() );
-  Assert( (d_children == NULL) == isAtom() );
+  Assert(isAtom() == other.isAtom());
+  Assert((d_children == NULL) == isAtom());
   return *this;
 }
 
-SExpr::SExpr() :
-    d_sexprType(SEXPR_STRING),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(NULL) {
-}
-
-
-SExpr::SExpr(const SExpr& other) :
-    d_sexprType(other.d_sexprType),
-    d_integerValue(other.d_integerValue),
-    d_rationalValue(other.d_rationalValue),
-    d_stringValue(other.d_stringValue),
-    d_children(NULL)
-{
-  d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children);
+SExpr::SExpr()
+    : d_sexprType(SEXPR_STRING),
+      d_integerValue(0),
+      d_rationalValue(0),
+      d_stringValue(""),
+      d_children(NULL) {}
+
+SExpr::SExpr(const SExpr& other)
+    : d_sexprType(other.d_sexprType),
+      d_integerValue(other.d_integerValue),
+      d_rationalValue(other.d_rationalValue),
+      d_stringValue(other.d_stringValue),
+      d_children(NULL) {
+  d_children =
+      (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children);
   // d_children being NULL is equivalent to the node being an atom.
-  Assert( (d_children == NULL) == isAtom() );
-}
-
-
-SExpr::SExpr(const CVC4::Integer& value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(NULL) {
-  }
-
-SExpr::SExpr(int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(long int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(unsigned int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(unsigned long int value) :
-    d_sexprType(SEXPR_INTEGER),
-    d_integerValue(value),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(const CVC4::Rational& value) :
-    d_sexprType(SEXPR_RATIONAL),
-    d_integerValue(0),
-    d_rationalValue(value),
-    d_stringValue(""),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(const std::string& value) :
-    d_sexprType(SEXPR_STRING),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(value),
-    d_children(NULL) {
-}
+  Assert((d_children == NULL) == isAtom());
+}
+
+SExpr::SExpr(const CVC4::Integer& value)
+    : d_sexprType(SEXPR_INTEGER),
+      d_integerValue(value),
+      d_rationalValue(0),
+      d_stringValue(""),
+      d_children(NULL) {}
+
+SExpr::SExpr(int value)
+    : d_sexprType(SEXPR_INTEGER),
+      d_integerValue(value),
+      d_rationalValue(0),
+      d_stringValue(""),
+      d_children(NULL) {}
+
+SExpr::SExpr(long int value)
+    : d_sexprType(SEXPR_INTEGER),
+      d_integerValue(value),
+      d_rationalValue(0),
+      d_stringValue(""),
+      d_children(NULL) {}
+
+SExpr::SExpr(unsigned int value)
+    : d_sexprType(SEXPR_INTEGER),
+      d_integerValue(value),
+      d_rationalValue(0),
+      d_stringValue(""),
+      d_children(NULL) {}
+
+SExpr::SExpr(unsigned long int value)
+    : d_sexprType(SEXPR_INTEGER),
+      d_integerValue(value),
+      d_rationalValue(0),
+      d_stringValue(""),
+      d_children(NULL) {}
+
+SExpr::SExpr(const CVC4::Rational& value)
+    : d_sexprType(SEXPR_RATIONAL),
+      d_integerValue(0),
+      d_rationalValue(value),
+      d_stringValue(""),
+      d_children(NULL) {}
+
+SExpr::SExpr(const std::string& value)
+    : d_sexprType(SEXPR_STRING),
+      d_integerValue(0),
+      d_rationalValue(0),
+      d_stringValue(value),
+      d_children(NULL) {}
 
 /**
  * This constructs a string expression from a const char* value.
@@ -155,37 +144,33 @@ SExpr::SExpr(const std::string& value) :
  * Given the other constructors this SExpr("foo") converts to bool.
  * instead of SExpr(string("foo")).
  */
-SExpr::SExpr(const char* value) :
-    d_sexprType(SEXPR_STRING),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(value),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(bool value) :
-    d_sexprType(SEXPR_KEYWORD),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(value ? "true" : "false"),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(const Keyword& value) :
-    d_sexprType(SEXPR_KEYWORD),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(value.getString()),
-    d_children(NULL) {
-}
-
-SExpr::SExpr(const std::vector<SExpr>& children) :
-    d_sexprType(SEXPR_NOT_ATOM),
-    d_integerValue(0),
-    d_rationalValue(0),
-    d_stringValue(""),
-    d_children(new SExprVector(children)) {
-}
+SExpr::SExpr(const char* value)
+    : d_sexprType(SEXPR_STRING),
+      d_integerValue(0),
+      d_rationalValue(0),
+      d_stringValue(value),
+      d_children(NULL) {}
+
+SExpr::SExpr(bool value)
+    : d_sexprType(SEXPR_KEYWORD),
+      d_integerValue(0),
+      d_rationalValue(0),
+      d_stringValue(value ? "true" : "false"),
+      d_children(NULL) {}
+
+SExpr::SExpr(const Keyword& value)
+    : d_sexprType(SEXPR_KEYWORD),
+      d_integerValue(0),
+      d_rationalValue(0),
+      d_stringValue(value.getString()),
+      d_children(NULL) {}
+
+SExpr::SExpr(const std::vector<SExpr>& children)
+    : d_sexprType(SEXPR_NOT_ATOM),
+      d_integerValue(0),
+      d_rationalValue(0),
+      d_stringValue(""),
+      d_children(new SExprVector(children)) {}
 
 std::string SExpr::toString() const {
   std::stringstream ss;
@@ -194,68 +179,61 @@ std::string SExpr::toString() const {
 }
 
 /** Is this S-expression an atom? */
-bool SExpr::isAtom() const {
-  return d_sexprType != SEXPR_NOT_ATOM;
-}
+bool SExpr::isAtom() const { return d_sexprType != SEXPR_NOT_ATOM; }
 
 /** Is this S-expression an integer? */
-bool SExpr::isInteger() const {
-  return d_sexprType == SEXPR_INTEGER;
-}
+bool SExpr::isInteger() const { return d_sexprType == SEXPR_INTEGER; }
 
 /** Is this S-expression a rational? */
-bool SExpr::isRational() const {
-  return d_sexprType == SEXPR_RATIONAL;
-}
+bool SExpr::isRational() const { return d_sexprType == SEXPR_RATIONAL; }
 
 /** Is this S-expression a string? */
-bool SExpr::isString() const {
-  return d_sexprType == SEXPR_STRING;
-}
+bool SExpr::isString() const { return d_sexprType == SEXPR_STRING; }
 
 /** Is this S-expression a keyword? */
-bool SExpr::isKeyword() const {
-  return d_sexprType == SEXPR_KEYWORD;
-}
-
+bool SExpr::isKeyword() const { return d_sexprType == SEXPR_KEYWORD; }
 
 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
   SExpr::toStream(out, sexpr);
   return out;
 }
 
-void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() {
+void SExpr::toStream(std::ostream& out, const SExpr& sexpr) {
   toStream(out, sexpr, language::SetLanguage::getLanguage(out));
 }
 
-void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() {
-  toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0);
+void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
+                     OutputLanguage language) {
+  const int indent = PrettySExprs::getPrettySExprs(out) ? 2 : 0;
+  toStream(out, sexpr, language, indent);
 }
 
-void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
-  if( sexpr.isKeyword() && languageQuotesKeywords(language) ){
+void SExpr::toStream(std::ostream& out, const SExpr& sexpr,
+                     OutputLanguage language, int indent) {
+  if (sexpr.isKeyword() && languageQuotesKeywords(language)) {
     out << quoteSymbol(sexpr.getValue());
   } else {
     toStreamRec(out, sexpr, language, indent);
   }
 }
 
-
-void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() {
-  if(sexpr.isInteger()) {
+void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
+                        OutputLanguage language, int indent) {
+  if (sexpr.isInteger()) {
     out << sexpr.getIntegerValue();
-  } else if(sexpr.isRational()) {
-    out << std::fixed << sexpr.getRationalValue().getDouble();
-  } else if(sexpr.isKeyword()) {
+  } else if (sexpr.isRational()) {
+    const double approximation = sexpr.getRationalValue().getDouble();
+    out << std::fixed << approximation;
+  } else if (sexpr.isKeyword()) {
     out << sexpr.getValue();
-  } else if(sexpr.isString()) {
+  } else if (sexpr.isString()) {
     std::string s = sexpr.getValue();
     // escape backslash and quote
-    for(size_t i = 0; i < s.length(); ++i) {
-      if(s[i] == '"') {
+    for (size_t i = 0; i < s.length(); ++i) {
+      if (s[i] == '"') {
         s.replace(i, 1, "\\\"");
         ++i;
-      } else if(s[i] == '\\') {
+      } else if (s[i] == '\\') {
         s.replace(i, 1, "\\\\");
         ++i;
       }
@@ -265,31 +243,32 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage la
     const std::vector<SExpr>& kids = sexpr.getChildren();
     out << (indent > 0 && kids.size() > 1 ? "( " : "(");
     bool first = true;
-    for(std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
-      if(first) {
+    for (std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end();
+         ++i) {
+      if (first) {
         first = false;
       } else {
-        if(indent > 0) {
+        if (indent > 0) {
           out << "\n" << std::string(indent, ' ');
         } else {
           out << ' ';
         }
       }
-      toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2);
+      toStreamRec(out, *i, language,
+                  indent <= 0 || indent > 2 ? 0 : indent + 2);
     }
-    if(indent > 0 && kids.size() > 1) {
+    if (indent > 0 && kids.size() > 1) {
       out << '\n';
-      if(indent > 2) {
+      if (indent > 2) {
         out << std::string(indent - 2, ' ');
       }
     }
     out << ')';
   }
-}/* toStreamRec() */
-
+} /* toStreamRec() */
 
 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
-  switch(language) {
+  switch (language) {
     case language::output::LANG_SMTLIB_V1:
     case language::output::LANG_SMTLIB_V2_0:
     case language::output::LANG_SMTLIB_V2_5:
@@ -305,83 +284,76 @@ bool SExpr::languageQuotesKeywords(OutputLanguage language) {
   };
 }
 
-
-
 std::string SExpr::getValue() const {
-  PrettyCheckArgument( isAtom(), this );
-  switch(d_sexprType) {
-  case SEXPR_INTEGER:
-    return d_integerValue.toString();
-  case SEXPR_RATIONAL: {
-    // We choose to represent rationals as decimal strings rather than
-    // "numerator/denominator."  Perhaps an additional SEXPR_DECIMAL
-    // could be added if we need both styles, even if it's backed by
-    // the same Rational object.
-    std::stringstream ss;
-    ss << std::fixed << d_rationalValue.getDouble();
-    return ss.str();
-  }
-  case SEXPR_STRING:
-  case SEXPR_KEYWORD:
-    return d_stringValue;
-  case SEXPR_NOT_ATOM:
-    return std::string();
+  PrettyCheckArgument(isAtom(), this);
+  switch (d_sexprType) {
+    case SEXPR_INTEGER:
+      return d_integerValue.toString();
+    case SEXPR_RATIONAL: {
+      // We choose to represent rationals as decimal strings rather than
+      // "numerator/denominator."  Perhaps an additional SEXPR_DECIMAL
+      // could be added if we need both styles, even if it's backed by
+      // the same Rational object.
+      std::stringstream ss;
+      ss << std::fixed << d_rationalValue.getDouble();
+      return ss.str();
+    }
+    case SEXPR_STRING:
+    case SEXPR_KEYWORD:
+      return d_stringValue;
+    case SEXPR_NOT_ATOM:
+      return std::string();
   }
   return std::string();
-
 }
 
 const CVC4::Integer& SExpr::getIntegerValue() const {
-  PrettyCheckArgument( isInteger(), this );
+  PrettyCheckArgument(isInteger(), this);
   return d_integerValue;
 }
 
 const CVC4::Rational& SExpr::getRationalValue() const {
-  PrettyCheckArgument( isRational(), this );
+  PrettyCheckArgument(isRational(), this);
   return d_rationalValue;
 }
 
 const std::vector<SExpr>& SExpr::getChildren() const {
-  PrettyCheckArgument( !isAtom(), this );
-  Assert( d_children != NULL );
+  PrettyCheckArgument(!isAtom(), this);
+  Assert(d_children != NULL);
   return *d_children;
 }
 
 bool SExpr::operator==(const SExpr& s) const {
-  if (d_sexprType == s.d_sexprType &&
-      d_integerValue == s.d_integerValue &&
+  if (d_sexprType == s.d_sexprType && d_integerValue == s.d_integerValue &&
       d_rationalValue == s.d_rationalValue &&
       d_stringValue == s.d_stringValue) {
-    if(d_children == NULL && s.d_children == NULL){
+    if (d_children == NULL && s.d_children == NULL) {
       return true;
-    } else if(d_children != NULL && s.d_children != NULL){
+    } else if (d_children != NULL && s.d_children != NULL) {
       return getChildren() == s.getChildren();
     }
   }
   return false;
 }
 
-bool SExpr::operator!=(const SExpr& s) const {
-  return !(*this == s);
-}
-
+bool SExpr::operator!=(const SExpr& s) const { return !(*this == s); }
 
 SExpr SExpr::parseAtom(const std::string& atom) {
-  if(atom == "true"){
+  if (atom == "true") {
     return SExpr(true);
-  } else if(atom == "false"){
+  } else if (atom == "false") {
     return SExpr(false);
   } else {
     try {
       Integer z(atom);
       return SExpr(z);
-    }catch(std::invalid_argument&){
+    } catch (std::invalid_argument&) {
       // Fall through to the next case
     }
     try {
       Rational q(atom);
       return SExpr(q);
-    }catch(std::invalid_argument&){
+    } catch (std::invalid_argument&) {
       // Fall through to the next case
     }
     return SExpr(atom);
@@ -391,21 +363,21 @@ SExpr SExpr::parseAtom(const std::string& atom) {
 SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) {
   std::vector<SExpr> parsedAtoms;
   typedef std::vector<std::string>::const_iterator const_iterator;
-  for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){
+  for (const_iterator i = atoms.begin(), i_end = atoms.end(); i != i_end; ++i) {
     parsedAtoms.push_back(parseAtom(*i));
   }
   return SExpr(parsedAtoms);
 }
 
-SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists) {
+SExpr SExpr::parseListOfListOfAtoms(
+    const std::vector<std::vector<std::string> >& atoms_lists) {
   std::vector<SExpr> parsedListsOfAtoms;
-  typedef std::vector< std::vector<std::string> >::const_iterator const_iterator;
-  for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){
+  typedef std::vector<std::vector<std::string> >::const_iterator const_iterator;
+  for (const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end();
+       i != i_end; ++i) {
     parsedListsOfAtoms.push_back(parseListOfAtoms(*i));
   }
   return SExpr(parsedListsOfAtoms);
 }
 
-
-
-}/* CVC4 namespace */
+} /* CVC4 namespace */
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 9c80a1b1f..2948cba4b 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -40,18 +40,18 @@ namespace CVC4 {
 
 class CVC4_PUBLIC SExprKeyword {
   std::string d_str;
-public:
+
+ public:
   SExprKeyword(const std::string& s) : d_str(s) {}
   const std::string& getString() const { return d_str; }
-};/* class SExpr::Keyword */
+}; /* class SExpr::Keyword */
 
 /**
  * A simple S-expression. An S-expression is either an atom with a
  * string value, or a list of other S-expressions.
  */
 class CVC4_PUBLIC SExpr {
-public:
-
+ public:
   typedef SExprKeyword Keyword;
 
   SExpr();
@@ -138,7 +138,6 @@ public:
   /** Is this S-expression different from another? */
   bool operator!=(const SExpr& s) const;
 
-
   /**
    * This returns the best match in the following order:
    * match atom with
@@ -157,21 +156,23 @@ public:
   /**
    * Parses a list of list of atoms.
    */
-  static SExpr parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists);
-
+  static SExpr parseListOfListOfAtoms(
+      const std::vector<std::vector<std::string> >& atoms_lists);
 
   /**
    * Outputs the SExpr onto the ostream out. This version reads defaults to the
-   * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is
+   * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level
+   * is
    * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise.
    */
-  static void toStream(std::ostream& out, const SExpr& sexpr) throw();
+  static void toStream(std::ostream& out, const SExpr& sexpr);
 
   /**
    * Outputs the SExpr onto the ostream out. This version sets the indent level
    * to 2 if PrettySExprs::getPrettySExprs() is on.
    */
-  static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw();
+  static void toStream(std::ostream& out, const SExpr& sexpr,
+                       OutputLanguage language);
 
   /**
    * Outputs the SExpr onto the ostream out.
@@ -181,19 +182,20 @@ public:
    * Otherwise this prints using toStreamRec().
    *
    * TIM: Keywords that are children are not currently quoted. This seems
-   * incorrect but I am just reproduicing the old behavior even if it does not make
+   * incorrect but I am just reproduicing the old behavior even if it does not
+   * make
    * sense.
    */
-  static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw();
-
-private:
+  static void toStream(std::ostream& out, const SExpr& sexpr,
+                       OutputLanguage language, int indent);
 
+ private:
   /**
    * Simple printer for SExpr to an ostream.
    * The current implementation is language independent.
    */
-  static void toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw();
-
+  static void toStreamRec(std::ostream& out, const SExpr& sexpr,
+                          OutputLanguage language, int indent);
 
   /** Returns true if this language quotes Keywords when printing. */
   static bool languageQuotesKeywords(OutputLanguage language);
@@ -222,11 +224,12 @@ private:
    * Whenever the SExpr isAtom() holds, this points at NULL.
    *
    * This should be a pointer in case the implementation of vector<SExpr> ever
-   * directly contained or allocated an SExpr. If this happened this would trigger,
+   * directly contained or allocated an SExpr. If this happened this would
+   * trigger,
    * either the size being infinite or SExpr() being an infinite loop.
    */
   SExprVector* d_children;
-};/* class SExpr */
+}; /* class SExpr */
 
 /** Prints an SExpr. */
 std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC;
@@ -245,7 +248,7 @@ class CVC4_PUBLIC PrettySExprs {
    */
   bool d_prettySExprs;
 
-public:
+ public:
   /**
    * Construct a PrettySExprs with the given setting.
    */
@@ -273,21 +276,17 @@ public:
     std::ostream& d_out;
     bool d_oldPrettySExprs;
 
-  public:
-
-    inline Scope(std::ostream& out, bool prettySExprs) :
-      d_out(out),
-      d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
+   public:
+    inline Scope(std::ostream& out, bool prettySExprs)
+        : d_out(out), d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
       PrettySExprs::setPrettySExprs(out, prettySExprs);
     }
 
-    inline ~Scope() {
-      PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs);
-    }
+    inline ~Scope() { PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); }
 
-  };/* class PrettySExprs::Scope */
+  }; /* class PrettySExprs::Scope */
 
-};/* class PrettySExprs */
+}; /* class PrettySExprs */
 
 /**
  * Sets the default pretty-sexprs setting for an ostream.  Use like this:
@@ -299,7 +298,6 @@ public:
  */
 std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
 
-
-}/* CVC4 namespace */
+} /* CVC4 namespace */
 
 #endif /* __CVC4__SEXPR_H */