diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-14 22:53:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-14 22:53:58 +0000 |
commit | 4941b3c516361183b4623f5660128e4f1bcce809 (patch) | |
tree | 5a996a0778b9a78b27b041fa582ff5585b710013 /test/unit | |
parent | 1c42109395b566a0068cc3ae9067fc87ab8f8e7b (diff) |
Type enumerator infrastructure and uninterpreted constant support. No support yet for enumerating arrays, or for enumerating non-trivial datatypes.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/theory/type_enumerator_white.h | 197 |
2 files changed, 198 insertions, 0 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 17165ecf7..bb8cdf7fe 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -6,6 +6,7 @@ UNIT_TESTS = \ theory/theory_arith_white \ theory/union_find_black \ theory/theory_bv_white \ + theory/type_enumerator_white \ expr/expr_public \ expr/expr_manager_public \ expr/node_white \ diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h new file mode 100644 index 000000000..bf76ba801 --- /dev/null +++ b/test/unit/theory/type_enumerator_white.h @@ -0,0 +1,197 @@ +/********************* */ +/*! \file type_enumerator_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 CVC4::theory::TypeEnumerator + ** + ** White box testing of CVC4::theory::TypeEnumerator. (These tests depends + ** on the ordering that the TypeEnumerators use, so it's a white-box test.) + **/ + +#include <cxxtest/TestSuite.h> + +#include "expr/node_manager.h" +#include "expr/expr_manager.h" +#include "expr/type_node.h" +#include "expr/kind.h" +#include "theory/type_enumerator.h" +#include "util/language.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::kind; + +using namespace std; + +class TypeEnumeratorWhite : public CxxTest::TestSuite { + ExprManager* d_em; + NodeManager* d_nm; + NodeManagerScope* d_scope; + +public: + + void setUp() { + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown() { + delete d_scope; + delete d_em; + } + + void testBooleans() { + TypeEnumerator te(d_nm->booleanType()); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(false)); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(true)); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + } + + void testUF() { + TypeNode sortn = d_nm->mkSort("T"); + Type sort = sortn.toType(); + TypeNode sortn2 = d_nm->mkSort("U"); + Type sort2 = sortn2.toType(); + TypeEnumerator te(sortn); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(UninterpretedConstant(sort, 0))); + for(size_t i = 1; i < 100; ++i) { + TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i))); + TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort2, i))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(UninterpretedConstant(sort, i))); + TS_ASSERT_DIFFERS(*te, d_nm->mkConst(UninterpretedConstant(sort, i + 2))); + } + } + + void testArith() { + TypeEnumerator te(d_nm->integerType()); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0))); + for(int i = 1; i <= 100; ++i) { + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(i))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-i))); + } + + te = TypeEnumerator(d_nm->realType()); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(Rational(0, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 2))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 2))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 2))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 2))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 4))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 4))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 5))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 5))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(6, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-6, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 2))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 2))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(4, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-4, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 4))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 4))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(2, 5))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-2, 5))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 6))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 6))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(7, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-7, 1))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(5, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-5, 3))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(3, 5))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-3, 5))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(1, 7))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(Rational(-1, 7))); + } + + void testDatatypesFinite() { + Datatype dt("Colors"); + dt.addConstructor(DatatypeConstructor("red")); + dt.addConstructor(DatatypeConstructor("orange")); + dt.addConstructor(DatatypeConstructor("yellow")); + dt.addConstructor(DatatypeConstructor("green")); + dt.addConstructor(DatatypeConstructor("blue")); + dt.addConstructor(DatatypeConstructor("violet")); + TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt)); + TypeEnumerator te(datatype); + TS_ASSERT_EQUALS(*te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("red"))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("orange"))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("yellow"))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("green"))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("blue"))); + TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(datatype.toType()).getDatatype().getConstructor("violet"))); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + } + + void NOtestDatatypesInfinite() { + TypeNode datatype; + TypeEnumerator te(datatype); + TS_FAIL("unimplemented"); + } + + void NOtestArraysInfinite() { + TypeEnumerator te(d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType())); + + TS_FAIL("unimplemented"); + } + + // remove this when ArrayConst is available + template <class T, class U> inline bool ArrayConst(const T&, const U&) { return false; } + + void NOtestArraysFinite() { + TypeEnumerator te(d_nm->mkArrayType(d_nm->mkBitVectorType(2), d_nm->booleanType())); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(0)), d_nm->mkConst(false)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(0)), d_nm->mkConst(true)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(1)), d_nm->mkConst(false)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(1)), d_nm->mkConst(true)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(2)), d_nm->mkConst(false)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(2)), d_nm->mkConst(true)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(3)), d_nm->mkConst(false)))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(ArrayConst(d_nm->mkConst(BitVector(3)), d_nm->mkConst(true)))); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + } + + void testBV() { + TypeEnumerator te(d_nm->mkBitVectorType(3)); + TS_ASSERT_EQUALS(*te, d_nm->mkConst(BitVector(3u, 0u))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 1u))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 2u))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 3u))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 4u))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 5u))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 6u))); + TS_ASSERT_EQUALS(*++te, d_nm->mkConst(BitVector(3u, 7u))); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + TS_ASSERT_THROWS(*++te, NoMoreValuesException); + } + +};/* class TypeEnumeratorWhite */ |