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 | |
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)
-rw-r--r-- | src/expr/node.h | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 6 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index e56774d7e..0b150d25d 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -230,7 +230,9 @@ class NodeTemplate { Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); } } + public: + /** * Cache-aware, recursive version of substitute() used by the public * member function with a similar signature. @@ -255,8 +257,6 @@ public: Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd, std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const; -public: - /** Default constructor, makes a null expression. */ NodeTemplate() : d_nv(&expr::NodeValue::s_null) { } 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)); } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index cb0c81872..e7e8893a3 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -190,7 +190,7 @@ public: */ void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId); -//private: +private: /** The context we are using */ context::Context* d_context; |