From 42d28850d4f2f4816af24dedf8d1cbd0a0d58b6f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 4 Sep 2013 19:55:16 -0400 Subject: [PATCH] Support empty (and 1-ary) tuples and records. --- src/expr/expr_manager_template.cpp | 1 - src/expr/node_manager.h | 1 - src/parser/cvc/Cvc.g | 22 +++++++++---------- src/theory/datatypes/kinds | 4 ++-- src/util/record.h | 1 - test/regress/regress0/datatypes/Makefile.am | 1 + .../regress0/datatypes/empty_tuprec.cvc | 20 +++++++++++++++++ 7 files changed, 34 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress0/datatypes/empty_tuprec.cvc diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 424ebab11..a838d6d30 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -509,7 +509,6 @@ FunctionType ExprManager::mkPredicateType(const std::vector& sorts) { TupleType ExprManager::mkTupleType(const std::vector& types) { NodeManagerScope nms(d_nodeManager); - Assert( types.size() >= 1 ); std::vector 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 f44c7e78b..7c84f3f15 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1090,7 +1090,6 @@ NodeManager::mkPredicateType(const std::vector& sorts) { } inline TypeNode NodeManager::mkTupleType(const std::vector& types) { - Assert(types.size() >= 1); std::vector 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 51ea87e39..cbdee9c74 100644 --- 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()); } + /* 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 2e58677df..81ef32b32 100644 --- 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 3d6481320..63c54930e 100644 --- a/src/util/record.h +++ b/src/util/record.h @@ -91,7 +91,6 @@ public: Record(const std::vector< std::pair >& 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 06227ad3a..b95261d56 100644 --- 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 index 000000000..8e163e855 --- /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 -- 2.30.2