diff options
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4a8f7eb7b..470fc5253 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1985,6 +1985,11 @@ simpleTerm[CVC4::Expr& f] } } + /* set cardinality literal */ + | BAR BAR formula[f] { args.push_back(f); } BAR BAR + { f = MK_EXPR(kind::CARD, args[0]); + } + /* array literals */ | ARRAY_TOK /* { PARSER_STATE->pushScope(); } */ LPAREN restrictedType[t, CHECK_DECLARED] OF_TOK restrictedType[t2, CHECK_DECLARED] |