--- /dev/null
+/********************* */
+/*! \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
/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff