diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 14:09:57 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-07 14:09:57 -0600 |
| commit | e43b45b42ee786f4dd103aa68d67915504c1f59c (patch) | |
| tree | 0b56c6395cda4feda9be7967869d7a8e5312d0c3 /src/parser | |
| parent | d2e45128356c725d479a3efff475d8e5f430e4f3 (diff) | |
Added cardinality to cvc language, fixes bug 753. Throw logic exception when using cardinality on sets with finite element type.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 1b1137a9d..8d76a5122 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -242,6 +242,7 @@ tokens { //REGEXP_EMPTY_TOK //REGEXP_SIGMA_TOK + SETS_CARD_TOK = 'CARD'; FMF_CARD_TOK = 'HAS_CARD'; @@ -328,6 +329,7 @@ int getOperatorPrecedence(int type) { case GEQ_TOK: case GT_TOK: case MEMBER_TOK: + case SETS_CARD_TOK: case FMF_CARD_TOK: return 25; case EQUAL_TOK: case DISEQUAL_TOK: return 26; @@ -371,6 +373,7 @@ Kind getOperatorKind(int type, bool& negate) { case LT_TOK: return kind::LT; case LEQ_TOK: return kind::LEQ; case MEMBER_TOK: return kind::MEMBER; + case SETS_CARD_TOK: return kind::CARD; case FMF_CARD_TOK: return kind::CARDINALITY_CONSTRAINT; // arithmeticBinop @@ -2012,8 +2015,18 @@ stringTerm[CVC4::Expr& f] | str[s] { f = MK_CONST(CVC4::String(s)); } + | setsTerm[f] + ; + +setsTerm[CVC4::Expr& f] +@init { +} + /* Sets prefix operators */ + : SETS_CARD_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::CARD, f); } | simpleTerm[f] ; + /** Parses a simple term. */ simpleTerm[CVC4::Expr& f] |