diff options
| -rw-r--r-- | src/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | src/theory/sets/normal_form.h | 13 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.cpp | 132 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 203 | ||||
| -rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/unit/theory/theory_sets_type_enumerator_white.h | 304 |
6 files changed, 492 insertions, 162 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 201b6a21d..aaa789308 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -661,6 +661,7 @@ libcvc4_add_sources( theory/sets/theory_sets_rels.h theory/sets/theory_sets_rewriter.cpp theory/sets/theory_sets_rewriter.h + theory/sets/theory_sets_type_enumerator.cpp theory/sets/theory_sets_type_enumerator.h theory/sets/theory_sets_type_rules.h theory/shared_terms_database.cpp diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index 5c7218332..c36692f00 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -27,16 +27,21 @@ class NormalForm { public: template <bool ref_count> static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements, - TypeNode setType) { + TypeNode setType) + { typedef typename std::set<NodeTemplate<ref_count> >::const_iterator ElementsIterator; NodeManager* nm = NodeManager::currentNM(); - if (elements.size() == 0) { + if (elements.size() == 0) + { return nm->mkConst(EmptySet(nm->toType(setType))); - } else { + } + else + { ElementsIterator it = elements.begin(); Node cur = nm->mkNode(kind::SINGLETON, *it); - while (++it != elements.end()) { + while (++it != elements.end()) + { cur = nm->mkNode(kind::UNION, cur, nm->mkNode(kind::SINGLETON, *it)); } return cur; diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp new file mode 100644 index 000000000..ded5975a5 --- /dev/null +++ b/src/theory/sets/theory_sets_type_enumerator.cpp @@ -0,0 +1,132 @@ +/********************* */ +/*! \file theory_sets_type_enumerator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Kshitij Bansal, Tim King, Andrew Reynolds, Mudathir Mahgoub + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 set enumerator implementation + ** + ** set enumerator implementation + **/ + +#include "theory/sets/theory_sets_type_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +SetEnumerator::SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep) + : TypeEnumeratorBase<SetEnumerator>(type), + d_nodeManager(NodeManager::currentNM()), + d_elementEnumerator(type.getSetElementType(), tep), + d_isFinished(false), + d_currentSetIndex(0), + d_currentSet() +{ + d_currentSet = d_nodeManager->mkConst(EmptySet(type.toType())); +} + +SetEnumerator::SetEnumerator(const SetEnumerator& enumerator) + : TypeEnumeratorBase<SetEnumerator>(enumerator.getType()), + d_nodeManager(enumerator.d_nodeManager), + d_elementEnumerator(enumerator.d_elementEnumerator), + d_isFinished(enumerator.d_isFinished), + d_currentSetIndex(enumerator.d_currentSetIndex), + d_currentSet(enumerator.d_currentSet) +{ +} + +SetEnumerator::~SetEnumerator() {} + +Node SetEnumerator::operator*() +{ + if (d_isFinished) + { + throw NoMoreValuesException(getType()); + } + + Trace("set-type-enum") << "SetEnumerator::operator* d_currentSet = " + << d_currentSet << std::endl; + + return d_currentSet; +} + +SetEnumerator& SetEnumerator::operator++() +{ + if (d_isFinished) + { + Trace("set-type-enum") << "SetEnumerator::operator++ finished!" + << std::endl; + Trace("set-type-enum") << "SetEnumerator::operator++ d_currentSet = " + << d_currentSet << std::endl; + return *this; + } + + d_currentSetIndex++; + + // if the index is a power of 2, get a new element from d_elementEnumerator + if (d_currentSetIndex == static_cast<unsigned>(1 << d_elementsSoFar.size())) + { + // if there are no more values from d_elementEnumerator, set d_isFinished + // to true + if (d_elementEnumerator.isFinished()) + { + d_isFinished = true; + + Trace("set-type-enum") + << "SetEnumerator::operator++ finished!" << std::endl; + Trace("set-type-enum") + << "SetEnumerator::operator++ d_currentSet = " << d_currentSet + << std::endl; + return *this; + } + + // get a new element and return it as a singleton set + Node element = *d_elementEnumerator; + d_elementsSoFar.push_back(element); + d_currentSet = d_nodeManager->mkNode(kind::SINGLETON, element); + d_elementEnumerator++; + } + else + { + // determine which elements are included in the set + BitVector indices = BitVector(d_elementsSoFar.size(), d_currentSetIndex); + std::vector<Node> elements; + for (unsigned i = 0; i < d_elementsSoFar.size(); i++) + { + // add the element to the set if its corresponding bit is set + if (indices.isBitSet(i)) + { + elements.push_back(d_elementsSoFar[i]); + } + } + d_currentSet = NormalForm::elementsToSet( + std::set<TNode>(elements.begin(), elements.end()), getType()); + } + + Assert(d_currentSet.isConst()); + Assert(d_currentSet == Rewriter::rewrite(d_currentSet)); + + Trace("set-type-enum") << "SetEnumerator::operator++ d_elementsSoFar = " + << d_elementsSoFar << std::endl; + Trace("set-type-enum") << "SetEnumerator::operator++ d_currentSet = " + << d_currentSet << std::endl; + + return *this; +} + +bool SetEnumerator::isFinished() +{ + Trace("set-type-enum") << "SetEnumerator::isFinished = " << d_isFinished + << std::endl; + return d_isFinished; +} + +} // namespace sets +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 5a6745367..306d96b52 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -2,185 +2,72 @@ /*! \file theory_sets_type_enumerator.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Tim King, Andrew Reynolds + ** Kshitij Bansal, Tim King, Andrew Reynolds, Mudathir Mahgoub ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 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 [[ Add one-line brief description here ]] + ** \brief type enumerator for sets ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** A set enumerator that iterates over the power set of the element type + ** starting with the empty set as the initial value **/ - #include "cvc4_private.h" #ifndef CVC4__THEORY__SETS__TYPE_ENUMERATOR_H #define CVC4__THEORY__SETS__TYPE_ENUMERATOR_H -#include "theory/type_enumerator.h" -#include "expr/type_node.h" #include "expr/kind.h" +#include "expr/type_node.h" #include "theory/rewriter.h" #include "theory/sets/normal_form.h" +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { namespace sets { -class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> { - /** type properties */ - TypeEnumeratorProperties * d_tep; - unsigned d_index; - TypeNode d_constituentType; - NodeManager* d_nm; - std::vector<bool> d_indexVec; - std::vector<TypeEnumerator*> d_constituentVec; - bool d_finished; - Node d_setConst; - +class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> +{ public: - SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) - : TypeEnumeratorBase<SetEnumerator>(type), - d_tep(tep), - d_index(0), - d_constituentType(type.getSetElementType()), - d_nm(NodeManager::currentNM()), - d_indexVec(), - d_constituentVec(), - d_finished(false), - d_setConst() - { - // d_indexVec.push_back(false); - // d_constituentVec.push_back(new TypeEnumerator(d_constituentType)); - d_setConst = d_nm->mkConst(EmptySet(type.toType())); - } - - // An set enumerator could be large, and generally you don't want to - // go around copying these things; but a copy ctor is presently required - // by the TypeEnumerator framework. - SetEnumerator(const SetEnumerator& ae) - : TypeEnumeratorBase<SetEnumerator>( - ae.d_nm->mkSetType(ae.d_constituentType)), - d_tep(ae.d_tep), - d_index(ae.d_index), - d_constituentType(ae.d_constituentType), - d_nm(ae.d_nm), - d_indexVec(ae.d_indexVec), - d_constituentVec(), // copied below - d_finished(ae.d_finished), - d_setConst(ae.d_setConst) - { - for(std::vector<TypeEnumerator*>::const_iterator i = - ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end(); - i != i_end; - ++i) { - d_constituentVec.push_back(new TypeEnumerator(**i)); - } - } - - ~SetEnumerator() { - while (!d_constituentVec.empty()) { - delete d_constituentVec.back(); - d_constituentVec.pop_back(); - } - } - - Node operator*() override - { - if (d_finished) { - throw NoMoreValuesException(getType()); - } - - std::vector<Node> elements; - for(unsigned i = 0; i < d_constituentVec.size(); ++i) { - elements.push_back(*(*(d_constituentVec[i]))); - } - - Node n = NormalForm::elementsToSet(std::set<TNode>(elements.begin(), elements.end()), - getType()); - - Assert(n.isConst()); - Assert(n == Rewriter::rewrite(n)); - - return n; - } - - SetEnumerator& operator++() override - { - Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl; - - if (d_finished) { - Trace("set-type-enum") << "operator++ finished!" << std::endl; - return *this; - } - - // increment by one, at the same time deleting all elements that - // cannot be incremented any further (note: we are keeping a set - // -- no repetitions -- thus some trickery to know what to pop and - // what not to.) - if(d_index > 0) { - Assert(d_index == d_constituentVec.size()); - - Node last_pre_increment; - last_pre_increment = *(*d_constituentVec.back()); - - ++(*d_constituentVec.back()); - - if (d_constituentVec.back()->isFinished()) { - delete d_constituentVec.back(); - d_constituentVec.pop_back(); - - while(!d_constituentVec.empty()) { - Node cur_pre_increment = *(*d_constituentVec.back()); - ++(*d_constituentVec.back()); - Node cur_post_increment = *(*d_constituentVec.back()); - if(last_pre_increment == cur_post_increment) { - delete d_constituentVec.back(); - d_constituentVec.pop_back(); - last_pre_increment = cur_pre_increment; - } else { - break; - } - } - } - } - - if (d_constituentVec.empty()) { - ++d_index; - d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); - } - - while (d_constituentVec.size() < d_index) { - TypeEnumerator* newEnumerator = - new TypeEnumerator(*d_constituentVec.back()); - ++(*newEnumerator); - if (newEnumerator->isFinished()) { - Trace("set-type-enum") << "operator++ finished!" << std::endl; - delete newEnumerator; - d_finished = true; - return *this; - } - d_constituentVec.push_back(newEnumerator); - } - - Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl; - return *this; - } - - bool isFinished() override - { - Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl; - return d_finished; - } - -};/* class SetEnumerator */ - -}/* CVC4::theory::sets namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ + SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + SetEnumerator(const SetEnumerator& enumerator); + ~SetEnumerator(); + + Node operator*() override; + + /** + * This operator iterates over the power set of the element type + * following the order of a bitvector counter. + * Example: iterating over a set of bitvecotors of length 2 will return the + * following sequence consisting of 16 sets: + * {}, {00}, {01}, {00, 01}, {10}, {00, 10}, {01, 10}, {00, 01, 10}, ..., + * {00, 01, 10, 11} + */ + SetEnumerator& operator++() override; + + bool isFinished() override; + + private: + /** a pointer to the node manager */ + NodeManager* d_nodeManager; + /** an enumerator for the elements' type */ + TypeEnumerator d_elementEnumerator; + /** a boolean to indicate whether the set enumerator is finished */ + bool d_isFinished; + /** a list of the elements encountered so far */ + std::vector<Node> d_elementsSoFar; + /** stores the index of the current set in the power set */ + unsigned d_currentSetIndex; + /** the current set returned by the set enumerator */ + Node d_currentSet; +}; /* class SetEnumerator */ + +} // namespace sets +} // namespace theory +} // namespace CVC4 #endif /* CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */ 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 <cxxtest/TestSuite.h> + +#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 */ |