summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-12-14 21:27:38 +0000
committerMorgan Deters <mdeters@gmail.com>2010-12-14 21:27:38 +0000
commit76154a935ff1065c346da197bac6303302b67ac2 (patch)
treedf5226c72e2bef95913e22e0e2fb2a7b051835f2 /src
parent96ce991a4b8593f7ec831c3a9b40b214d2ac3761 (diff)
make some CC module methods private that should not have been public
Diffstat (limited to 'src')
-rw-r--r--src/util/congruence_closure.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index 0968b39ed..4d50eb712 100644
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -234,6 +234,8 @@ public:
Node eq = eqb;
addEq(eq, inputEq);
}
+
+private:
void addEq(TNode eq, TNode inputEq);
Node flatten(TNode t) {
@@ -279,6 +281,7 @@ public:
}
}
+public:
/**
* Inquire whether two expressions are congruent in the current
* context.
@@ -310,6 +313,7 @@ public:
return ap == bp || normalize(ap) == normalize(bp);
}
+private:
/**
* Find the EC representative for a term t in the current context.
*/
@@ -327,6 +331,7 @@ public:
Node nearestCommonAncestor(TNode a, TNode b, UnionFind_t& unionFind)
throw(AssertionException);
+public:
/**
* Request an explanation for why a and b are in the same EC in the
* current context. Throws a CongruenceClosureException if they
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback