diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-14 09:33:34 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-14 09:33:34 -0500 |
| commit | ca54910668960ea492e8dc12178648032c5df489 (patch) | |
| tree | c1164f2123ed9c8d47d150222edef7febace8ab8 /src/parser | |
| parent | e868c3d05660fe5d8dc1da8a104da850f4d101d5 (diff) | |
Allow empty record literals (fixing an oversight in previous work on empty tuples/records)
Diffstat (limited to 'src/parser')
| -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 03d1e7a8a..3ab6079a2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1845,6 +1845,11 @@ simpleTerm[CVC4::Expr& f] /* empty tuple literal */ | LPAREN RPAREN { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); } + /* empty record literal */ + | PARENHASH HASHPAREN + { RecordType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); + f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>()); + } /* boolean literals */ | TRUE_TOK { f = MK_CONST(bool(true)); } |