diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-12 16:18:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-12 16:18:04 +0000 |
commit | 2a92b09014430bedb9360d186e1d88144e07cf11 (patch) | |
tree | 39337a20c03f5f7a71f8aaf9fac2b37b4ff4eef1 /src/expr/node_manager.h | |
parent | 7f4e310c1ba02795bae56702e26cf8460f7e212b (diff) |
minor cleanup, and replace a "private:" in equality engine that had been removed by the quantifiers merge (I had reengineered some things from quantifiers so that the equality engine didn't have to expose internals as public, but then had neglected to re-privatize them)
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index e763a1f10..b900a6994 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -910,17 +910,17 @@ inline TypeNode NodeManager::kindType() { } /** Get the bound var list type. */ -inline TypeNode NodeManager::boundVarListType(){ +inline TypeNode NodeManager::boundVarListType() { return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE)); } /** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternType(){ +inline TypeNode NodeManager::instPatternType() { return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE)); } /** Get the instantiation pattern type. */ -inline TypeNode NodeManager::instPatternListType(){ +inline TypeNode NodeManager::instPatternListType() { return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE)); } |