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.++).

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();
   }