From ca54910668960ea492e8dc12178648032c5df489 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 14 Nov 2013 09:33:34 -0500
Subject: [PATCH] Allow empty record literals (fixing an oversight in previous
 work on empty tuples/records)

---
 src/parser/cvc/Cvc.g       | 5 +++++
 src/theory/datatypes/kinds | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

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
 
-- 
2.30.2