From bcd0007231ebdef6e555dae07255c06a93397794 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 21 Dec 2023 14:13:47 -0600 Subject: [PATCH] Update strings to gradual type system (#9821) --- .../strings/theory_strings_type_rules.cpp | 337 +++++++++++------- test/unit/node/CMakeLists.txt | 2 + test/unit/node/node_type_rules.cpp | 67 ++++ 3 files changed, 286 insertions(+), 120 deletions(-) create mode 100644 test/unit/node/node_type_rules.cpp diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index 4b4eb6cb026..8f379f081ea 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -25,6 +25,20 @@ namespace cvc5::internal { namespace theory { namespace strings { +bool isMaybeStringLike(const TypeNode& tn) +{ + if (tn.isString()) + { + return true; + } + return tn.isMaybeKind(Kind::SEQUENCE_TYPE); +} + +bool isMaybeInteger(const TypeNode& tn) +{ + return tn.isInteger() || tn.isFullyAbstract(); +} + TypeNode StringConcatTypeRule::preComputeType(NodeManager* nm, TNode n) { return TypeNode::null(); @@ -37,29 +51,35 @@ TypeNode StringConcatTypeRule::computeType(NodeManager* nodeManager, TypeNode tret; for (const Node& nc : n) { - TypeNode t = nc.getType(check); - if (tret.isNull()) + TypeNode t = nc.getTypeOrNull(); + if (check) { - tret = t; - if (check) + if (!isMaybeStringLike(t)) { - if (!t.isStringLike()) + if (errOut) { - throw TypeCheckingExceptionPrivate( - n, "expecting string-like terms in concat"); + (*errOut) << "expecting string-like terms in concat"; } - } - else - { - break; + return TypeNode::null(); } } - else if (t != tret) + if (tret.isNull()) { - throw TypeCheckingExceptionPrivate( - n, "expecting all children to have the same type in concat"); + tret = t; + continue; + } + tret = tret.leastUpperBound(t); + if (tret.isNull()) + { + if (errOut) + { + (*errOut) << "expecting comparable terms in concat"; + } + return TypeNode::null(); } } + // note we could be fully abstract if all arguments are fully abstract, + // this is due to the fact that string/sequence are not comparable. return tret; } @@ -72,27 +92,37 @@ TypeNode StringSubstrTypeRule::computeType(NodeManager* nodeManager, bool check, std::ostream* errOut) { - TypeNode t = n[0].getType(check); + TypeNode t = n[0].getTypeOrNull(); if (check) { - if (!t.isStringLike()) + if (!isMaybeStringLike(t)) { - throw TypeCheckingExceptionPrivate( - n, "expecting a string-like term in substr"); + if (errOut) + { + (*errOut) << "expecting a string-like term in substr"; + } + return TypeNode::null(); } - TypeNode t2 = n[1].getType(check); - if (!t2.isInteger()) + TypeNode t2 = n[1].getTypeOrNull(); + if (!isMaybeInteger(t2)) { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer start term in substr"); + if (errOut) + { + (*errOut) << "expecting an integer start term in substr"; + } + return TypeNode::null(); } - t2 = n[2].getType(check); - if (!t2.isInteger()) + t2 = n[2].getTypeOrNull(); + if (!isMaybeInteger(t2)) { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer length term in substr"); + if (errOut) + { + (*errOut) << "expecting an integer length term in substr"; + } + return TypeNode::null(); } } + // note that we could be fully abstract if the argument is fully abstract return t; } @@ -105,28 +135,39 @@ TypeNode StringUpdateTypeRule::computeType(NodeManager* nodeManager, bool check, std::ostream* errOut) { - TypeNode t = n[0].getType(check); - if (check) + TypeNode t = n[0].getTypeOrNull(); + TypeNode t3 = n[2].getTypeOrNull(); + TypeNode tret = t.leastUpperBound(t3); + if (tret.isNull()) { - if (!t.isStringLike()) + if (errOut) { - throw TypeCheckingExceptionPrivate( - n, "expecting a string-like term in update"); + (*errOut) << "expecting compatible string-like terms"; } - TypeNode t2 = n[1].getType(check); - if (!t2.isInteger()) + return TypeNode::null(); + } + if (check) + { + // check that the return is maybe string-like + if (!isMaybeStringLike(tret)) { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer start term in update"); + if (errOut) + { + (*errOut) << "expecting string-like terms in update"; + } + return TypeNode::null(); } - t2 = n[2].getType(check); - if (!t2.isStringLike()) + TypeNode t2 = n[1].getTypeOrNull(); + if (!isMaybeInteger(t2)) { - throw TypeCheckingExceptionPrivate( - n, "expecting an string-like replace term in update"); + if (errOut) + { + (*errOut) << "expecting an integer start term in update"; + } + return TypeNode::null(); } } - return t; + return tret; } TypeNode StringAtTypeRule::preComputeType(NodeManager* nm, TNode n) @@ -138,19 +179,25 @@ TypeNode StringAtTypeRule::computeType(NodeManager* nodeManager, bool check, std::ostream* errOut) { - TypeNode t = n[0].getType(check); + TypeNode t = n[0].getTypeOrNull(); if (check) { - if (!t.isStringLike()) + if (!isMaybeStringLike(t)) { - throw TypeCheckingExceptionPrivate( - n, "expecting a string-like term in str.at"); + if (errOut) + { + (*errOut) << "expecting a string-like term in str.at"; + } + return TypeNode::null(); } - TypeNode t2 = n[1].getType(check); - if (!t2.isInteger()) + TypeNode t2 = n[1].getTypeOrNull(); + if (!isMaybeInteger(t2)) { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer start term in str.at"); + if (errOut) + { + (*errOut) << "expecting an integer start term in str.at"; + } + return TypeNode::null(); } } return t; @@ -167,25 +214,33 @@ TypeNode StringIndexOfTypeRule::computeType(NodeManager* nodeManager, { if (check) { - TypeNode t = n[0].getType(check); - if (!t.isStringLike()) + TypeNode t = n[0].getTypeOrNull(); + if (!isMaybeStringLike(t)) { - throw TypeCheckingExceptionPrivate( - n, "expecting a string-like term in indexof"); + if (errOut) + { + (*errOut) << "expecting a string-like term in indexof"; + } + return TypeNode::null(); } - TypeNode t2 = n[1].getType(check); - if (t != t2) + TypeNode t2 = n[1].getTypeOrNull(); + if (!t.isComparableTo(t2)) { - throw TypeCheckingExceptionPrivate( - n, - "expecting a term in second argument of indexof that is the same " - "type as the first argument"); + if (errOut) + { + (*errOut) << "expecting a term in second argument of indexof that is " + "the same type as the first argument"; + } + return TypeNode::null(); } - t = n[2].getType(check); - if (!t.isInteger()) + t = n[2].getTypeOrNull(); + if (!isMaybeInteger(t)) { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer term in third argument of indexof"); + if (errOut) + { + (*errOut) << "expecting an integer term in third argument of indexof"; + } + return TypeNode::null(); } } return nodeManager->integerType(); @@ -200,29 +255,35 @@ TypeNode StringReplaceTypeRule::computeType(NodeManager* nodeManager, bool check, std::ostream* errOut) { - TypeNode t = n[0].getType(check); - if (check) + TypeNode t; + for (const Node& nc : n) { - if (!t.isStringLike()) + TypeNode tc = nc.getTypeOrNull(); + if (check) { - throw TypeCheckingExceptionPrivate( - n, "expecting a string-like term in replace"); + if (!isMaybeStringLike(tc)) + { + if (errOut) + { + (*errOut) << "expecting a string-like term in replace"; + } + return TypeNode::null(); + } } - TypeNode t2 = n[1].getType(check); - if (t != t2) + // if first child + if (t.isNull()) { - throw TypeCheckingExceptionPrivate( - n, - "expecting a term in second argument of replace that is the same " - "type as the first argument"); + t = tc; + continue; } - t2 = n[2].getType(check); - if (t != t2) + t = t.leastUpperBound(tc); + if (t.isNull()) { - throw TypeCheckingExceptionPrivate( - n, - "expecting a term in third argument of replace that is the same " - "type as the first argument"); + if (errOut) + { + (*errOut) << "expecting comparable string-like terms"; + } + return TypeNode::null(); } } return t; @@ -243,11 +304,14 @@ TypeNode StringStrToBoolTypeRule::computeType(NodeManager* nodeManager, for (const Node& nc : n) { TypeNode t = nc.getType(check); - if (!t.isStringLike()) + if (!isMaybeStringLike(t)) { - std::stringstream ss; - ss << "expecting a string-like term in argument of " << n.getKind(); - throw TypeCheckingExceptionPrivate(n, ss.str()); + if (errOut) + { + (*errOut) << "expecting a string-like term in argument of " + << n.getKind(); + } + return TypeNode::null(); } if (firstType.isNull()) { @@ -255,9 +319,12 @@ TypeNode StringStrToBoolTypeRule::computeType(NodeManager* nodeManager, } else if (!t.isComparableTo(firstType)) { - std::stringstream ss; - ss << "expecting string terms of the same type in " << n.getKind(); - throw TypeCheckingExceptionPrivate(n, ss.str()); + if (errOut) + { + (*errOut) << "expecting string terms of the same type in " + << n.getKind(); + } + return TypeNode::null(); } } } @@ -275,12 +342,15 @@ TypeNode StringStrToIntTypeRule::computeType(NodeManager* nodeManager, { if (check) { - TypeNode t = n[0].getType(check); - if (!t.isStringLike()) + TypeNode t = n[0].getTypeOrNull(); + if (!isMaybeStringLike(t)) { - std::stringstream ss; - ss << "expecting a string-like term in argument of " << n.getKind(); - throw TypeCheckingExceptionPrivate(n, ss.str()); + if (errOut) + { + (*errOut) << "expecting a string-like term in argument of " + << n.getKind(); + } + return TypeNode::null(); } } return nodeManager->integerType(); @@ -295,14 +365,16 @@ TypeNode StringStrToStrTypeRule::computeType(NodeManager* nodeManager, bool check, std::ostream* errOut) { - TypeNode t = n[0].getType(check); + TypeNode t = n[0].getTypeOrNull(); if (check) { - if (!t.isStringLike()) + if (!isMaybeStringLike(t)) { - std::stringstream ss; - ss << "expecting a string term in argument of " << n.getKind(); - throw TypeCheckingExceptionPrivate(n, ss.str()); + if (errOut) + { + (*errOut) << "expecting a string term in argument of " << n.getKind(); + } + return TypeNode::null(); } } return t; @@ -319,17 +391,24 @@ TypeNode StringRelationTypeRule::computeType(NodeManager* nodeManager, { if (check) { - TypeNode t = n[0].getType(check); - if (!t.isStringLike()) + TypeNode t = n[0].getTypeOrNull(); + if (!isMaybeStringLike(t)) { - throw TypeCheckingExceptionPrivate( - n, "expecting a string-like term in relation"); + if (errOut) + { + (*errOut) << "expecting a string-like term in relation"; + } + return TypeNode::null(); } - TypeNode t2 = n[1].getType(check); - if (t != t2) + TypeNode t2 = n[1].getTypeOrNull(); + if (!t.isComparableTo(t2)) { - throw TypeCheckingExceptionPrivate( - n, "expecting two terms of the same string-like type in relation"); + if (errOut) + { + (*errOut) + << "expecting two terms of comparable string-like type in relation"; + } + return TypeNode::null(); } } return nodeManager->booleanType(); @@ -349,11 +428,14 @@ TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager, TNode::iterator it = n.begin(); for (int i = 0; i < 2; ++i) { - TypeNode t = (*it).getType(check); - if (!t.isString()) // string-only + TypeNode t = (*it).getTypeOrNull(); + if (!t.isString() && !t.isFullyAbstract()) // string-only { - throw TypeCheckingExceptionPrivate( - n, "expecting a string term in regexp range"); + if (errOut) + { + (*errOut) << "expecting a string term in regexp range"; + } + return TypeNode::null(); } ++it; } @@ -372,10 +454,14 @@ TypeNode StringToRegExpTypeRule::computeType(NodeManager* nodeManager, { if (check) { - if (!n[0].getType().isString()) + TypeNode tn = n[0].getTypeOrNull(); + if (!tn.isString() && !tn.isFullyAbstract()) { - throw TypeCheckingExceptionPrivate( - n, "expecting string term in string to regexp"); + if (errOut) + { + (*errOut) << "expecting string term in string to regexp"; + } + return TypeNode::null(); } } return nodeManager->regExpType(); @@ -410,7 +496,7 @@ TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager, std::ostream* errOut) { Assert(n.getKind() == Kind::SEQ_UNIT); - TypeNode argType = n[0].getType(check); + TypeNode argType = n[0].getTypeOrNull(); return nodeManager->mkSequenceType(argType); } @@ -424,21 +510,32 @@ TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager, std::ostream* errOut) { Assert(n.getKind() == Kind::SEQ_NTH); - TypeNode t = n[0].getType(check); - if (check && !t.isStringLike()) + TypeNode t = n[0].getTypeOrNull(); + if (check && !isMaybeStringLike(t)) { - throw TypeCheckingExceptionPrivate(n, - "expecting a string-like term in nth"); + if (errOut) + { + (*errOut) << "expecting a string-like term in nth"; + } + return TypeNode::null(); } if (check) { - TypeNode t2 = n[1].getType(check); - if (!t2.isInteger()) + TypeNode t2 = n[1].getTypeOrNull(); + if (!isMaybeInteger(t2)) { - throw TypeCheckingExceptionPrivate( - n, "expecting an integer start term in nth"); + if (errOut) + { + (*errOut) << "expecting an integer start term in nth"; + } + return TypeNode::null(); } } + if (t.isAbstract()) + { + // if selecting from abstract, we don't know the type + return nodeManager->mkAbstractType(Kind::ABSTRACT_TYPE); + } if (t.isSequence()) { return t.getSequenceElementType(); diff --git a/test/unit/node/CMakeLists.txt b/test/unit/node/CMakeLists.txt index 04638bd312a..7002146197d 100644 --- a/test/unit/node/CMakeLists.txt +++ b/test/unit/node/CMakeLists.txt @@ -30,3 +30,5 @@ cvc5_add_unit_test_white(node_white node) cvc5_add_unit_test_black(symbol_table_black node) cvc5_add_unit_test_black(type_cardinality_black node) cvc5_add_unit_test_white(type_node_white node) +cvc5_add_unit_test_white(node_type_rules node) + diff --git a/test/unit/node/node_type_rules.cpp b/test/unit/node/node_type_rules.cpp new file mode 100644 index 00000000000..44a45c6ade6 --- /dev/null +++ b/test/unit/node/node_type_rules.cpp @@ -0,0 +1,67 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2023 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. + * **************************************************************************** + * + * Black box testing of type rules for cvc5::Node. + */ + +#include + +#include +#include +#include +#include + +#include "expr/node_manager.h" +#include "expr/type_node.h" +#include "test_node.h" +#include "util/rational.h" + +namespace cvc5::internal { +namespace test { + +class TestNodeTestRules : public TestNode +{ + protected: + TypeNode getTypeConcat(const Node& a, const Node& b) + { + NodeManager* nm = NodeManager::currentNM(); + Node c = nm->mkNode(Kind::STRING_CONCAT, a, b); + return c.getTypeOrNull(true); + } +}; + +TEST_F(TestNodeTestRules, gradual_types) +{ + NodeManager* nm = NodeManager::currentNM(); + TypeNode at = nm->mkAbstractType(Kind::ABSTRACT_TYPE); + TypeNode aseqt = nm->mkAbstractType(Kind::SEQUENCE_TYPE); + TypeNode intt = nm->integerType(); + TypeNode sit = nm->mkSequenceType(intt); + + SkolemManager* sm = nm->getSkolemManager(); + Node kat = sm->mkDummySkolem("kat", at); + Node kaseqt = sm->mkDummySkolem("kaseqt", aseqt); + Node ksit = sm->mkDummySkolem("ksit", sit); + Node one = nm->mkConstInt(Rational(1)); + + TypeNode t1 = getTypeConcat(kat, kat); + ASSERT_TRUE(t1 == at); + TypeNode t2 = getTypeConcat(kat, kaseqt); + ASSERT_TRUE(t2 == aseqt); + TypeNode t3 = getTypeConcat(kat, ksit); + ASSERT_TRUE(t3 == sit); + TypeNode t4 = getTypeConcat(kat, one); + ASSERT_TRUE(t4.isNull()); +} + +} // namespace test +} // namespace cvc5::internal