From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 3 Dec 2013 00:32:59 +0000 (-0500)
Subject: Minor cleanup.
X-Git-Tag: cvc5-1.0.0~7223
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99152fedc21ec1772ddd4c915b4af616270c10c7;p=cvc5.git

Minor cleanup.
---

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index d87c498e6..5fe7b34c1 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -542,7 +542,7 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const {
 
 DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
   // Not worth a special implementation; this doesn't need to be fast
-  // code anyway..
+  // code anyway.
   vector<Datatype> datatypes;
   datatypes.push_back(datatype);
   vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes);
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 335dd2b6d..af4752d13 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -337,7 +337,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
   if(__builtin_expect( (t0 == t1), true )) {
     return t0;
   } else { // t0 != t1
-    if(t0.getKind()== kind::TYPE_CONSTANT) {
+    if(t0.getKind() == kind::TYPE_CONSTANT) {
       switch(t0.getConst<TypeConstant>()) {
       case INTEGER_TYPE:
         if(t1.isInteger()) {
@@ -363,7 +363,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
         }
       }
     } else if(t1.getKind() == kind::TYPE_CONSTANT) {
-      return leastCommonTypeNode(t1, t0); //decrease the number of special cases
+      return leastCommonTypeNode(t1, t0); // decrease the number of special cases
     } else {
       // t0 != t1 &&
       // t0.getKind() == kind::TYPE_CONSTANT &&
@@ -384,7 +384,7 @@ TypeNode TypeNode::leastCommonTypeNode(TypeNode t0, TypeNode t1){
         return TypeNode(); // Not sure if this is right
       case kind::SEXPR_TYPE:
         Unimplemented("haven't implemented leastCommonType for symbolic expressions yet");
-        return TypeNode(); // Not sure if this is right
+        return TypeNode();
       case kind::SUBTYPE_TYPE:
         if(t1.isPredicateSubtype()){
           // This is the case where both t0 and t1 are predicate subtypes.
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f3855e713..657384e99 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -708,11 +708,11 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | str[s]
     { sexpr = SExpr(s); }
-//  | LPAREN_TOK STRCST_TOK 
-//      ( INTEGER_LITERAL { 
+//  | LPAREN_TOK STRCST_TOK
+//      ( INTEGER_LITERAL {
 //	    s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 );
 //	  } )* RPAREN_TOK
-//   { 
+//   {
 //	sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) );
 //	}
   | symbol[s,CHECK_NONE,SYM_SORT]