Allow empty record literals (fixing an oversight in previous work on empty tuples...

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 03d1e7a8a5d294124640e2460f0fb6a5987ece08..3ab6079a27c766db8868f13acca528c1f310540b 100644 (file)
--- 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 81ef32b32edd4a3e4649cdac3c003ceddb3246aa..bb6fd43732a7e750136352748fac1af62a6444ae 100644 (file)
--- 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