diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/parser/cvc | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/parser/cvc')
| -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; |