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 | |
| parent | e868c3d05660fe5d8dc1da8a104da850f4d101d5 (diff) | |
Allow empty record literals (fixing an oversight in previous work on empty tuples/records)
| -rw-r--r-- | src/parser/cvc/Cvc.g | 5 | ||||
| -rw-r--r-- | src/theory/datatypes/kinds | 2 |
2 files changed, 6 insertions, 1 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)); } diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 81ef32b32..bb6fd4373 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -136,7 +136,7 @@ enumerator RECORD_TYPE \ "::CVC4::theory::datatypes::RecordEnumerator" \ "theory/datatypes/type_enumerator.h" -parameterized RECORD RECORD_TYPE 1: "a record" +parameterized RECORD RECORD_TYPE 0: "a record" typerule RECORD ::CVC4::theory::datatypes::RecordTypeRule construle RECORD ::CVC4::theory::datatypes::RecordProperties |