Add the sequence type (#4539)

This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.

The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.

8 files changed, 222 insertions, 1 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 27ffe5d26..800847ffe 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -58,12 +58,27 @@ constant CONST_STRING \
     "util/string.h" \
     "a string of characters"
 
+# the type
+operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements"
+cardinality SEQUENCE_TYPE \
+    "::CVC4::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \
+    "theory/strings/theory_strings_type_rules.h"
+well-founded SEQUENCE_TYPE \
+    "::CVC4::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \
+    "::CVC4::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \
+    "theory/strings/theory_strings_type_rules.h"
+enumerator SEQUENCE_TYPE \
+    "::CVC4::theory::strings::SequenceEnumerator" \
+    "theory/strings/type_enumerator.h"
+
 constant CONST_SEQUENCE \
     ::CVC4::ExprSequence \
     ::CVC4::ExprSequenceHashFunction \
     "expr/expr_sequence.h" \
     "a sequence of characters"
 
+operator SEQ_UNIT 1 "a sequence of length one"
+
 # equal equal / less than / output
 operator STRING_TO_REGEXP 1 "convert string to regexp"
 operator REGEXP_CONCAT 2: "regexp concat"
@@ -144,4 +159,9 @@ typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>"
 typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
 typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
 
+### sequence specific operators
+
+typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule
+typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule
+
 endtheory
diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp
index 2953a2b3c..a4055c4f9 100644
--- a/src/theory/strings/rewrites.cpp
+++ b/src/theory/strings/rewrites.cpp
@@ -200,6 +200,7 @@ const char* toString(Rewrite r)
     case Rewrite::LEN_REPL_INV: return "LEN_REPL_INV";
     case Rewrite::LEN_CONV_INV: return "LEN_CONV_INV";
     case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM";
+    case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL";
     default: return "?";
   }
 }
diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h
index 7a315ebd3..96a3b65fd 100644
--- a/src/theory/strings/rewrites.h
+++ b/src/theory/strings/rewrites.h
@@ -202,7 +202,8 @@ enum class Rewrite : uint32_t
   LEN_CONCAT,
   LEN_REPL_INV,
   LEN_CONV_INV,
-  CHARAT_ELIM
+  CHARAT_ELIM,
+  SEQ_UNIT_EVAL
 };
 
 /**
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 2d2ec0af0..55d58b860 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1461,6 +1461,10 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node)
   {
     retNode = rewriteRepeatRegExp(node);
   }
+  else if (nk == SEQ_UNIT)
+  {
+    retNode = rewriteSeqUnit(node);
+  }
 
   Trace("sequences-postrewrite")
       << "Strings::SequencesRewriter::postRewrite returning " << retNode
@@ -3095,6 +3099,19 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
   return res;
 }
 
+Node SequencesRewriter::rewriteSeqUnit(Node node)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (node[0].isConst())
+  {
+    std::vector<Expr> seq;
+    seq.push_back(node[0].toExpr());
+    TypeNode stype = nm->mkSequenceType(node[0].getType());
+    Node ret = nm->mkConst(ExprSequence(stype.toType(), seq));
+    return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL);
+  }
+  return node;
+}
 
 Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
 {
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 56b74f536..490dd8b3c 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -224,6 +224,12 @@ class SequencesRewriter : public TheoryRewriter
    * Returns the rewritten form of node.
    */
   Node rewriteStringToCode(Node node);
+  /** rewrite seq.unit
+   * This is the entry point for post-rewriting terms n of the form
+   *   seq.unit( t )
+   * Returns the rewritten form of node.
+   */
+  Node rewriteSeqUnit(Node node);
 
   /** length preserving rewrite
    *
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 93a32f26e..3229e6631 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -20,6 +20,9 @@
 #ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 #define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 
+#include "expr/expr_sequence.h"
+#include "expr/sequence.h"
+
 namespace CVC4 {
 namespace theory {
 namespace strings {
@@ -318,6 +321,53 @@ public:
   }
 };
 
+class ConstSequenceTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::CONST_SEQUENCE);
+    return n.getConst<ExprSequence>().getSequence().getType();
+  }
+};
+
+class SeqUnitTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    return nodeManager->mkSequenceType(n[0].getType(check));
+  }
+};
+
+/** Properties of the sequence type */
+struct SequenceProperties
+{
+  static Cardinality computeCardinality(TypeNode type)
+  {
+    Assert(type.getKind() == kind::SEQUENCE_TYPE);
+    return Cardinality::INTEGERS;
+  }
+  /** A sequence is well-founded if its element type is */
+  static bool isWellFounded(TypeNode type)
+  {
+    return type[0].isWellFounded();
+  }
+  /** Make ground term for sequence type (return the empty sequence) */
+  static Node mkGroundTerm(TypeNode type)
+  {
+    Assert(type.isSequence());
+    // empty sequence
+    std::vector<Expr> seq;
+    return NodeManager::currentNM()->mkConst(
+        ExprSequence(SequenceType(type.toType()), seq));
+  }
+}; /* struct SequenceProperties */
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index d24206860..c25363e65 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -158,6 +158,67 @@ void StringEnumLen::mkCurr()
   d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
 }
 
