Minor cleanup. No performance difference expected.

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 682a48bda4f9dd5eb88be22db8f5f9904afa7a42..bad20b3b65f94e6c0c51cecfec81dde81a409e4c 100644 (file)
--- 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 d443b8452b302ccd67e4fd5fd74a36ecb180072d..ef707862476fe4f35bc78a3af60638e1bb14986e 100644 (file)
--- 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: