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.

4 files changed, 260 insertions, 103 deletions

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>() <= Rational(String::maxSize()))
           << "Exceeded UINT32_MAX in string model";
-      StringEnumeratorLength sel(
-          tn,
-          lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
+      uint32_t currLen =
+          lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt();
+      std::unique_ptr<SEnumLen> 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<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
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 <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 */