diff options
| author | Paul Meng <baolmeng@gmail.com> | 2017-04-20 14:04:24 -0500 |
|---|---|---|
| committer | Paul Meng <baolmeng@gmail.com> | 2017-04-20 14:04:24 -0500 |
| commit | 7152d6136fc8bd4701d9440ba3eee6bb7bf3a16c (patch) | |
| tree | 9012cc085fcde111d5a0609441415cdbb1a7b460 /src/parser/cvc/Cvc.g | |
| parent | c110fa8d07b5650c671b99797c17822e757bc52f (diff) | |
Support for relational operators identity and join image
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2dc74afdb..b5bad6a2d 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -209,6 +209,8 @@ tokens { TRANSPOSE_TOK = 'TRANSPOSE'; PRODUCT_TOK = 'PRODUCT'; TRANSCLOSURE_TOK = 'TCLOSURE'; + IDEN_TOK = 'IDEN'; + JOIN_IMAGE_TOK = 'JOIN_IMAGE'; // Strings @@ -324,6 +326,8 @@ int getOperatorPrecedence(int type) { case JOIN_TOK: case TRANSPOSE_TOK: case PRODUCT_TOK: + case IDEN_TOK: + case JOIN_IMAGE_TOK: case TRANSCLOSURE_TOK: return 24; case LEQ_TOK: case LT_TOK: @@ -365,6 +369,7 @@ Kind getOperatorKind(int type, bool& negate) { case PRODUCT_TOK: return kind::PRODUCT; case JOIN_TOK: return kind::JOIN; + case JOIN_IMAGE_TOK: return kind::JOIN_IMAGE; // comparisonBinop case EQUAL_TOK: return kind::EQUAL; @@ -1509,6 +1514,7 @@ booleanBinop[unsigned& op] | AND_TOK | JOIN_TOK | PRODUCT_TOK + | JOIN_IMAGE_TOK ; comparison[CVC4::Expr& f] @@ -1706,7 +1712,9 @@ relationTerm[CVC4::Expr& f] const Datatype& dt = t.getDatatype(); args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); - } + } + | IDEN_TOK relationTerm[f] + { f = MK_EXPR(CVC4::kind::IDEN, f); } | postfixTerm[f] ; |