From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 14 Nov 2013 14:33:34 +0000 (-0500)
Subject: Allow empty record literals (fixing an oversight in previous work on empty tuples... 
X-Git-Tag: cvc5-1.0.0~7251
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca54910668960ea492e8dc12178648032c5df489;p=cvc5.git

Allow empty record literals (fixing an oversight in previous work on empty tuples/records)
---

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