From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 14 Dec 2010 21:27:38 +0000 (+0000)
Subject: make some CC module methods private that should not have been public
X-Git-Tag: cvc5-1.0.0~8719
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76154a935ff1065c346da197bac6303302b67ac2;p=cvc5.git

make some CC module methods private that should not have been public
---

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