From 01bd928fa45459114ae4f5effcc8fbcf91bef7e8 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Tue, 27 Jul 2010 20:55:10 +0000
Subject: [PATCH] Moving EQ->IFF handling from TheoryEngine to parser/type
 checker

---
 src/parser/smt2/Smt2.g                         | 10 +++++++++-
 src/theory/builtin/theory_builtin_type_rules.h | 13 +++++++++++--
 src/theory/theory_engine.cpp                   |  2 +-
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 89c37883a..6919c86c4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -206,7 +206,15 @@ term[CVC4::Expr& expr]
 } 
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK 
-    { if( !PARSER_STATE->strictModeEnabled() && 
+    { 
+      if( kind == CVC4::kind::EQUAL &&
+          args.size() > 0 &&
+          args[0].getType() == EXPR_MANAGER->booleanType() ) {
+        /* Use IFF for boolean equalities. */
+        kind = CVC4::kind::IFF;
+      }
+
+      if( !PARSER_STATE->strictModeEnabled() && 
           (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && 
           args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
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];
-- 
2.30.2