Implement TypeNode::isComparableTo() and add a unit test for it.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 8cfb6387a15a6db2576296efd2f672bcf666def3..4ddb01974591232c49b2c60ecacd796c6da4980c 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -102,6 +102,19 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
   return false;
 }
 
+bool TypeNode::isComparableTo(TypeNode t) const {
+  if(*this == t) {
+    return true;
+  }
+  if(isSubtypeOf(NodeManager::currentNM()->realType())) {
+    return t.isSubtypeOf(NodeManager::currentNM()->realType());
+  }
+  if(isPredicateSubtype()) {
+    return t.isComparableTo(getSubtypeBaseType());
+  }
+  return false;
+}
+
 Node TypeNode::getSubtypePredicate() const {
   Assert(isPredicateSubtype());
   return Node::fromExpr(getConst<Predicate>());

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index f59ce2dfe140a158297abab8cb622cae298e5051..7fe3bc75ece5f677f33f6f22e663e0d7db6fa9ce 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -450,6 +450,12 @@ public:
   /** Is this type a subtype of the given type? */
   bool isSubtypeOf(TypeNode t) const;
 
+  /**
+   * Is this type comparable to the given type (i.e., do they share
+   * a common ancestor in the subtype tree)?
+   */
+  bool isComparableTo(TypeNode t) const;
+
   /** Is this the Boolean type? */
   bool isBoolean() const;
 

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 9dbb12ae35cac71766c1f0a52b357fda65c2a9ed..17165ecf732b971c22f93aa549fe75af948d08bd 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -20,6 +20,7 @@ UNIT_TESTS = \
        expr/declaration_scope_black \
        expr/node_self_iterator_black \
        expr/type_cardinality_public \
+       expr/type_node_white \
        parser/parser_black \
        parser/parser_builder_black \
        prop/cnf_stream_black \

diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
new file mode 100644 (file)
index 0000000..ddc06c5
--- /dev/null
+++ b/test/unit/expr/type_node_white.h
@@ -0,0 +1,133 @@
+/*********************                                                        */
+/*! \file type_node_white.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief White box testing of TypeNode
+ **
+ ** White box testing of TypeNode.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <string>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+#include "util/subrange_bound.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace std;
+
+class TypeNodeWhite : public CxxTest::TestSuite {
+  ExprManager* d_em;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+  SmtEngine* d_smt;
+
+public:
+
+  void setUp() {
+    d_em = new ExprManager();
+    d_nm = d_em->getNodeManager();
+    d_smt = new SmtEngine(d_em);
+    d_scope = new NodeManagerScope(d_nm);
+  }
+
+  void tearDown() {
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  void testIsComparableTo() {
+    TypeNode realType = d_nm->realType();
+    TypeNode integerType = d_nm->realType();
+    TypeNode booleanType = d_nm->booleanType();
+    TypeNode arrayType = d_nm->mkArrayType(realType, integerType);
+    TypeNode bvType = d_nm->mkBitVectorType(32);
+    TypeNode subrangeType = d_nm->mkSubrangeType(SubrangeBounds(Integer(1), Integer(10)));
+
+    Node x = d_nm->mkVar("x", realType);
+    Node xPos = d_nm->mkNode(GT, x, d_nm->mkConst(Rational(0)));
+    TypeNode funtype = d_nm->mkFunctionType(integerType, booleanType);
+    Node lambda = d_nm->mkVar("lambda", funtype);
+    vector<Expr> formals;
+    formals.push_back(x.toExpr());
+    d_smt->defineFunction(lambda.toExpr(), formals, xPos.toExpr());
+    TypeNode predicateSubtype = d_nm->mkPredicateSubtype(lambda.toExpr());
+
+    TS_ASSERT( not realType.isComparableTo(booleanType) );
+    TS_ASSERT( realType.isComparableTo(integerType) );
+    TS_ASSERT( realType.isComparableTo(realType) );
+    TS_ASSERT( not realType.isComparableTo(arrayType) );
+    TS_ASSERT( not realType.isComparableTo(bvType) );
+    TS_ASSERT( realType.isComparableTo(subrangeType) );
+    TS_ASSERT( realType.isComparableTo(predicateSubtype) );
+
+    TS_ASSERT( not booleanType.isComparableTo(integerType) );
+    TS_ASSERT( not booleanType.isComparableTo(realType) );
+    TS_ASSERT( booleanType.isComparableTo(booleanType) );
+    TS_ASSERT( not booleanType.isComparableTo(arrayType) );
+    TS_ASSERT( not booleanType.isComparableTo(bvType) );
+    TS_ASSERT( not booleanType.isComparableTo(subrangeType) );
+    TS_ASSERT( not booleanType.isComparableTo(predicateSubtype) );
+
+    TS_ASSERT( integerType.isComparableTo(realType) );
+    TS_ASSERT( integerType.isComparableTo(integerType) );
+    TS_ASSERT( not integerType.isComparableTo(booleanType) );
+    TS_ASSERT( not integerType.isComparableTo(arrayType) );
+    TS_ASSERT( not integerType.isComparableTo(bvType) );
+    TS_ASSERT( integerType.isComparableTo(subrangeType) );
+    TS_ASSERT( integerType.isComparableTo(predicateSubtype) );
+
+    TS_ASSERT( not arrayType.isComparableTo(booleanType) );
+    TS_ASSERT( not arrayType.isComparableTo(integerType) );
+    TS_ASSERT( not arrayType.isComparableTo(realType) );
+    TS_ASSERT( arrayType.isComparableTo(arrayType) );
+    TS_ASSERT( not arrayType.isComparableTo(bvType) );
+    TS_ASSERT( not arrayType.isComparableTo(subrangeType) );
+    TS_ASSERT( not arrayType.isComparableTo(predicateSubtype) );
+
+    TS_ASSERT( not bvType.isComparableTo(booleanType) );
+    TS_ASSERT( not bvType.isComparableTo(integerType) );
+    TS_ASSERT( not bvType.isComparableTo(realType) );
+    TS_ASSERT( not bvType.isComparableTo(arrayType) );
+    TS_ASSERT( bvType.isComparableTo(bvType) );
+    TS_ASSERT( not bvType.isComparableTo(subrangeType) );
+    TS_ASSERT( not bvType.isComparableTo(predicateSubtype) );
+
+    TS_ASSERT( not subrangeType.isComparableTo(booleanType) );
+    TS_ASSERT( subrangeType.isComparableTo(integerType) );
+    TS_ASSERT( subrangeType.isComparableTo(realType) );
+    TS_ASSERT( not subrangeType.isComparableTo(arrayType) );
+    TS_ASSERT( not subrangeType.isComparableTo(bvType) );
+    TS_ASSERT( subrangeType.isComparableTo(subrangeType) );
+    TS_ASSERT( subrangeType.isComparableTo(predicateSubtype) );
+
+    TS_ASSERT( not predicateSubtype.isComparableTo(booleanType) );
+    TS_ASSERT( predicateSubtype.isComparableTo(integerType) );
+    TS_ASSERT( predicateSubtype.isComparableTo(realType) );
+    TS_ASSERT( not predicateSubtype.isComparableTo(arrayType) );
+    TS_ASSERT( not predicateSubtype.isComparableTo(bvType) );
+    TS_ASSERT( predicateSubtype.isComparableTo(subrangeType) );
+    TS_ASSERT( predicateSubtype.isComparableTo(predicateSubtype) );
+  }
+
+};/* TypeNodeWhite */
+