congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk

1 files changed, 11 insertions, 0 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 206cf35d5..04de81b1c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -472,6 +472,12 @@ public:
   inline TypeNode kindType();
 
   /**
+   * Get the (singleton) type for builtin operators (that is, the type
+   * of the Node returned from Node::getOperator() when the operator
+   * is built-in, like EQUAL). */
+  inline TypeNode builtinOperatorType();
+
+  /**
    * Make a function type from domain to range.
    *
    * @param domain the domain type
@@ -680,6 +686,11 @@ inline TypeNode NodeManager::kindType() {
   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
 }
 
+/** Get the (singleton) type for builtin operators. */
+inline TypeNode NodeManager::builtinOperatorType() {
+  return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
+}
+
 /** Make a function type from domain to range. */
 inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
   std::vector<TypeNode> sorts;