isConst() rule for datatypes

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 {