diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:55:10 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:55:10 +0000 |
| commit | 01bd928fa45459114ae4f5effcc8fbcf91bef7e8 (patch) | |
| tree | d29748d3b830c807cc6577e60742045490735df1 /src/parser | |
| parent | 2564d8730f768a8305325d4b6cc08211d8a3281d (diff) | |
Moving EQ->IFF handling from TheoryEngine to parser/type checker
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 10 |
1 files changed, 9 insertions, 1 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. |