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

3 files changed, 17 insertions, 1 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 280c55254..9006bf4d9 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -228,6 +228,9 @@ TypeNode NodeManager::computeType(TNode n, bool check)
 
   // Infer the type
   switch(n.getKind()) {
+  case kind::BUILTIN:
+    typeNode = builtinOperatorType();
+    break;
   case kind::SORT_TYPE:
     typeNode = kindType();
     break;
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;
diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h
index 3001d4513..23c23cc9f 100644
--- a/src/expr/type_constant.h
+++ b/src/expr/type_constant.h
@@ -36,7 +36,9 @@ enum TypeConstant {
   /** The real type */
   REAL_TYPE,
   /** The kind type (type of types) */
-  KIND_TYPE
+  KIND_TYPE,
+  /** The builtin operator type (type of non-PARAMETERIZED operators) */
+  BUILTIN_OPERATOR_TYPE
 };/* enum TypeConstant */
 
 /**