Minor cleanup.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index d87c498e64e46747b80495a78a80ffb536150428..5fe7b34c106fe1c7d648681ad6953e8db7fbbc77 100644 (file)
--- 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 335dd2b6d61e1e7dcfcfed00803997720c924a9b..af4752d131663e7dfc63c423332b61f650f7f8c7 100644 (file)
--- 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 f3855e713a36eae859f1371ee2d5f450b6eea769..657384e997c7fa439607b908cbbe5c5a4921f1e4 100644 (file)
--- 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]