Support empty (and 1-ary) tuples and records.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 424ebab11759756a526a0a0ee705ba26282c8437..a838d6d30959817a69a922d265398916b4afe207 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -509,7 +509,6 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
 
 TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( types.size() >= 1 );
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
      typeNodes.push_back(*types[i].d_typeNode);

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f44c7e78bb749ed4815a074c12aa35354667ff70..7c84f3f15e6bef583b9fc7895645d0524e3024ad 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1090,7 +1090,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
 }
 
 inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
-  Assert(types.size() >= 1);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
     CheckArgument(!types[i].isFunctionLike(), types,

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 51ea87e39567152b05a68781a9b24d67d4be085b..cbdee9c74ad0a79d11b7b0238724b5eaa6b147e5 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1163,15 +1163,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     }
 
     /* tuple types / old-style function types */
-  | LBRACKET type[t,check] { types.push_back(t); }
-    ( COMMA type[t,check] { types.push_back(t); } )* RBRACKET
-    { if(types.size() == 1) {
-        if(types.front().isFunction()) {
-          // old style function syntax [ T -> U ]
-          PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax");
-        } else {
-          PARSER_STATE->parseError("I'm not sure what you're trying to do here; tuples must have > 1 type");
-        }
+  | LBRACKET ( type[t,check] { types.push_back(t); }
+    ( COMMA type[t,check] { types.push_back(t); } )* )? RBRACKET
+    { if(types.size() == 1 && types.front().isFunction()) {
+        // old style function syntax [ T -> U ]
+        PARSER_STATE->parseError("old-style function type syntax not supported anymore; please use the new syntax");
       } else {
         // tuple type [ T, U, V... ]
         t = EXPR_MANAGER->mkTupleType(types);
@@ -1179,8 +1175,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     }
 
     /* record types */
-  | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); }
-    ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* HASHSQ
+  | SQHASH ( identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); }
+    ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] { typeIds.push_back(std::make_pair(id, t)); } )* )? HASHSQ
     { t = EXPR_MANAGER->mkRecordType(typeIds); }
 
     /* bitvector types */
@@ -1846,6 +1842,10 @@ simpleTerm[CVC4::Expr& f]
       }
     }
 
+    /* empty tuple literal */
+  | LPAREN RPAREN
+    { f = MK_EXPR(kind::TUPLE, std::vector<Expr>()); }
+
     /* boolean literals */
   | TRUE_TOK  { f = MK_CONST(bool(true)); }
   | FALSE_TOK { f = MK_CONST(bool(false)); }

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 2e58677dfb8e19e370ff0da4052567c8725add11..81ef32b32edd4a3e4649cdac3c003ceddb3246aa 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -88,7 +88,7 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType
 # constructor applications are constant if they are applied only to constants
 construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 
-operator TUPLE_TYPE 1: "tuple type"
+operator TUPLE_TYPE 0: "tuple type"
 cardinality TUPLE_TYPE \
     "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \
     "theory/datatypes/theory_datatypes_type_rules.h"
@@ -100,7 +100,7 @@ enumerator TUPLE_TYPE \
     "::CVC4::theory::datatypes::TupleEnumerator" \
     "theory/datatypes/type_enumerator.h"
 
-operator TUPLE 1: "a tuple"
+operator TUPLE 0: "a tuple"
 typerule TUPLE ::CVC4::theory::datatypes::TupleTypeRule
 construle TUPLE ::CVC4::theory::datatypes::TupleProperties
 

diff --git a/src/util/record.h b/src/util/record.h
index 3d6481320faf7ef33516942922b4bb1d4fe495fa..63c54930ec0427f598d6cd36d301ec20a9ce4367 100644 (file)
--- a/src/util/record.h
+++ b/src/util/record.h
@@ -91,7 +91,6 @@ public:
 
   Record(const std::vector< std::pair<std::string, Type> >& fields) :
     d_fields(fields) {
-    CheckArgument(! fields.empty(), fields, "fields in record description cannot be empty");
   }
 
   const_iterator find(std::string name) const {

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 06227ad3aaa97810fa990421d0df8deee0f651b3..b95261d5600744153ed8bd1c866c538be83c60b3 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -30,6 +30,7 @@ TESTS =       \
        datatype3.cvc \
        datatype4.cvc \
        datatype13.cvc \
+       empty_tuprec.cvc \
        mutually-recursive.cvc \
        rewriter.cvc \
        typed_v1l50016-simp.cvc \

diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc
new file mode 100644 (file)
index 0000000..8e163e8
--- /dev/null
+++ b/test/regress/regress0/datatypes/empty_tuprec.cvc
@@ -0,0 +1,20 @@
+OPTION "incremental";
+
+a1, a2 : []; % empty tuples (a unit type)
+b1, b2 : [##]; % empty records (a unit type)
+c1, c2 : [[]]; % 1-tuples of the empty tuple (a unit type)
+d1, d2 : [#x:[[##]],y:[#z:[]#]#]; % more complicated records (still a unit type)
+
+% EXPECT: valid
+QUERY a1 = a2;
+
+% EXPECT: valid
+QUERY b1 = b2;
+
+% EXPECT: valid
+QUERY c1 = c2;
+
+% EXPECT: valid
+QUERY d1 = d2;
+
+% EXIT: 20