1 files changed, 16 insertions, 2 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 5be32ab90..9638b9f09 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -230,6 +230,9 @@ private:
   /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */
   KindMap d_congruenceKindsInterpreted;
 
+  /** The map of kinds with operators to be considered external (for higher-order) */
+  KindMap d_congruenceKindsExtOperators;
+
   /** Objects that need to be notified during equality path reconstruction */
   std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
 
@@ -714,9 +717,13 @@ public:
   }
 
   /**
-   * Add a kind to treat as function applications.
+   * Add a kind to treat as function applications. 
+   * When extOperator is true, this equality engine will treat the operators of this kind 
+   * as "external" e.g. not internal nodes (see d_isInternal). This means that we will 
+   * consider equivalence classes containing the operators of such terms, and "hasTerm" will
+   * return true.
    */
-  void addFunctionKind(Kind fun, bool interpreted = false);
+  void addFunctionKind(Kind fun, bool interpreted = false, bool extOperator = false);
 
   /**
    * Returns true if this kind is used for congruence closure.
@@ -733,6 +740,13 @@ public:
   }
 
   /**
+   * Returns true if this kind has an operator that is considered external (e.g. not internal).
+   */
+  bool isExternalOperatorKind(Kind fun) const {
+    return d_congruenceKindsExtOperators.tst(fun);
+  }
+
+  /**
    * Check whether the node is already in the database.
    */
   bool hasTerm(TNode t) const;