From 1467abb8bd69050c2518f87a1775590cd5a9882e Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 4 Aug 2012 18:45:13 +0000
Subject: [PATCH] isConst() rule for datatypes

---
 src/expr/node.h                               |  8 ++++++-
 src/theory/datatypes/kinds                    |  3 +++
 .../datatypes/theory_datatypes_type_rules.h   | 18 ++++++++++++++--
 test/unit/expr/expr_public.h                  | 21 +++++++++++++++++++
 4 files changed, 47 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 {
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 491f99584..d4a968e96 100644
--- 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() {
-- 
2.30.2