Front end support for sequences (#4690)

With this PR, we now support a preliminary draft of a theory of sequences.

This PR adds front end support for sequences in the smt2 parser, in the new API, adds regressions and unit tests for them.

As discussed offline, many of the string kinds are given a sequence version in the external API, but not in the internal one. This means that a special case for such kinds, getKindHelper was added to Term.

We do not yet support proper smt2 printing of sequences, which will require access to this code for Kind conversions (to distinguish e.g. str.++ from seq.++).

6 files changed, 25 insertions, 10 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 074b023a2..cb30a408e 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -409,7 +409,7 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   else if (type.isStringLike())
   {
     ops.push_back(strings::Word::mkEmptyWord(type));
-    if (type.isString())
+    if (type.isString())  // string-only
     {
       // Dummy character "A". This is not necessary for sequences which
       // have the generic constructor seq.unit.
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 9f502e1f6..928414523 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -60,7 +60,7 @@ bool StringsEntail::canConstantContainConcat(Node c,
     }
     else if (n[i].getKind() == STRING_ITOS && ArithEntail::check(n[i][0]))
     {
-      Assert(c.getType().isString());
+      Assert(c.getType().isString());  // string-only
       const std::vector<unsigned>& tvec = c.getConst<String>().getVec();
       // find the first occurrence of a digit starting at pos
       while (pos < tvec.size() && !String::isDigit(tvec[pos]))
@@ -594,7 +594,7 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
       {
         if (n2[index1].isConst())
         {
-          Assert(n2[index1].getType().isString());
+          Assert(n2[index1].getType().isString());  // string-only
           CVC4::String t = n2[index1].getConst<String>();
           if (n1.size() == 1)
           {
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index b4fbbed98..d21cf069d 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -179,7 +179,7 @@ void TermRegistry::preRegisterTerm(TNode n)
     ss << "Regular expression variables are not supported.";
     throw LogicException(ss.str());
   }
-  if (tn.isString())
+  if (tn.isString())  // string-only
   {
     // all characters of constants should fall in the alphabet
     if (n.isConst())
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 9f66c5f82..192b4fd34 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -291,7 +291,8 @@ public:
 
       for(int i=0; i<2; ++i) {
         TypeNode t = (*it).getType(check);
-        if (!t.isString()) {
+        if (!t.isString())  // string-only
+        {
           throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
         }
         if (!(*it).isConst())
@@ -329,7 +330,8 @@ class ConstSequenceTypeRule
                                      bool check)
   {
     Assert(n.getKind() == kind::CONST_SEQUENCE);
-    return n.getConst<ExprSequence>().getSequence().getType();
+    return nodeManager->mkSequenceType(
+        n.getConst<ExprSequence>().getSequence().getType());
   }
 };
 
@@ -363,8 +365,8 @@ struct SequenceProperties
     Assert(type.isSequence());
     // empty sequence
     std::vector<Expr> seq;
-    return NodeManager::currentNM()->mkConst(
-        ExprSequence(SequenceType(type.toType()), seq));
+    return NodeManager::currentNM()->mkConst(ExprSequence(
+        SequenceType(type.getSequenceElementType().toType()), seq));
   }
 }; /* struct SequenceProperties */
 
diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index 6d3949514..afedaed5c 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -176,6 +176,9 @@ SeqEnumLen::SeqEnumLen(TypeNode tn,
 {
   d_elementEnumerator.reset(
       new TypeEnumerator(d_type.getSequenceElementType(), tep));
+  // ensure non-empty element domain
+  d_elementDomain.push_back((**d_elementEnumerator).toExpr());
+  ++(*d_elementEnumerator);
   mkCurr();
 }
 
@@ -212,11 +215,12 @@ void SeqEnumLen::mkCurr()
   const std::vector<unsigned>& data = d_witer->getData();
   for (unsigned i : data)
   {
+    Assert(i < d_elementDomain.size());
     seq.push_back(d_elementDomain[i]);
   }
   // make sequence from seq
-  d_curr =
-      NodeManager::currentNM()->mkConst(ExprSequence(d_type.toType(), seq));
+  d_curr = NodeManager::currentNM()->mkConst(
+      ExprSequence(d_type.getSequenceElementType().toType(), seq));
 }
 
 StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index 35b315e35..fec567733 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -452,6 +452,15 @@ Node Word::reverse(TNode x)
     std::reverse(nvec.begin(), nvec.end());
     return nm->mkConst(String(nvec));
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const std::vector<Node>& vecc = sx.getVec();
+    std::vector<Node> vecr(vecc.begin(), vecc.end());
+    std::reverse(vecr.begin(), vecr.end());
+    Sequence res(sx.getType(), vecr);
+    return nm->mkConst(res.toExprSequence());
+  }
   Unimplemented();
   return Node::null();
 }