summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-06-12 16:18:04 +0000
committerMorgan Deters <mdeters@gmail.com>2012-06-12 16:18:04 +0000
commit2a92b09014430bedb9360d186e1d88144e07cf11 (patch)
tree39337a20c03f5f7a71f8aaf9fac2b37b4ff4eef1 /src/expr/node_manager.h
parent7f4e310c1ba02795bae56702e26cf8460f7e212b (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.h6
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));
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback