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 /src/theory | |
parent | ecdd09877ecc4c07a22cc27cd2dd5441134476ba (diff) |
Minor cleanup. No performance difference expected.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 8 |
1 files changed, 1 insertions, 7 deletions
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: |