From 18fe192c29a9a2c37d1925730af01e906b9888c5 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 3 Mar 2020 12:17:06 -0600 Subject: Refactoring and cleaning the type enumerator for sets (#3908) * Miscellaneous changes * Removed unnecessary vector of enumerators * cleanup * cleanup * cleanup * refactoring * cleanup * refactoring * used binary numbers for sets * isFinished for enumerator * format * added theory_sets_type_enumerator_white.h * format * Used BitVector class * Tracing * Documentation * moved implementation to theory_sets_type_enumerator.cpp * minor changes --- test/unit/theory/CMakeLists.txt | 1 + .../theory/theory_sets_type_enumerator_white.h | 304 +++++++++++++++++++++ 2 files changed, 305 insertions(+) create mode 100644 test/unit/theory/theory_sets_type_enumerator_white.h (limited to 'test/unit/theory') diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index f20088ad1..35f2f7bfa 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -8,6 +8,7 @@ cvc4_add_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) +cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) cvc4_add_unit_test_white(theory_strings_rewriter_white theory) cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) cvc4_add_unit_test_white(theory_strings_word_white theory) diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h new file mode 100644 index 000000000..3b5016fad --- /dev/null +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -0,0 +1,304 @@ +/********************* */ +/*! \file theory_sets_type_enumerator_white.h + ** \verbatim + ** Top contributors (to current version): + ** Mudathir Mahgoub + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief White box testing of CVC4::theory::sets::SetEnumerator + ** + ** White box testing of CVC4::theory::sets::SetEnumerator. (These tests + ** depends on the ordering that the SetEnumerator use, so it's a white-box + * test.) + **/ + +#include + +#include "theory/sets/theory_sets_type_enumerator.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::kind; +using namespace CVC4::theory::sets; +using namespace std; + +class SetEnumeratorWhite : public CxxTest::TestSuite +{ + ExprManager* d_em; + NodeManager* d_nm; + NodeManagerScope* d_scope; + + public: + void setUp() override + { + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown() override + { + delete d_scope; + delete d_em; + } + + void testSetOfBooleans() + { + TypeNode boolType = d_nm->booleanType(); + SetEnumerator setEnumerator(d_nm->mkSetType(boolType)); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual0 = *setEnumerator; + Node expected0 = + d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType).toType())); + TS_ASSERT_EQUALS(expected0, actual0); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual1 = *++setEnumerator; + Node expected1 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(false)); + TS_ASSERT_EQUALS(expected1, actual1); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual2 = *++setEnumerator; + Node expected2 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(true)); + TS_ASSERT_EQUALS(expected2, actual2); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual3 = *++setEnumerator; + Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2); + TS_ASSERT_EQUALS(expected3, actual3); + TS_ASSERT(!setEnumerator.isFinished()); + + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + } + + void testSetOfUF() + { + TypeNode typeNode = d_nm->mkSort("Atom"); + Type sort = typeNode.toType(); + SetEnumerator setEnumerator(d_nm->mkSetType(typeNode)); + + Node actual0 = *setEnumerator; + Node expected0 = + d_nm->mkConst(EmptySet(d_nm->mkSetType(typeNode).toType())); + TS_ASSERT_EQUALS(expected0, actual0); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual1 = *++setEnumerator; + Node expected1 = d_nm->mkNode( + Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 0))); + TS_ASSERT_EQUALS(expected1, actual1); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual2 = *++setEnumerator; + Node expected2 = d_nm->mkNode( + Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 1))); + TS_ASSERT_EQUALS(expected2, actual2); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual3 = *++setEnumerator; + Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2); + TS_ASSERT_EQUALS(expected3, actual3); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual4 = *++setEnumerator; + Node expected4 = d_nm->mkNode( + Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 2))); + TS_ASSERT_EQUALS(expected4, actual4); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual5 = *++setEnumerator; + Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4); + TS_ASSERT_EQUALS(expected5, actual5); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual6 = *++setEnumerator; + Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4); + TS_ASSERT_EQUALS(expected6, actual6); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual7 = *++setEnumerator; + Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4); + TS_ASSERT_EQUALS(expected7, actual7); + TS_ASSERT(!setEnumerator.isFinished()); + } + + void testSetOfFiniteDatatype() + { + Datatype dt(d_em, "Colors"); + dt.addConstructor(DatatypeConstructor("red")); + dt.addConstructor(DatatypeConstructor("green")); + dt.addConstructor(DatatypeConstructor("blue")); + TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt)); + SetEnumerator setEnumerator(d_nm->mkSetType(datatype)); + + Node red = d_nm->mkNode( + APPLY_CONSTRUCTOR, + DatatypeType(datatype.toType()).getDatatype().getConstructor("red")); + + Node green = d_nm->mkNode( + APPLY_CONSTRUCTOR, + DatatypeType(datatype.toType()).getDatatype().getConstructor("green")); + + Node blue = d_nm->mkNode( + APPLY_CONSTRUCTOR, + DatatypeType(datatype.toType()).getDatatype().getConstructor("blue")); + + Node actual0 = *setEnumerator; + Node expected0 = + d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype).toType())); + TS_ASSERT_EQUALS(expected0, actual0); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual1 = *++setEnumerator; + Node expected1 = d_nm->mkNode(Kind::SINGLETON, red); + TS_ASSERT_EQUALS(expected1, actual1); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual2 = *++setEnumerator; + Node expected2 = d_nm->mkNode(Kind::SINGLETON, green); + TS_ASSERT_EQUALS(expected2, actual2); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual3 = *++setEnumerator; + Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2); + TS_ASSERT_EQUALS(expected3, actual3); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual4 = *++setEnumerator; + Node expected4 = d_nm->mkNode(Kind::SINGLETON, blue); + TS_ASSERT_EQUALS(expected4, actual4); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual5 = *++setEnumerator; + Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4); + TS_ASSERT_EQUALS(expected5, actual5); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual6 = *++setEnumerator; + Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4); + TS_ASSERT_EQUALS(expected6, actual6); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual7 = *++setEnumerator; + Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4); + TS_ASSERT_EQUALS(expected7, actual7); + TS_ASSERT(!setEnumerator.isFinished()); + + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + } + + void testBV() + { + TypeNode bitVector2 = d_nm->mkBitVectorType(2); + SetEnumerator setEnumerator(d_nm->mkSetType(bitVector2)); + Node zero = d_nm->mkConst(BitVector(2u, 0u)); + Node one = d_nm->mkConst(BitVector(2u, 1u)); + Node two = d_nm->mkConst(BitVector(2u, 2u)); + Node three = d_nm->mkConst(BitVector(2u, 3u)); + Node four = d_nm->mkConst(BitVector(2u, 4u)); + + Node actual0 = *setEnumerator; + Node expected0 = + d_nm->mkConst(EmptySet(d_nm->mkSetType(bitVector2).toType())); + TS_ASSERT_EQUALS(expected0, actual0); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual1 = *++setEnumerator; + Node expected1 = d_nm->mkNode(Kind::SINGLETON, zero); + TS_ASSERT_EQUALS(expected1, actual1); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual2 = *++setEnumerator; + Node expected2 = d_nm->mkNode(Kind::SINGLETON, one); + TS_ASSERT_EQUALS(expected2, actual2); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual3 = *++setEnumerator; + Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2); + TS_ASSERT_EQUALS(expected3, actual3); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual4 = *++setEnumerator; + Node expected4 = d_nm->mkNode(Kind::SINGLETON, two); + TS_ASSERT_EQUALS(expected4, actual4); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual5 = *++setEnumerator; + Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4); + TS_ASSERT_EQUALS(expected5, actual5); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual6 = *++setEnumerator; + Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4); + TS_ASSERT_EQUALS(expected6, actual6); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual7 = *++setEnumerator; + Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4); + TS_ASSERT_EQUALS(expected7, actual7); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual8 = *++setEnumerator; + Node expected8 = d_nm->mkNode(Kind::SINGLETON, three); + TS_ASSERT_EQUALS(expected8, actual8); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual9 = *++setEnumerator; + Node expected9 = d_nm->mkNode(Kind::UNION, expected1, expected8); + TS_ASSERT_EQUALS(expected9, actual9); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual10 = *++setEnumerator; + Node expected10 = d_nm->mkNode(Kind::UNION, expected2, expected8); + TS_ASSERT_EQUALS(expected10, actual10); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual11 = *++setEnumerator; + Node expected11 = d_nm->mkNode(Kind::UNION, expected3, expected8); + TS_ASSERT_EQUALS(expected11, actual11); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual12 = *++setEnumerator; + Node expected12 = d_nm->mkNode(Kind::UNION, expected4, expected8); + TS_ASSERT_EQUALS(expected12, actual12); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual13 = *++setEnumerator; + Node expected13 = d_nm->mkNode(Kind::UNION, expected5, expected8); + TS_ASSERT_EQUALS(expected13, actual13); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual14 = *++setEnumerator; + Node expected14 = d_nm->mkNode(Kind::UNION, expected6, expected8); + TS_ASSERT_EQUALS(expected14, actual14); + TS_ASSERT(!setEnumerator.isFinished()); + + Node actual15 = *++setEnumerator; + Node expected15 = d_nm->mkNode(Kind::UNION, expected7, expected8); + TS_ASSERT_EQUALS(expected15, actual15); + TS_ASSERT(!setEnumerator.isFinished()); + + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&); + TS_ASSERT(setEnumerator.isFinished()); + } + +}; /* class SetEnumeratorWhite */ -- cgit v1.2.3