From: Christopher L. Conway Date: Tue, 27 Jul 2010 20:55:10 +0000 (+0000) Subject: Moving EQ->IFF handling from TheoryEngine to parser/type checker X-Git-Tag: cvc5-1.0.0~8904 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=01bd928fa45459114ae4f5effcc8fbcf91bef7e8;p=cvc5.git 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 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];