+SeqEnumLen::SeqEnumLen(TypeNode tn,
+                       TypeEnumeratorProperties* tep,
+                       uint32_t startLength)
+    : SEnumLen(tn, startLength)
+{
+  d_elementEnumerator.reset(
+      new TypeEnumerator(d_type.getSequenceElementType(), tep));
+  mkCurr();
+}
+
+SeqEnumLen::SeqEnumLen(TypeNode tn,
+                       TypeEnumeratorProperties* tep,
+                       uint32_t startLength,
+                       uint32_t endLength)
+    : SEnumLen(tn, startLength, endLength)
+{
+  d_elementEnumerator.reset(
+      new TypeEnumerator(d_type.getSequenceElementType(), tep));
+  mkCurr();
+}
+
+SeqEnumLen::SeqEnumLen(const SeqEnumLen& wenum)
+    : SEnumLen(wenum),
+      d_elementEnumerator(new TypeEnumerator(*wenum.d_elementEnumerator)),
+      d_elementDomain(wenum.d_elementDomain)
+{
+}
+
+bool SeqEnumLen::increment()
+{
+  if (!d_elementEnumerator->isFinished())
+  {
+    // yet to establish domain
+    Assert(d_elementEnumerator != nullptr);
+    d_elementDomain.push_back((**d_elementEnumerator).toExpr());
+    ++(*d_elementEnumerator);
+  }
+  // the current cardinality is the domain size of the element
+  if (!d_witer->increment(d_elementDomain.size()))
+  {
+    Assert(d_elementEnumerator->isFinished());
+    d_curr = Node::null();
+    return false;
+  }
+  mkCurr();
+  return true;
+}
+
+void SeqEnumLen::mkCurr()
+{
+  std::vector<Expr> seq;
+  const std::vector<unsigned>& data = d_witer->getData();
+  for (unsigned i : data)
+  {
+    seq.push_back(d_elementDomain[i]);
+  }
+  // make sequence from seq
+  d_curr =
+      NodeManager::currentNM()->mkConst(ExprSequence(d_type.toType(), seq));
+}
+
 StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
     : TypeEnumeratorBase<StringEnumerator>(type),
       d_wenum(0, utils::getAlphabetCardinality())
@@ -182,6 +243,28 @@ StringEnumerator& StringEnumerator::operator++()
 
 bool StringEnumerator::isFinished() { return d_wenum.isFinished(); }
 
+SequenceEnumerator::SequenceEnumerator(TypeNode type,
+                                       TypeEnumeratorProperties* tep)
+    : TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0)
+{
+}
+
+SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator)
+    : TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()),
+      d_wenum(enumerator.d_wenum)
+{
+}
+
+Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); }
+
+SequenceEnumerator& SequenceEnumerator::operator++()
+{
+  d_wenum.increment();
+  return *this;
+}
+
+bool SequenceEnumerator::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 b379ce5c3..c82892624 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -136,6 +136,34 @@ class StringEnumLen : public SEnumLen
   void mkCurr();
 };
 
+/**
+ * Enumerates sequence values for a given length.
+ */
+class SeqEnumLen : public SEnumLen
+{
+ public:
+  /** For sequences */
+  SeqEnumLen(TypeNode tn, TypeEnumeratorProperties* tep, uint32_t startLength);
+  SeqEnumLen(TypeNode tn,
+             TypeEnumeratorProperties* tep,
+             uint32_t startLength,
+             uint32_t endLength);
+  /** copy constructor */
+  SeqEnumLen(const SeqEnumLen& wenum);
+  /** destructor */
+  ~SeqEnumLen() {}
+  /** increment */
+  bool increment() override;
+
+ private:
+  /** an enumerator for the elements' type */
+  std::unique_ptr<TypeEnumerator> d_elementEnumerator;
+  /** The domain */
+  std::vector<Expr> d_elementDomain;
+  /** Make the current term from d_data */
+  void mkCurr();
+};
+
 class StringEnumerator : public TypeEnumeratorBase<StringEnumerator>
 {
  public:
@@ -154,6 +182,21 @@ class StringEnumerator : public TypeEnumeratorBase<StringEnumerator>
   StringEnumLen d_wenum;
 }; /* class StringEnumerator */
 
+class SequenceEnumerator : public TypeEnumeratorBase<SequenceEnumerator>
+{
+ public:
+  SequenceEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
+  SequenceEnumerator(const SequenceEnumerator& enumerator);
+  ~SequenceEnumerator() {}
+  Node operator*() override;
+  SequenceEnumerator& operator++() override;
+  bool isFinished() override;
+
+ private:
+  /** underlying sequence enumerator */
+  SeqEnumLen d_wenum;
+}; /* class SequenceEnumerator */
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */