diff options
-rw-r--r-- | src/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.cpp | 373 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 338 |
3 files changed, 396 insertions, 316 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index fabff516f..c33110cc3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -995,6 +995,7 @@ libcvc4_add_sources( theory/strings/theory_strings.h theory/strings/theory_strings_preprocess.cpp theory/strings/theory_strings_preprocess.h + theory/strings/theory_strings_type_rules.cpp theory/strings/theory_strings_type_rules.h theory/strings/theory_strings_utils.cpp theory/strings/theory_strings_utils.h diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp new file mode 100644 index 000000000..7f7799b25 --- /dev/null +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -0,0 +1,373 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Aina Niemetz, Yoni Zohar + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Typing rules for the theory of strings and regexps. + */ +#include "theory/strings/theory_strings_type_rules.h" + +#include <sstream> + +#include "expr/node_manager.h" +#include "expr/sequence.h" +#include "options/strings_options.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +TypeNode StringConcatTypeRule::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; +} + +TypeNode StringSubstrTypeRule::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; +} + +TypeNode StringUpdateTypeRule::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 update"); + } + TypeNode t2 = n[1].getType(check); + if (!t2.isInteger()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting an integer start term in update"); + } + t2 = n[2].getType(check); + if (!t2.isStringLike()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting an string-like replace term in update"); + } + } + return t; +} + +TypeNode StringAtTypeRule::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; +} + +TypeNode StringIndexOfTypeRule::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(); +} + +TypeNode StringReplaceTypeRule::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; +} + +TypeNode StringStrToBoolTypeRule::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(); +} + +TypeNode StringStrToIntTypeRule::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(); +} + +TypeNode StringStrToStrTypeRule::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; +} + +TypeNode StringRelationTypeRule::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(); +} + +TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + if (check) + { + TNode::iterator it = n.begin(); + unsigned ch[2]; + + for (int i = 0; i < 2; ++i) + { + TypeNode t = (*it).getType(check); + if (!t.isString()) // string-only + { + throw TypeCheckingExceptionPrivate( + n, "expecting a string term in regexp range"); + } + if (!(*it).isConst()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting a constant string term in regexp range"); + } + if ((*it).getConst<String>().size() != 1) + { + throw TypeCheckingExceptionPrivate( + n, "expecting a single constant string term in regexp range"); + } + unsigned ci = (*it).getConst<String>().front(); + ch[i] = ci; + ++it; + } + if (ch[0] > ch[1]) + { + throw TypeCheckingExceptionPrivate( + n, + "expecting the first constant is less or equal to the second one in " + "regexp range"); + } + } + return nodeManager->regExpType(); +} + +TypeNode ConstSequenceTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + Assert(n.getKind() == kind::CONST_SEQUENCE); + return nodeManager->mkSequenceType(n.getConst<Sequence>().getType()); +} + +TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return nodeManager->mkSequenceType(n[0].getType(check)); +} + +TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + TypeNode t = n[0].getType(check); + TypeNode t1 = t.getSequenceElementType(); + if (check) + { + if (!t.isSequence()) + { + throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth"); + } + TypeNode t2 = n[1].getType(check); + if (!t2.isInteger()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting an integer start term in nth"); + } + } + return t1; +} + +Cardinality SequenceProperties::computeCardinality(TypeNode type) +{ + Assert(type.getKind() == kind::SEQUENCE_TYPE); + return Cardinality::INTEGERS; +} +/** A sequence is well-founded if its element type is */ +bool SequenceProperties::isWellFounded(TypeNode type) +{ + return type[0].isWellFounded(); +} +/** Make ground term for sequence type (return the empty sequence) */ +Node SequenceProperties::mkGroundTerm(TypeNode type) +{ + Assert(type.isSequence()); + // empty sequence + std::vector<Node> seq; + return NodeManager::currentNM()->mkConst( + Sequence(type.getSequenceElementType(), seq)); +} +} // namespace strings +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 93c252942..496599252 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -14,405 +14,111 @@ */ #include "cvc4_private.h" -#include "options/strings_options.h" #ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H #define CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H -#include "expr/sequence.h" +#include "expr/node.h" namespace cvc5 { + +class NodeManager; +class TypeNode; + 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; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; class StringUpdateTypeRule { 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 update"); - } - TypeNode t2 = n[1].getType(check); - if (!t2.isInteger()) - { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer start term in update"); - } - t2 = n[2].getType(check); - if (!t2.isStringLike()) - { - throw TypeCheckingExceptionPrivate( - n, "expecting an string-like replace term in update"); - } - } - return t; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; 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(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; class RegExpRangeTypeRule { public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - if( check ) { - TNode::iterator it = n.begin(); - unsigned ch[2]; - - for(int i=0; i<2; ++i) { - TypeNode t = (*it).getType(check); - if (!t.isString()) // string-only - { - throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range"); - } - if (!(*it).isConst()) - { - throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range"); - } - if( (*it).getConst<String>().size() != 1 ) { - throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range"); - } - unsigned ci = (*it).getConst<String>().front(); - ch[i] = ci; - ++it; - } - if(ch[0] > ch[1]) { - throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range"); - } - } - return nodeManager->regExpType(); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; class ConstSequenceTypeRule { public: - static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - Assert(n.getKind() == kind::CONST_SEQUENCE); - return nodeManager->mkSequenceType(n.getConst<Sequence>().getType()); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; class SeqUnitTypeRule { public: - static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - return nodeManager->mkSequenceType(n[0].getType(check)); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; class SeqNthTypeRule { public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TypeNode t = n[0].getType(check); - TypeNode t1 = t.getSequenceElementType(); - if (check) - { - if (!t.isSequence()) - { - throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth"); - } - TypeNode t2 = n[1].getType(check); - if (!t2.isInteger()) - { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer start term in nth"); - } - } - return t1; - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; /** Properties of the sequence type */ struct SequenceProperties { - static Cardinality computeCardinality(TypeNode type) - { - Assert(type.getKind() == kind::SEQUENCE_TYPE); - return Cardinality::INTEGERS; - } + static Cardinality computeCardinality(TypeNode type); /** A sequence is well-founded if its element type is */ - static bool isWellFounded(TypeNode type) - { - return type[0].isWellFounded(); - } + static bool isWellFounded(TypeNode type); /** Make ground term for sequence type (return the empty sequence) */ - static Node mkGroundTerm(TypeNode type) - { - Assert(type.isSequence()); - // empty sequence - std::vector<Node> seq; - return NodeManager::currentNM()->mkConst( - Sequence(type.getSequenceElementType(), seq)); - } + static Node mkGroundTerm(TypeNode type); }; /* struct SequenceProperties */ } // namespace strings |