Moving EQ->IFF handling from TheoryEngine to parser/type checker

2 files changed, 12 insertions, 3 deletions

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 4458931a9..33e4c942f 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -32,12 +32,21 @@ namespace builtin {
 class EqualityTypeRule {
   public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) {
+    TypeNode booleanType = nodeManager->booleanType();
+
     if( check ) {
-      if (n[0].getType(check) != n[1].getType(check)) {
+      TypeNode lhsType = n[0].getType(check);
+      TypeNode rhsType = n[1].getType(check);
+
+      if ( lhsType != rhsType ) {
         throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
       }
+
+      if ( lhsType == booleanType ) {
+        throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)");
+      }
     }
-    return nodeManager->booleanType();
+    return booleanType;
   }
 };
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bf501ec37..8db81902d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -165,7 +165,7 @@ Theory* TheoryEngine::theoryOf(TNode n) {
     return theoryOf(n.getType());
   } else if(k == kind::EQUAL) {
     // equality is special: use LHS
-    return theoryOf(n[0].getType());
+    return theoryOf(n[0]);
   } else {
     // use our Kind-to-Theory mapping
     return d_theoryOfTable[k];