diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-04 18:45:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-04 18:45:13 +0000 |
commit | 1467abb8bd69050c2518f87a1775590cd5a9882e (patch) | |
tree | 30c269deec8189fde2b8db2abd4bee9600ad8a2f /src/theory | |
parent | c956906a5dc4cb51b4676c3bba80159cbe76fdbc (diff) |
isConst() rule for datatypes
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/kinds | 3 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 18 |
2 files changed, 19 insertions, 2 deletions
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index b83450723..e66cc3454 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -81,4 +81,7 @@ typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule +# constructor applications are constant if they are applied only to constants +construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index d8d40154a..1b61ef470 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -38,7 +38,7 @@ typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node> struct DatatypeConstructorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { + throw(TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); TypeNode consType = n.getOperator().getType(check); Type t = consType.getConstructorRangeType().toType(); @@ -73,13 +73,27 @@ struct DatatypeConstructorTypeRule { Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; TypeNode argumentType = *tchild_it; if(!childType.isSubtypeOf(argumentType)) { - throw TypeCheckingExceptionPrivate(n, "bad type for constructor argument"); + std::stringstream ss; + ss << "bad type for constructor argument:\nexpected: " << argumentType << "\ngot : " << childType; + throw TypeCheckingExceptionPrivate(n, ss.str()); } } } return consType.getConstructorRangeType(); } } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) + throw(AssertionException) { + Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); + NodeManagerScope nms(nodeManager); + for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) { + if( ! (*i).isConst() ) { + return false; + } + } + return true; + } };/* struct DatatypeConstructorTypeRule */ struct DatatypeSelectorTypeRule { |