diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 | ||||
| -rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 13 | ||||
| -rw-r--r-- | 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]; |