summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-05-15 19:28:18 +0000
committerMorgan Deters <mdeters@gmail.com>2012-05-15 19:28:18 +0000
commit49c07e26bae748fae3bdc2dadc742a3036e39b3f (patch)
tree18a5e399127aba003d231ba7dc9059e26d0a736d /test
parent26a6e8585d75cf6128016064e8cd2d19e7ee9a49 (diff)
Implement TypeNode::isComparableTo() and add a unit test for it.
Diffstat (limited to 'test')
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/expr/type_node_white.h133
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 */
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback