From: Morgan Deters Date: Tue, 15 May 2012 19:28:18 +0000 (+0000) Subject: Implement TypeNode::isComparableTo() and add a unit test for it. X-Git-Tag: cvc5-1.0.0~8172 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=49c07e26bae748fae3bdc2dadc742a3036e39b3f;p=cvc5.git 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 8cfb6387a..4ddb01974 100644 --- 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()); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index f59ce2dfe..7fe3bc75e 100644 --- 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 9dbb12ae3..17165ecf7 100644 --- 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 index 000000000..ddc06c5f2 --- /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 + +#include +#include +#include + +#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 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 */ +