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: Allow empty record literals (fixing an oversight in previous work on
 empty tuples/records)

---
 src/parser/cvc/Cvc.g | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/parser')

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)); }
-- 
cgit v1.2.3