From 74a31b92b0d7bd83777fa1650b5c21ed968fb887 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Mar 2020 09:25:24 -0500 Subject: [PATCH] Refactor enumerator for strings (#4014) Towards theory of sequences. This separates out a virtual base class and utility class for the strings enumerator, which will be extended for sequences later. --- src/CMakeLists.txt | 1 + src/theory/strings/theory_strings.cpp | 22 ++- src/theory/strings/type_enumerator.cpp | 149 +++++++++++++++++++ src/theory/strings/type_enumerator.h | 191 ++++++++++++------------- 4 files changed, 260 insertions(+), 103 deletions(-) create mode 100644 src/theory/strings/type_enumerator.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index dfdfb0a47..7e31d1494 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -694,6 +694,7 @@ libcvc4_add_sources( theory/strings/theory_strings_type_rules.h theory/strings/theory_strings_utils.cpp theory/strings/theory_strings_utils.h + theory/strings/type_enumerator.cpp theory/strings/type_enumerator.h theory/strings/word.cpp theory/strings/word.h diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 5015db3f1..c0dc561f6 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -413,9 +413,18 @@ bool TheoryStrings::collectModelInfoType( //use type enumerator Assert(lts_values[i].getConst() <= Rational(String::maxSize())) << "Exceeded UINT32_MAX in string model"; - StringEnumeratorLength sel( - tn, - lts_values[i].getConst().getNumerator().toUnsignedInt()); + uint32_t currLen = + lts_values[i].getConst().getNumerator().toUnsignedInt(); + std::unique_ptr sel; + if (tn.isString()) + { + sel.reset(new StringEnumLen( + currLen, currLen, utils::getAlphabetCardinality())); + } + else + { + Unimplemented() << "Collect model info not implemented for type " << tn; + } for (const Node& eqc : pure_eq) { Node c; @@ -424,7 +433,7 @@ bool TheoryStrings::collectModelInfoType( { do { - if (sel.isFinished()) + if (sel->isFinished()) { // We are in a case where model construction is impossible due to // an insufficient number of constants of a given length. @@ -460,8 +469,9 @@ bool TheoryStrings::collectModelInfoType( } return false; } - c = *sel; - ++sel; + c = sel->getCurrent(); + // increment + sel->increment(); } while (m->hasTerm(c)); } else diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp new file mode 100644 index 000000000..12cf899b4 --- /dev/null +++ b/src/theory/strings/type_enumerator.cpp @@ -0,0 +1,149 @@ +/********************* */ +/*! \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& 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(type), + d_wenum(0, utils::getAlphabetCardinality()) +{ + Assert(type.getKind() == kind::TYPE_CONSTANT + && type.getConst() == STRING_TYPE); +} + +StringEnumerator::StringEnumerator(const StringEnumerator& enumerator) + : TypeEnumeratorBase(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 diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index 16bfc75a6..2061628a5 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -10,8 +10,6 @@ ** directory for licensing information.\endverbatim ** ** \brief Enumerators for strings - ** - ** Enumerators for strings. **/ #include "cvc4_private.h" @@ -19,124 +17,123 @@ #ifndef CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H #define CVC4__THEORY__STRINGS__TYPE_ENUMERATOR_H -#include +#include -#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 { - 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(type) - { - Assert(type.getKind() == kind::TYPE_CONSTANT - && type.getConst() == 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& 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 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 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 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 +{ + 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 */ -- 2.30.2