diff options
Diffstat (limited to 'src')
-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 |