From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 13 Aug 2012 19:46:27 +0000 (+0000)
Subject: Minor cleanup.  No performance difference expected.
X-Git-Tag: cvc5-1.0.0~7876
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=db2c74345f23b68a2421c15878311414a71cf210;p=cvc5.git

Minor cleanup.  No performance difference expected.
---

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 682a48bda..bad20b3b6 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -979,14 +979,11 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   Assert(types.size() >= 2);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
-    /* FIXME when congruence closure no longer abuses tuples */
-#if 0
     CheckArgument(!types[i].isFunctionLike(), types,
                   "cannot put function-like types in tuples");
     if(types[i].isBoolean()) {
       WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a tuple type with a Boolean argument)" << std::endl;
     }
-#endif /* 0 */
     typeNodes.push_back(types[i]);
   }
   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index d443b8452..ef7078624 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -146,21 +146,15 @@ public:
 };/* class StringConstantTypeRule */
 
 class SortProperties {
-//private:  //FIXME?
-//  static std::map< TypeNode, TNode > d_groundTerms;
 public:
   inline static bool isWellFounded(TypeNode type) {
     return true;
   }
   inline static Node mkGroundTerm(TypeNode type) {
     Assert(type.getKind() == kind::SORT_TYPE);
-    //if( d_groundTerms.find( type )==d_groundTerms.end() ){
-    //  d_groundTerms[type] = NodeManager::currentNM()->mkVar( type );
-    //}
-    //return d_groundTerms[type];
     return NodeManager::currentNM()->mkVar( type );
   }
-};
+};/* class SortProperties */
 
 class FunctionProperties {
 public: