Generalize type rules for strings to sequences (#3987)

Towards theory of sequences.

2 files changed, 276 insertions, 20 deletions

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 9d12cd906..6c7846737 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -58,8 +58,6 @@ constant CONST_STRING \
     "util/regexp.h" \
     "a string of characters"
 
-typerule CONST_STRING "SimpleTypeRule<RString>"
-
 # equal equal / less than / output
 operator STRING_TO_REGEXP 1 "convert string to regexp"
 operator REGEXP_CONCAT 2: "regexp concat"
@@ -80,7 +78,8 @@ operator REGEXP_SIGMA 0 "regexp all characters"
 operator REGEXP_RV 1 "regexp rv (internal use only)"
 typerule REGEXP_RV "SimpleTypeRule<RRegExp, AInteger>"
 
-#typerules
+# regular expressions
+
 typerule REGEXP_CONCAT "SimpleTypeRuleVar<RRegExp, ARegExp>"
 typerule REGEXP_UNION "SimpleTypeRuleVar<RRegExp, ARegExp>"
 typerule REGEXP_INTER "SimpleTypeRuleVar<RRegExp, ARegExp>"
@@ -91,21 +90,30 @@ typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>"
 typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
 typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp, AInteger, AOptional<AInteger>>"
 typerule REGEXP_COMPLEMENT "SimpleTypeRule<RRegExp, ARegExp>"
-
 typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
+typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
+typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>"
+typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>"
+
+### operators that apply to both strings and sequences
 
-typerule STRING_CONCAT "SimpleTypeRuleVar<RString, AString>"
-typerule STRING_LENGTH "SimpleTypeRule<RInteger, AString>"
-typerule STRING_SUBSTR "SimpleTypeRule<RString, AString, AInteger, AInteger>"
-typerule STRING_CHARAT "SimpleTypeRule<RString, AString, AInteger>"
-typerule STRING_STRCTN "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
+typerule STRING_LENGTH ::CVC4::theory::strings::StringStrToIntTypeRule
+typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
+typerule STRING_CHARAT ::CVC4::theory::strings::StringAtTypeRule
+typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule
+typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
+typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
+typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule
+typerule STRING_PREFIX ::CVC4::theory::strings::StringStrToBoolTypeRule
+typerule STRING_SUFFIX ::CVC4::theory::strings::StringStrToBoolTypeRule
+typerule STRING_REV ::CVC4::theory::strings::StringStrToStrTypeRule
+
+### string specific operators
+
+typerule CONST_STRING "SimpleTypeRule<RString>"
 typerule STRING_LT "SimpleTypeRule<RBool, AString, AString>"
 typerule STRING_LEQ "SimpleTypeRule<RBool, AString, AString>"
-typerule STRING_STRIDOF "SimpleTypeRule<RInteger, AString, AString, AInteger>"
-typerule STRING_STRREPL "SimpleTypeRule<RString, AString, AString, AString>"
-typerule STRING_STRREPLALL "SimpleTypeRule<RString, AString, AString, AString>"
-typerule STRING_PREFIX "SimpleTypeRule<RBool, AString, AString>"
-typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>"
 typerule STRING_IS_DIGIT "SimpleTypeRule<RBool, AString>"
 typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
 typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
@@ -113,11 +121,5 @@ typerule STRING_TO_CODE "SimpleTypeRule<RInteger, AString>"
 typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>"
 typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
 typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
-typerule STRING_REV "SimpleTypeRule<RString, AString>"
-
-typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
-
-typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>"
-typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>"
 
 endtheory
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 497366f40..6abb57504 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -24,6 +24,260 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+class StringConcatTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    TypeNode tret;
+    for (const Node& nc : n)
+    {
+      TypeNode t = nc.getType(check);
+      if (tret.isNull())
+      {
+        tret = t;
+        if (check)
+        {
+          if (!t.isStringLike())
+          {
+            throw TypeCheckingExceptionPrivate(
+                n, "expecting string-like terms in concat");
+          }
+        }
+        else
+        {
+          break;
+        }
+      }
+      else if (t != tret)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting all children to have the same type in concat");
+      }
+    }
+    return tret;
+  }
+};
+
+class StringSubstrTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (check)
+    {
+      if (!t.isStringLike())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string-like term in substr");
+      }
+      TypeNode t2 = n[1].getType(check);
+      if (!t2.isInteger())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting an integer start term in substr");
+      }
+      t2 = n[2].getType(check);
+      if (!t2.isInteger())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting an integer length term in substr");
+      }
+    }
+    return t;
+  }
+};
+
+class StringAtTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (check)
+    {
+      if (!t.isStringLike())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string-like term in str.at");
+      }
+      TypeNode t2 = n[1].getType(check);
+      if (!t2.isInteger())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting an integer start term in str.at");
+      }
+    }
+    return t;
+  }
+};
+
+class StringIndexOfTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (check)
+    {
+      TypeNode t = n[0].getType(check);
+      if (!t.isStringLike())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string-like term in indexof");
+      }
+      TypeNode t2 = n[1].getType(check);
+      if (t != t2)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n,
+            "expecting a term in second argument of indexof that is the same "
+            "type as the first argument");
+      }
+      t = n[2].getType(check);
+      if (!t.isInteger())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting an integer term in third argument of indexof");
+      }
+    }
+    return nodeManager->integerType();
+  }
+};
+
+class StringReplaceTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (check)
+    {
+      if (!t.isStringLike())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string-like term in replace");
+      }
+      TypeNode t2 = n[1].getType(check);
+      if (t != t2)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n,
+            "expecting a term in second argument of replace that is the same "
+            "type as the first argument");
+      }
+      t2 = n[2].getType(check);
+      if (t != t2)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n,
+            "expecting a term in third argument of replace that is the same "
+            "type as the first argument");
+      }
+    }
+    return t;
+  }
+};
+
+class StringStrToBoolTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (check)
+    {
+      TypeNode t = n[0].getType(check);
+      if (!t.isStringLike())
+      {
+        std::stringstream ss;
+        ss << "expecting a string-like term in argument of " << n.getKind();
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};
+
+class StringStrToIntTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (check)
+    {
+      TypeNode t = n[0].getType(check);
+      if (!t.isStringLike())
+      {
+        std::stringstream ss;
+        ss << "expecting a string-like term in argument of " << n.getKind();
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+    }
+    return nodeManager->integerType();
+  }
+};
+
+class StringStrToStrTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (check)
+    {
+      if (!t.isStringLike())
+      {
+        std::stringstream ss;
+        ss << "expecting a string term in argument of " << n.getKind();
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+    }
+    return t;
+  }
+};
+
+class StringRelationTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (check)
+    {
+      TypeNode t = n[0].getType(check);
+      if (!t.isStringLike())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string-like term in relation");
+      }
+      TypeNode t2 = n[1].getType(check);
+      if (t != t2)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting two terms of the same string-like type in relation");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};
+
 class RegExpRangeTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)