--- /dev/null
+/********************* */
+/*! \file type_enumerator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** 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 Implementation of enumerators for strings
+ **/
+
+#include "theory/strings/type_enumerator.h"
+
+#include "theory/strings/theory_strings_utils.h"
+#include "util/regexp.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0)
+{
+ for (uint32_t i = 0; i < startLength; i++)
+ {
+ d_data.push_back(0);
+ }
+}
+WordIter::WordIter(uint32_t startLength, uint32_t endLength)
+ : d_hasEndLength(true), d_endLength(endLength)
+{
+ for (uint32_t i = 0; i < startLength; i++)
+ {
+ d_data.push_back(0);
+ }
+}
+
+WordIter::WordIter(const WordIter& witer)
+ : d_hasEndLength(witer.d_hasEndLength),
+ d_endLength(witer.d_endLength),
+ d_data(witer.d_data)
+{
+}
+
+const std::vector<unsigned>& WordIter::getData() const { return d_data; }
+
+bool WordIter::increment(uint32_t card)
+{
+ for (unsigned i = 0, dsize = d_data.size(); i < dsize; ++i)
+ {
+ if (d_data[i] + 1 < card)
+ {
+ ++d_data[i];
+ return true;
+ }
+ else
+ {
+ d_data[i] = 0;
+ }
+ }
+ if (d_hasEndLength && d_data.size() == d_endLength)
+ {
+ return false;
+ }
+ // otherwise increase length
+ d_data.push_back(0);
+ return true;
+}
+
+SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength)
+ : d_type(tn), d_witer(new WordIter(startLength))
+{
+}
+SEnumLen::SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength)
+ : d_type(tn), d_witer(new WordIter(startLength, endLength))
+{
+}
+
+SEnumLen::SEnumLen(const SEnumLen& e)
+ : d_type(e.d_type), d_witer(new WordIter(*e.d_witer)), d_curr(e.d_curr)
+{
+}
+
+Node SEnumLen::getCurrent() const { return d_curr; }
+
+bool SEnumLen::isFinished() const { return d_curr.isNull(); }
+
+StringEnumLen::StringEnumLen(uint32_t startLength,
+ uint32_t endLength,
+ uint32_t card)
+ : SEnumLen(NodeManager::currentNM()->stringType(), startLength, endLength),
+ d_cardinality(card)
+{
+ mkCurr();
+}
+
+StringEnumLen::StringEnumLen(uint32_t startLength, uint32_t card)
+ : SEnumLen(NodeManager::currentNM()->stringType(), startLength),
+ d_cardinality(card)
+{
+ mkCurr();
+}
+
+bool StringEnumLen::increment()
+{
+ // always use the same cardinality
+ if (!d_witer->increment(d_cardinality))
+ {
+ d_curr = Node::null();
+ return false;
+ }
+ mkCurr();
+ return true;
+}
+
+void StringEnumLen::mkCurr()
+{
+ d_curr = NodeManager::currentNM()->mkConst(String(d_witer->getData()));
+}
+
+StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
+ : TypeEnumeratorBase<StringEnumerator>(type),
+ d_wenum(0, utils::getAlphabetCardinality())
+{
+ Assert(type.getKind() == kind::TYPE_CONSTANT
+ && type.getConst<TypeConstant>() == STRING_TYPE);
+}
+
+StringEnumerator::StringEnumerator(const StringEnumerator& enumerator)
+ : TypeEnumeratorBase<StringEnumerator>(enumerator.getType()),
+ d_wenum(enumerator.d_wenum)
+{
+}
+
+Node StringEnumerator::operator*() { return d_wenum.getCurrent(); }
+
+StringEnumerator& StringEnumerator::operator++()
+{
+ d_wenum.increment();
+ return *this;
+}
+
+bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }
+
+} // namespace strings
+} // namespace theory
+} // namespace CVC4
** directory for licensing information.\endverbatim
**
** \brief Enumerators for strings
- **
- ** Enumerators for strings.
**/
#include "cvc4_private.h"
#ifndef CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
#define CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H
-#include <sstream>
+#include <vector>
-#include "expr/kind.h"
+#include "expr/node.h"
#include "expr/type_node.h"
-#include "theory/strings/theory_strings_rewriter.h"
-#include "theory/strings/theory_strings_utils.h"
#include "theory/type_enumerator.h"
-#include "util/regexp.h"
namespace CVC4 {
namespace theory {
namespace strings {
-class StringEnumerator : public TypeEnumeratorBase<StringEnumerator> {
- std::vector< unsigned > d_data;
- uint32_t d_cardinality;
- Node d_curr;
- void mkCurr() {
- //make constant from d_data
- d_curr = NodeManager::currentNM()->mkConst( ::CVC4::String( d_data ) );
- }
-
+/**
+ * Generic iteration over vectors of indices of a given start/end length.
+ */
+class WordIter
+{
public:
- StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
- : TypeEnumeratorBase<StringEnumerator>(type)
- {
- Assert(type.getKind() == kind::TYPE_CONSTANT
- && type.getConst<TypeConstant>() == STRING_TYPE);
- d_cardinality = utils::getAlphabetCardinality();
- mkCurr();
- }
- Node operator*() override { return d_curr; }
- StringEnumerator& operator++() override
- {
- bool changed = false;
- do
- {
- for (unsigned i = 0; i < d_data.size(); ++i)
- {
- if (d_data[i] + 1 < d_cardinality)
- {
- ++d_data[i];
- changed = true;
- break;
- }
- else
- {
- d_data[i] = 0;
- }
- }
+ /**
+ * This iterator will start with words at length startLength and continue
+ * indefinitely.
+ */
+ WordIter(uint32_t startLength);
+ /**
+ * This iterator will start with words at length startLength and continue
+ * until length endLength.
+ */
+ WordIter(uint32_t startLength, uint32_t endLength);
+ /** copy constructor */
+ WordIter(const WordIter& witer);
+ /** Get the current data */
+ const std::vector<unsigned>& getData() const;
+ /**
+ * Increment assuming the cardinality of the alphabet is card. Notice that
+ * the value of card may be different for multiple calls; the caller is
+ * responsible for using this function to achieve the required result. This
+ * is required for enumerating sequences where the cardinality of the
+ * alphabet is not known upfront, but a lower bound can be determined.
+ *
+ * This method returns true if the increment was successful, otherwise we
+ * are finished with this iterator.
+ */
+ bool increment(uint32_t card);
- if (!changed)
- {
- d_data.push_back(0);
- }
- } while (!changed);
-
- mkCurr();
- return *this;
- }
+ private:
+ /** Whether we have an end length */
+ bool d_hasEndLength;
+ /** The end length */
+ uint32_t d_endLength;
+ /** The data. */
+ std::vector<unsigned> d_data;
+};
- bool isFinished() override { return d_curr.isNull(); }
-};/* class StringEnumerator */
+/**
+ * A virtual class for enumerating string-like terms, with a similar
+ * interface to the one above.
+ */
+class SEnumLen
+{
+ public:
+ SEnumLen(TypeNode tn, uint32_t startLength);
+ SEnumLen(TypeNode tn, uint32_t startLength, uint32_t endLength);
+ SEnumLen(const SEnumLen& e);
+ virtual ~SEnumLen() {}
+ /** Get current term */
+ Node getCurrent() const;
+ /** Is this enumerator finished? */
+ bool isFinished() const;
+ /** increment, returns true if the increment was successful. */
+ virtual bool increment() = 0;
+
+ protected:
+ /** The type we are enumerating */
+ TypeNode d_type;
+ /** The word iterator utility */
+ std::unique_ptr<WordIter> d_witer;
+ /** The current term */
+ Node d_curr;
+};
/**
* Enumerates string values for a given length.
*/
-class StringEnumeratorLength {
+class StringEnumLen : public SEnumLen
+{
public:
- StringEnumeratorLength(TypeNode tn, uint32_t length, uint32_t card = 256)
- : d_type(tn), d_cardinality(card)
- {
- // TODO (cvc4-projects #23): sequence here
- Assert(tn.isString());
- for( unsigned i=0; i<length; i++ ){
- d_data.push_back( 0 );
- }
- mkCurr();
- }
-
- Node operator*() { return d_curr; }
- StringEnumeratorLength& operator++() {
- bool changed = false;
- for(unsigned i=0; i<d_data.size(); ++i) {
- if( d_data[i] + 1 < d_cardinality ) {
- ++d_data[i]; changed = true;
- break;
- } else {
- d_data[i] = 0;
- }
- }
-
- if(!changed) {
- d_curr = Node::null();
- }else{
- mkCurr();
- }
- return *this;
- }
-
- bool isFinished() { return d_curr.isNull(); }
+ /** For strings */
+ StringEnumLen(uint32_t startLength, uint32_t card);
+ StringEnumLen(uint32_t startLength, uint32_t endLength, uint32_t card);
+ /** destructor */
+ ~StringEnumLen() {}
+ /** increment */
+ bool increment() override;
private:
- /** The type we are enumerating */
- TypeNode d_type;
/** The cardinality of the alphabet */
uint32_t d_cardinality;
- /** The data (index to members) */
- std::vector<unsigned> d_data;
- /** The current term */
- Node d_curr;
/** Make the current term from d_data */
- void mkCurr()
- {
- d_curr = NodeManager::currentNM()->mkConst(::CVC4::String(d_data));
- }
+ void mkCurr();
};
+class StringEnumerator : public TypeEnumeratorBase<StringEnumerator>
+{
+ public:
+ StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
+ StringEnumerator(const StringEnumerator& enumerator);
+ ~StringEnumerator() {}
+ /** get the current term */
+ Node operator*() override;
+ /** increment */
+ StringEnumerator& operator++() override;
+ /** is this enumerator finished? */
+ bool isFinished() override;
+
+ private:
+ /** underlying string enumerator */
+ StringEnumLen d_wenum;
+}; /* class StringEnumerator */
+
}/* CVC4::theory::strings namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff