summaryrefslogtreecommitdiff
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
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)
-rw-r--r--src/expr/node.h4
-rw-r--r--src/expr/node_manager.h6
-rw-r--r--src/theory/uf/equality_engine.h2
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback