isConst() rule for datatypes

diff --git a/src/expr/node.h b/src/expr/node.h
index cada443a1d6cc062f63504c175fa5db55246cf92..b5186f2ed1c1288ccf02a256b9c096a9529b1c33 100644 (file)
--- 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 b83450723cad3369d7985bb817d862b6d428154e..e66cc3454c9520e9331e39d8cd34b458d0b29765 100644 (file)
--- 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 d8d40154ae7249a6e6d6069cfc4df9711b6a1f50..1b61ef470b7efa177c42bb5bfd53babbae40008b 100644 (file)
--- 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 {

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 491f995840b332e3546f8e5881419e7577dbc911..d4a968e9667fc08be841df5f5a7172b20f95ce94 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -345,6 +345,8 @@ public:
   void testIsConst() {
     /* bool isConst() const; */
 
+    Debug.on("isConst");
+
     TS_ASSERT(!a_bool->isConst());
     TS_ASSERT(!b_bool->isConst());
     TS_ASSERT(!c_bool_and->isConst());
@@ -352,6 +354,25 @@ public:
     TS_ASSERT(plus_op->isConst());
     TS_ASSERT(!d_apply_fun_bool->isConst());
     TS_ASSERT(!null->isConst());
+
+    // more complicated "constants" exist in datatypes and arrays theories
+    Datatype list("list");
+    DatatypeConstructor consC("cons");
+    consC.addArg("car", d_em->integerType());
+    consC.addArg("cdr", DatatypeSelfType());
+    list.addConstructor(consC);
+    list.addConstructor(DatatypeConstructor("nil"));
+    DatatypeType listType = d_em->mkDatatypeType(list);
+    Expr cons = listType.getDatatype().getConstructor("cons");
+    Expr nil = listType.getDatatype().getConstructor("nil");
+    Expr x = d_em->mkVar("x", d_em->integerType());
+    Expr cons_x_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, x, d_em->mkExpr(APPLY_CONSTRUCTOR, nil));
+    Expr cons_1_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(1)), d_em->mkExpr(APPLY_CONSTRUCTOR, nil));
+    Expr cons_1_cons_2_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(1)), d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(2)), d_em->mkExpr(APPLY_CONSTRUCTOR, nil)));
+    TS_ASSERT(d_em->mkExpr(APPLY_CONSTRUCTOR, nil).isConst());
+    TS_ASSERT(!cons_x_nil.isConst());
+    TS_ASSERT(cons_1_nil.isConst());
+    TS_ASSERT(cons_1_cons_2_nil.isConst());
   }
 
   void testGetConst() {