1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index d8757926a..4eabf63de 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -558,6 +558,11 @@ private:
   /** The false node */
   Node d_false;
 
+  /**
+   * Adds an equality of terms t1 and t2 to the database.
+   */
+  void addEqualityInternal(TNode t1, TNode t2, TNode reason);
+
 public:
 
   /**
@@ -617,6 +622,11 @@ public:
   bool hasTerm(TNode t) const;
 
   /**
+   * Adds aa predicate t with given polarity
+   */
+  void addPredicate(TNode t, bool polarity, TNode reason);
+
+  /**
    * Adds an equality t1 = t2 to the database.
    */
   void addEquality(TNode t1, TNode t2, TNode reason);
@@ -693,6 +703,13 @@ public:
    * Check whether the two term are dis-equal.
    */
   bool areDisequal(TNode t1, TNode t2);
+
+  /**
+   * Return the number of nodes in the equivalence class contianing t
+   * Adds t if not already there.
+   */
+  size_t getSize(TNode t);
+
 };
 
 } // Namespace uf