isConst() rule for datatypes

3 files changed, 26 insertions, 3 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index cada443a1..b5186f2ed 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1271,19 +1271,25 @@ template <bool ref_count>
 inline bool
 NodeTemplate<ref_count>::isConst() const {
   assertTNodeNotExpired();
+  Debug("isConst") << "Node::isConst() for " << getKind() << " with " << getNumChildren() << " children" << std::endl;
   if(isNull()) {
     return false;
   }
   switch(getMetaKind()) {
   case kind::metakind::CONSTANT:
+    Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
     return true;
   case kind::metakind::VARIABLE:
+    Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
     return false;
   default:
     if(getAttribute(IsConstComputedAttr())) {
-      return getAttribute(IsConstAttr());
+      bool bval = getAttribute(IsConstAttr());
+      Debug("isConst") << "Node::isConst() returning cached value " << bval << std::endl;
+      return bval;
     } else {
       bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
+      Debug("isConst") << "Node::isConst() computed value " << bval << std::endl;
       const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
       const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
       return bval;
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 {