diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/expr/type_node_white.h | 133 |
2 files changed, 134 insertions, 0 deletions
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 <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 */ + |