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

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 89c37883a8610fc66d6e85631890ce0ff894ed60..6919c86c4e3401c1a419e8da8f214a240cad3745 100644 (file)
--- 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 4458931a9de6dd0f29473de6a98fe3e002b2b353..33e4c942f32db0bc503c4e2071d949eefd32a2fc 100644 (file)
--- 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 bf501ec376c33fca473afeccf37f04711dca0228..8db81902d8056a1f501bf9115df1f77ccf64b6de 100644 (file)
--- 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];