From 9efc82b701f1ab3a395306662f6d4fa37b130218 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Mar 2020 13:11:21 -0500 Subject: [PATCH] Generalize type rules for strings to sequences (#3987) Towards theory of sequences. --- src/theory/strings/kinds | 42 +-- .../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" - # 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" -#typerules +# regular expressions + typerule REGEXP_CONCAT "SimpleTypeRuleVar" typerule REGEXP_UNION "SimpleTypeRuleVar" typerule REGEXP_INTER "SimpleTypeRuleVar" @@ -91,21 +90,30 @@ typerule REGEXP_OPT "SimpleTypeRule" typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule typerule REGEXP_LOOP "SimpleTypeRule>" typerule REGEXP_COMPLEMENT "SimpleTypeRule" - typerule STRING_TO_REGEXP "SimpleTypeRule" +typerule STRING_IN_REGEXP "SimpleTypeRule" +typerule REGEXP_EMPTY "SimpleTypeRule" +typerule REGEXP_SIGMA "SimpleTypeRule" + +### operators that apply to both strings and sequences -typerule STRING_CONCAT "SimpleTypeRuleVar" -typerule STRING_LENGTH "SimpleTypeRule" -typerule STRING_SUBSTR "SimpleTypeRule" -typerule STRING_CHARAT "SimpleTypeRule" -typerule STRING_STRCTN "SimpleTypeRule" +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" typerule STRING_LT "SimpleTypeRule" typerule STRING_LEQ "SimpleTypeRule" -typerule STRING_STRIDOF "SimpleTypeRule" -typerule STRING_STRREPL "SimpleTypeRule" -typerule STRING_STRREPLALL "SimpleTypeRule" -typerule STRING_PREFIX "SimpleTypeRule" -typerule STRING_SUFFIX "SimpleTypeRule" typerule STRING_IS_DIGIT "SimpleTypeRule" typerule STRING_ITOS "SimpleTypeRule" typerule STRING_STOI "SimpleTypeRule" @@ -113,11 +121,5 @@ typerule STRING_TO_CODE "SimpleTypeRule" typerule STRING_FROM_CODE "SimpleTypeRule" typerule STRING_TOUPPER "SimpleTypeRule" typerule STRING_TOLOWER "SimpleTypeRule" -typerule STRING_REV "SimpleTypeRule" - -typerule STRING_IN_REGEXP "SimpleTypeRule" - -typerule REGEXP_EMPTY "SimpleTypeRule" -typerule REGEXP_SIGMA "SimpleTypeRule" 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) -- 2.30.2