diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-08-13 19:46:27 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-08-13 19:46:27 +0000 |
| commit | db2c74345f23b68a2421c15878311414a71cf210 (patch) | |
| tree | 650340a3bc6e5f11c31942a5d4eef27a45adf2e7 | |
| parent | ecdd09877ecc4c07a22cc27cd2dd5441134476ba (diff) | |
Minor cleanup. No performance difference expected.
| -rw-r--r-- | src/expr/node_manager.h | 3 | ||||
| -rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 8 |
2 files changed, 1 insertions, 10 deletions
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: |