diff options
Diffstat (limited to 'src/theory')
-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 |
3 files changed, 186 insertions, 162 deletions
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 */ |