diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-07 11:17:34 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-07 11:17:34 -0600 |
| commit | ab68adfc44049598ee79a3c8b4379694d786d9aa (patch) | |
| tree | 1609ecda726c535466b4f7501d4dba5b72409ba9 /src/parser/cvc/Cvc.g | |
| parent | 105cae4ed94f0ce13b0525a348b29d2fc7d5af72 (diff) | |
More fixes for printing/parsing sets, fix kind name.
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 267fe303e..fb0304045 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -448,7 +448,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, default: break; } Expr e = em->mkExpr(k, lhs, rhs); - return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLIMENT : kind::NOT, e) : e; + return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLEMENT : kind::NOT, e) : e; }/* createPrecedenceTree() recursive variant */ Expr createPrecedenceTree(Parser* parser, ExprManager* em, @@ -474,7 +474,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, /** Add n NOTs to the front of e and return the result. */ Expr addNots(ExprManager* em, size_t n, Expr e) { - Kind k = e.getType().isSet() ? kind::COMPLIMENT : kind::NOT; + Kind k = e.getType().isSet() ? kind::COMPLEMENT : kind::NOT; while(n-- > 0) { e = em->mkExpr(k, e); } @@ -1689,6 +1689,8 @@ bvNegTerm[CVC4::Expr& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } + | NOT_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::COMPLEMENT, f); } | TRANSPOSE_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } | TRANSCLOSURE_TOK bvNegTerm[f] |