Convert more uses of strings to words (#4584)

Towards theory of sequences.

This PR also adds support for sequences in default sygus grammars.

Also removes an interface for mkEmptyWord which doesn't have an equivalent for sequences.

1 files changed, 18 insertions, 17 deletions

diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index 484b0df2d..35b315e35 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -27,7 +27,8 @@ Node Word::mkEmptyWord(TypeNode tn)
 {
   if (tn.isString())
   {
-    return mkEmptyWord(CONST_STRING);
+    std::vector<unsigned> vec;
+    return NodeManager::currentNM()->mkConst(String(vec));
   }
   else if (tn.isSequence())
   {
@@ -39,17 +40,6 @@ Node Word::mkEmptyWord(TypeNode tn)
   return Node::null();
 }
 
-Node Word::mkEmptyWord(Kind k)
-{
-  if (k == CONST_STRING)
-  {
-    std::vector<unsigned> vec;
-    return NodeManager::currentNM()->mkConst(String(vec));
-  }
-  Unimplemented();
-  return Node::null();
-}
-
 Node Word::mkWordFlatten(const std::vector<Node>& xs)
 {
   Assert(!xs.empty());
@@ -81,7 +71,8 @@ Node Word::mkWordFlatten(const std::vector<Node>& xs)
         seq.push_back(c.toExpr());
       }
     }
-    return NodeManager::currentNM()->mkConst(ExprSequence(tn.toType(), seq));
+    return NodeManager::currentNM()->mkConst(
+        ExprSequence(tn.getSequenceElementType().toType(), seq));
   }
   Unimplemented();
   return Node::null();
@@ -98,17 +89,17 @@ size_t Word::getLength(TNode x)
   {
     return x.getConst<ExprSequence>().getSequence().size();
   }
-  Unimplemented();
+  Unimplemented() << "Word::getLength on " << x;
   return 0;
 }
 
 std::vector<Node> Word::getChars(TNode x)
 {
   Kind k = x.getKind();
+  std::vector<Node> ret;
+  NodeManager* nm = NodeManager::currentNM();
   if (k == CONST_STRING)
   {
-    std::vector<Node> ret;
-    NodeManager* nm = NodeManager::currentNM();
     std::vector<unsigned> ccVec;
     const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
     for (unsigned chVal : cvec)
@@ -120,8 +111,18 @@ std::vector<Node> Word::getChars(TNode x)
     }
     return ret;
   }
+  else if (k == CONST_SEQUENCE)
+  {
+    Type t = x.getConst<ExprSequence>().getType();
+    const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+    const std::vector<Node>& vec = sx.getVec();
+    for (const Node& v : vec)
+    {
+      ret.push_back(nm->mkConst(ExprSequence(t, {v.toExpr()})));
+    }
+    return ret;
+  }
   Unimplemented();
-  std::vector<Node> ret;
   return ret;
 }