4 files changed, 47 insertions, 5 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b504d290b..fe5f5e636 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -244,6 +244,7 @@ tokens {
   REGEXP_EMPTY_TOK = 'RE_EMPTY';
   REGEXP_SIGMA_TOK = 'RE_SIGMA';
   REGEXP_COMPLEMENT_TOK = 'RE_COMPLEMENT';
+  SEQ_UNIT_TOK = 'SEQ_UNIT';
 
   SETS_CARD_TOK = 'CARD';
 
@@ -2080,6 +2081,8 @@ stringTerm[CVC4::api::Term& f]
     }
   | REGEXP_COMPLEMENT_TOK LPAREN formula[f] RPAREN
     { f = MK_TERM(CVC4::api::REGEXP_COMPLEMENT, f); }
+  | SEQ_UNIT_TOK LPAREN formula[f] RPAREN
+    { f = MK_TERM(CVC4::api::SEQ_UNIT, f); }
   | REGEXP_EMPTY_TOK
     { f = MK_TERM(CVC4::api::REGEXP_EMPTY, std::vector<api::Term>()); }
   | REGEXP_SIGMA_TOK
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 5d80dd55f..a5ce1bed0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -563,6 +563,22 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
   {
     t = d_solver->mkEmptySet(s);
   }
+  else if (k == api::CONST_SEQUENCE)
+  {
+    if (!s.isSequence())
+    {
+      std::stringstream ss;
+      ss << "Type ascription on empty sequence must be a sequence, got " << s;
+      parseError(ss.str());
+    }
+    if (!t.getConstSequenceElements().empty())
+    {
+      std::stringstream ss;
+      ss << "Cannot apply a type ascription to a non-empty sequence";
+      parseError(ss.str());
+    }
+    t = d_solver->mkEmptySequence(s.getSequenceElementSort());
+  }
   else if (k == api::UNIVERSE_SET)
   {
     t = d_solver->mkUniverseSet(s);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 703696cf5..cc87306e3 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2122,7 +2122,13 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
             PARSER_STATE->parseError("Illegal set type.");
           }
           t = SOLVER->mkSetSort( args[0] );
-        } else if(name == "Tuple") {
+        } else if(name == "Seq" && !PARSER_STATE->strictModeEnabled() &&
+                  PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) ) {
+          if(args.size() != 1) {
+            PARSER_STATE->parseError("Illegal sequence type.");
+          }
+          t = SOLVER->mkSequenceSort( args[0] );
+        } else if (name == "Tuple" && !PARSER_STATE->strictModeEnabled()) {
           t = SOLVER->mkTupleSort(args);
         } else if(check == CHECK_DECLARED ||
                   PARSER_STATE->isDeclared(name, SYM_SORT)) {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 68b1945fc..aba409109 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -156,6 +156,10 @@ void Smt2::addStringOperators() {
   addOperator(api::STRING_CHARAT, "str.at");
   addOperator(api::STRING_INDEXOF, "str.indexof");
   addOperator(api::STRING_REPLACE, "str.replace");
+  addOperator(api::STRING_PREFIX, "str.prefixof");
+  addOperator(api::STRING_SUFFIX, "str.suffixof");
+  addOperator(api::STRING_FROM_CODE, "str.from_code");
+  addOperator(api::STRING_IS_DIGIT, "str.is_digit");
   addOperator(api::STRING_REPLACE_RE, "str.replace_re");
   addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all");
   if (!strictModeEnabled())
@@ -163,11 +167,20 @@ void Smt2::addStringOperators() {
     addOperator(api::STRING_TOLOWER, "str.tolower");
     addOperator(api::STRING_TOUPPER, "str.toupper");
     addOperator(api::STRING_REV, "str.rev");
+    // sequence versions
+    addOperator(api::SEQ_CONCAT, "seq.++");
+    addOperator(api::SEQ_LENGTH, "seq.len");
+    addOperator(api::SEQ_EXTRACT, "seq.extract");
+    addOperator(api::SEQ_AT, "seq.at");
+    addOperator(api::SEQ_CONTAINS, "seq.contains");
+    addOperator(api::SEQ_INDEXOF, "seq.indexof");
+    addOperator(api::SEQ_REPLACE, "seq.replace");
+    addOperator(api::SEQ_PREFIX, "seq.prefixof");
+    addOperator(api::SEQ_SUFFIX, "seq.suffixof");
+    addOperator(api::SEQ_REV, "seq.rev");
+    addOperator(api::SEQ_REPLACE_ALL, "seq.replace_all");
+    addOperator(api::SEQ_UNIT, "seq.unit");
   }
-  addOperator(api::STRING_PREFIX, "str.prefixof");
-  addOperator(api::STRING_SUFFIX, "str.suffixof");
-  addOperator(api::STRING_FROM_CODE, "str.from_code");
-  addOperator(api::STRING_IS_DIGIT, "str.is_digit");
   // at the moment, we only use this syntax for smt2.6
   if (getLanguage() == language::input::LANG_SMTLIB_V2_6
       || getLanguage() == language::input::LANG_SYGUS_V2)
@@ -692,6 +705,10 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     }
     defineVar("re.allchar", d_solver->mkRegexpSigma());
 
+    // Boolean is a placeholder
+    defineVar("seq.empty",
+              d_solver->mkEmptySequence(d_solver->getBooleanSort()));
+
     addStringOperators();
   }