diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-13 13:11:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-13 11:11:21 -0700 |
commit | 9efc82b701f1ab3a395306662f6d4fa37b130218 (patch) | |
tree | 2ff901c9147cbc84c6b22fc65bab3435c5cc7a15 /src/theory | |
parent | 3e96419d27621be3c0c0d4f3af4b14afb0ce24a8 (diff) |
Generalize type rules for strings to sequences (#3987)
Towards theory of sequences.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/kinds | 42 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 254 |
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) |