diff options
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 8d76a5122..3a8f3a794 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -356,7 +356,7 @@ Kind getOperatorKind(int type, bool& negate) { switch(type) { // booleanBinop - case IFF_TOK: return kind::IFF; + case IFF_TOK: return kind::EQUAL; case IMPLIES_TOK: return kind::IMPLIES; case OR_TOK: return kind::OR; case XOR_TOK: return kind::XOR; @@ -440,16 +440,6 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex); switch(k) { - case kind::EQUAL: { - if(lhs.getType().isBoolean()) { - if(parser->strictModeEnabled()) { - WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl; - } else { - k = kind::IFF; - } - } - break; - } case kind::LEQ : if(lhs.getType().isSet()) { k = kind::SUBSET; } break; case kind::MINUS : if(lhs.getType().isSet()) { k = kind::SETMINUS; } break; case kind::BITVECTOR_AND: if(lhs.getType().isSet()) { k = kind::INTERSECTION; } break; |