From 1de0246d86704c2d3ec9ce18f50c4325bad9a273 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Mar 2022 20:07:05 -0500 Subject: [PATCH] Fixes for API kind documentation (#8397) Also renames str.tolower -> str.to_lower, str.toupper -> str.to_upper. Co-authored-by: Aina Niemetz --- proofs/lfsc/signatures/strings_programs.plf | 4 +- proofs/lfsc/signatures/theory_def.plf | 8 +- src/api/cpp/cvc5.cpp | 8 +- src/api/cpp/cvc5.h | 4 + src/api/cpp/cvc5_kind.h | 114 ++++++++++++++---- src/parser/smt2/smt2.cpp | 4 +- src/printer/smt2/smt2_printer.cpp | 4 +- src/theory/strings/extf_solver.cpp | 6 +- src/theory/strings/kinds | 8 +- src/theory/strings/sequences_rewriter.cpp | 4 +- src/theory/strings/strings_rewriter.cpp | 20 +-- src/theory/strings/strings_rewriter.h | 2 +- src/theory/strings/term_registry.cpp | 2 +- src/theory/strings/theory_strings.cpp | 4 +- .../strings/theory_strings_preprocess.cpp | 9 +- src/theory/strings/theory_strings_utils.cpp | 4 +- .../cli/regress0/strings/parser-syms.cvc.smt2 | 2 +- .../cli/regress0/strings/tolower-rrs.smt2 | 6 +- .../cli/regress0/strings/tolower-simple.smt2 | 2 +- .../cli/regress1/strings/rev-conv1.smt2 | 2 +- .../cli/regress1/strings/tolower-find.smt2 | 4 +- test/unit/api/cpp/solver_black.cpp | 2 +- 22 files changed, 146 insertions(+), 77 deletions(-) diff --git a/proofs/lfsc/signatures/strings_programs.plf b/proofs/lfsc/signatures/strings_programs.plf index 384343052..eb7351e0c 100644 --- a/proofs/lfsc/signatures/strings_programs.plf +++ b/proofs/lfsc/signatures/strings_programs.plf @@ -135,8 +135,8 @@ ; str.replaceall ; str.replace_re ; str.replace_re_all - ; str.tolower - ; str.toupper + ; str.to_lower + ; str.to_upper ; str.rev ; str.leq )))))))) diff --git a/proofs/lfsc/signatures/theory_def.plf b/proofs/lfsc/signatures/theory_def.plf index 4e57abb37..5170932f7 100644 --- a/proofs/lfsc/signatures/theory_def.plf +++ b/proofs/lfsc/signatures/theory_def.plf @@ -172,10 +172,10 @@ (define str.rev (# x term (apply f_str.rev x))) (declare f_str.update term) (define str.update (# x term (# y term (# z term (apply (apply (apply f_str.update x) y) z))))) -(declare f_str.tolower term) -(define str.tolower (# x term (apply f_str.tolower x))) -(declare f_str.toupper term) -(define str.toupper (# x term (apply f_str.toupper x))) +(declare f_str.to_lower term) +(define str.to_lower (# x term (apply f_str.to_lower x))) +(declare f_str.to_upper term) +(define str.to_upper (# x term (apply f_str.to_upper x))) (declare f_str.to_code term) (define str.to_code (# x term (apply f_str.to_code x))) (declare f_str.from_code term) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 459ded731..7c39e991c 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -340,8 +340,8 @@ const static std::unordered_map> KIND_ENUM(STRING_REPLACE_ALL, cvc5::Kind::STRING_REPLACE_ALL), KIND_ENUM(STRING_REPLACE_RE, cvc5::Kind::STRING_REPLACE_RE), KIND_ENUM(STRING_REPLACE_RE_ALL, cvc5::Kind::STRING_REPLACE_RE_ALL), - KIND_ENUM(STRING_TOLOWER, cvc5::Kind::STRING_TOLOWER), - KIND_ENUM(STRING_TOUPPER, cvc5::Kind::STRING_TOUPPER), + KIND_ENUM(STRING_TO_LOWER, cvc5::Kind::STRING_TO_LOWER), + KIND_ENUM(STRING_TO_UPPER, cvc5::Kind::STRING_TO_UPPER), KIND_ENUM(STRING_REV, cvc5::Kind::STRING_REV), KIND_ENUM(STRING_FROM_CODE, cvc5::Kind::STRING_FROM_CODE), KIND_ENUM(STRING_TO_CODE, cvc5::Kind::STRING_TO_CODE), @@ -652,8 +652,8 @@ const static std::unordered_map {cvc5::Kind::STRING_REPLACE_ALL, STRING_REPLACE_ALL}, {cvc5::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE}, {cvc5::Kind::STRING_REPLACE_RE_ALL, STRING_REPLACE_RE_ALL}, - {cvc5::Kind::STRING_TOLOWER, STRING_TOLOWER}, - {cvc5::Kind::STRING_TOUPPER, STRING_TOUPPER}, + {cvc5::Kind::STRING_TO_LOWER, STRING_TO_LOWER}, + {cvc5::Kind::STRING_TO_UPPER, STRING_TO_UPPER}, {cvc5::Kind::STRING_REV, STRING_REV}, {cvc5::Kind::STRING_FROM_CODE, STRING_FROM_CODE}, {cvc5::Kind::STRING_TO_CODE, STRING_TO_CODE}, diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index a9e5de81c..f2156f13b 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4251,6 +4251,9 @@ class CVC5_EXPORT Solver /** * Declare a symbolic pool of terms with the given initial value. * + * For details on how pools are used to specify instructions for quantifier + * instantiation, see documentation for the #INST_POOL kind. + * * SMT-LIB: * * \verbatim embed:rst:leading-asterisk @@ -4262,6 +4265,7 @@ class CVC5_EXPORT Solver * @param symbol The name of the pool * @param sort The sort of the elements of the pool. * @param initValue The initial value of the pool + * @return The pool symbol */ Term declarePool(const std::string& symbol, const Sort& sort, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index d757406d0..edda9845f 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -333,20 +333,11 @@ enum Kind : int32_t * Cardinality constraint on uninterpreted sort. * * Interpreted as a predicate that is true when the cardinality of - * uinterpreted Sort @f$S@f$ is less than or equal to the value of - * the second argument. - * - * - Arity: `2` - * - `1:` Term of Sort @f$S@f$ - * - `2:` Term of Sort Int (positive integer value that bounds the - * cardinality of @f$S@f$) + * uinterpreted Sort @f$S@f$ is less than or equal to an upper bound. * + * - Arity: `0` * - Create Term of this Kind with: - * - Solver::mkTerm(Kind, const std::vector&) const - * - Solver::mkTerm(const Op&, const std::vector&) const - * - * - Create Op of this kind with: - * - Solver::mkOp(Kind, const std::vector&) const + * - Solver::mkCardinalityConstraint(const Sort&, uint32_t) const */ CARDINALITY_CONSTRAINT, /** @@ -502,7 +493,7 @@ enum Kind : int32_t */ INTS_DIVISION, /** - * Integer modulus, modulus by `0` undefined. + * Integer modulus, modulus by 0 undefined. * * - Arity: `2` * - `1:` Term of Sort Int @@ -2176,6 +2167,9 @@ enum Kind : int32_t APPLY_UPDATER, /** * Match expression. + + * This kind is primarily used in the parser to support the + * SMT-LIBv2 `match` expression. * * For example, the SMT-LIBv2 syntax for the following match term * \rst @@ -2216,7 +2210,7 @@ enum Kind : int32_t * * - Arity: `2` * - `1:` Term of kind #APPLY_CONSTRUCTOR (the pattern to match against) - * - `2:` Term of any Sort (the term the pattern evaluates to) + * - `2:` Term of any Sort (the term the match term evaluates to) * * - Create Term of this Kind with: * - Solver::mkTerm(Kind, const std::vector&) const @@ -2244,7 +2238,7 @@ enum Kind : int32_t * the case) * - `2:` Term of kind #APPLY_CONSTRUCTOR (the pattern expression, * applying the set of variables to the constructor) - * - `3:` Term of any Sort (the term the pattern evaluates to) + * - `3:` Term of any Sort (the term the match term evaluates to) * * - Create Term of this Kind with: * - Solver::mkTerm(Kind, const std::vector&) const @@ -3270,7 +3264,7 @@ enum Kind : int32_t * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const */ - STRING_TOLOWER, + STRING_TO_LOWER, /** * String to upper case. * @@ -3284,7 +3278,7 @@ enum Kind : int32_t * - Create Op of this kind with: * - Solver::mkOp(Kind, const std::vector&) const */ - STRING_TOUPPER, + STRING_TO_UPPER, /** * String reverse. * @@ -3988,6 +3982,8 @@ enum Kind : int32_t * Specifies a (list of) terms to be used as a pattern for quantifier * instantiation. * + * @note Should only be used as a child of #INST_PATTERN_LIST. + * * - Arity: `n > 0` * - `1..n:` Terms of any Sort * @@ -4005,6 +4001,8 @@ enum Kind : int32_t * Specifies a (list of) terms that should not be used as a pattern for * quantifier instantiation. * + * @note Should only be used as a child of #INST_PATTERN_LIST. + * * - Arity: `n > 0` * - `1..n:` Terms of any Sort * @@ -4017,10 +4015,33 @@ enum Kind : int32_t */ INST_NO_PATTERN, /** - * Instantiation pool. + * Instantiation pool annotation. * * Specifies an annotation for pool based instantiation. * + * @note Should only be used as a child of #INST_PATTERN_LIST. + * + * In detail, pool symbols can be declared via the method + * - Solver::declarePool(const std::string&, const Sort&, const std::vector&) const + * + * A pool symbol represents a set of terms of a given sort. An instantiation + * pool annotation should match the types of the quantified formula. + * + * For example, for a quantified formula: + * + * \rst + * .. code:: lisp + * + * (FORALL (VARIABLE_LIST x y) F (INST_PATTERN_LIST (INST_POOL p q))) + * \endrst + * + * if @f$x@f$ and @f$y@f$ have Sorts @f$S_1@f$ and @f$S_2@f$, + * then pool symbols @f$p@f$ and @f$q@f$ should have Sorts + * (Set @f$S_1@f$) and (Set @f$S_2@f$), respectively. + * This annotation specifies that the quantified formula above should be + * instantiated with the product of all terms that occur in the sets @f$p@f$ + * and @f$q@f$. + * * - Arity: `n > 0` * - `1..n:` Terms that comprise the pools, which are one-to-one with the * variables of the quantified formula to be instantiated @@ -4036,8 +4057,28 @@ enum Kind : int32_t /** * A instantantiation-add-to-pool annotation. * - * - Arity: `1` - * - `1:` The pool to add to. + * @note Should only be used as a child of #INST_PATTERN_LIST. + * + * An instantantiation-add-to-pool annotation indicates that when a quantified + * formula is instantiated, the instantiated version of a term should be + * added to the given pool. + * + * For example, consider a quantified formula: + * + * \rst + * .. code:: lisp + * + * (FORALL (VARIABLE_LIST x) F + * (INST_PATTERN_LIST (INST_ADD_TO_POOL (ADD x 1) p))) + * \endrst + * + * where assume that @f$x@f$ has type Int. When this quantified formula is + * instantiated with, e.g., the term @f$t@f$, the term `(ADD t 1)` is added to pool @f$p@f$. + * + * - Arity: `2` + * - `1:` The Term whose free variables are bound by the quantified formula. + * - `2:` The pool to add to, whose Sort should be a set of elements that + * match the Sort of the first argument. * * - Create Term of this Kind with: * - Solver::mkTerm(Kind, const std::vector&) const @@ -4050,8 +4091,29 @@ enum Kind : int32_t /** * A skolemization-add-to-pool annotation. * - * - Arity: `1` - * - `1:` The pool to add to. + * @note Should only be used as a child of #INST_PATTERN_LIST. + * + * An skolemization-add-to-pool annotation indicates that when a quantified + * formula is skolemized, the skolemized version of a term should be added to + * the given pool. + * + * For example, consider a quantified formula: + * + * \rst + * .. code:: lisp + * + * (FORALL (VARIABLE_LIST x) F + * (INST_PATTERN_LIST (SKOLEM_ADD_TO_POOL (ADD x 1) p))) + * \endrst + * + * where assume that @f$x@f$ has type Int. When this quantified formula is + * skolemized, e.g., with @f$k@f$ of type Int, then the term `(ADD k 1)` is + * added to the pool @f$p@f$. + * + * - Arity: `2` + * - `1:` The Term whose free variables are bound by the quantified formula. + * - `2:` The pool to add to, whose Sort should be a set of elements that + * match the Sort of the first argument. * * - Create Term of this Kind with: * - Solver::mkTerm(Kind, const std::vector&) const @@ -4067,6 +4129,8 @@ enum Kind : int32_t * Specifies a custom property for a quantified formula given by a * term that is ascribed a user attribute. * + * @note Should only be used as a child of #INST_PATTERN_LIST. + * * - Arity: `n > 0` * - `1:` Term of Kind #CONST_STRING (the keyword of the attribute) * - `2...n:` Terms representing the values of the attribute @@ -4080,11 +4144,11 @@ enum Kind : int32_t */ INST_ATTRIBUTE, /** - * A list of instantiation patterns and/or attributes. + * A list of instantiation patterns, attributes or annotations. * * - Arity: `n > 1` - * - `1..n:` Terms of Kind #INST_PATTERN, #INST_NO_PATTERN, or - * #INST_ATTRIBUTE + * - `1..n:` Terms of Kind #INST_PATTERN, #INST_NO_PATTERN, #INST_POOL, + * #INST_ADD_TO_POOL, #SKOLEM_ADD_TO_POOL, #INST_ATTRIBUTE * * - Create Term of this Kind with: * - Solver::mkTerm(Kind, const std::vector&) const diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 027d7e588..9183c2bf7 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -160,8 +160,8 @@ void Smt2::addStringOperators() { { addOperator(api::STRING_INDEXOF_RE, "str.indexof_re"); addOperator(api::STRING_UPDATE, "str.update"); - addOperator(api::STRING_TOLOWER, "str.tolower"); - addOperator(api::STRING_TOUPPER, "str.toupper"); + addOperator(api::STRING_TO_LOWER, "str.to_lower"); + addOperator(api::STRING_TO_UPPER, "str.to_upper"); addOperator(api::STRING_REV, "str.rev"); // sequence versions addOperator(api::SEQ_CONCAT, "seq.++"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c9125df3d..616c51bab 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1222,8 +1222,8 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::STRING_REPLACE_ALL: return "str.replace_all"; case kind::STRING_REPLACE_RE: return "str.replace_re"; case kind::STRING_REPLACE_RE_ALL: return "str.replace_re_all"; - case kind::STRING_TOLOWER: return "str.tolower"; - case kind::STRING_TOUPPER: return "str.toupper"; + case kind::STRING_TO_LOWER: return "str.to_lower"; + case kind::STRING_TO_UPPER: return "str.to_upper"; case kind::STRING_REV: return "str.rev"; case kind::STRING_PREFIX: return "str.prefixof" ; case kind::STRING_SUFFIX: return "str.suffixof" ; diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index be8e2de5b..96ec58890 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -67,8 +67,8 @@ ExtfSolver::ExtfSolver(Env& env, d_extt.addFunctionKind(kind::STRING_IN_REGEXP); d_extt.addFunctionKind(kind::STRING_LEQ); d_extt.addFunctionKind(kind::STRING_TO_CODE); - d_extt.addFunctionKind(kind::STRING_TOLOWER); - d_extt.addFunctionKind(kind::STRING_TOUPPER); + d_extt.addFunctionKind(kind::STRING_TO_LOWER); + d_extt.addFunctionKind(kind::STRING_TO_UPPER); d_extt.addFunctionKind(kind::STRING_REV); d_extt.addFunctionKind(kind::SEQ_UNIT); d_extt.addFunctionKind(kind::SEQ_NTH); @@ -213,7 +213,7 @@ bool ExtfSolver::doReduction(int effort, Node n) || k == STRING_STOI || k == STRING_REPLACE || k == STRING_REPLACE_ALL || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL || k == STRING_LEQ - || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV) + || k == STRING_TO_LOWER || k == STRING_TO_UPPER || k == STRING_REV) << "Unknown reduction: " << k; std::vector new_nodes; Node res = d_preproc.simplify(n, new_nodes); diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index ff226202b..6ac95bb46 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -34,8 +34,8 @@ operator STRING_ITOS 1 "integer to string" operator STRING_STOI 1 "string to integer (total function)" operator STRING_TO_CODE 1 "string to code, returns the code of the first character of the string if it has length one, -1 otherwise" operator STRING_FROM_CODE 1 "string from code, returns a string containing a single character whose code point matches the argument to this function, empty string if the argument is out-of-bounds" -operator STRING_TOLOWER 1 "string to lowercase conversion" -operator STRING_TOUPPER 1 "string to uppercase conversion" +operator STRING_TO_LOWER 1 "string to lowercase conversion" +operator STRING_TO_UPPER 1 "string to uppercase conversion" operator STRING_REV 1 "string reverse" sort STRING_TYPE \ @@ -187,8 +187,8 @@ typerule STRING_ITOS "SimpleTypeRule" typerule STRING_STOI "SimpleTypeRule" typerule STRING_TO_CODE "SimpleTypeRule" typerule STRING_FROM_CODE "SimpleTypeRule" -typerule STRING_TOUPPER "SimpleTypeRule" -typerule STRING_TOLOWER "SimpleTypeRule" +typerule STRING_TO_UPPER "SimpleTypeRule" +typerule STRING_TO_LOWER "SimpleTypeRule" ### sequence specific operators diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index ce95d193f..3a2cbb900 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -631,10 +631,10 @@ Node SequencesRewriter::rewriteLength(Node node) return returnRewrite(node, retNode, Rewrite::LEN_REPL_INV); } } - else if (nk0 == STRING_TOLOWER || nk0 == STRING_TOUPPER || nk0 == STRING_REV + else if (nk0 == STRING_TO_LOWER || nk0 == STRING_TO_UPPER || nk0 == STRING_REV || nk0 == STRING_UPDATE) { - // len( f( x ) ) == len( x ) where f is tolower, toupper, or rev. + // len( f( x ) ) == len( x ) where f is to_lower, to_upper, or rev. // len( update( x, n, y ) ) = len( x ) Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]); return returnRewrite(node, retNode, Rewrite::LEN_CONV_INV); diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 2ff7598b5..000e2e70c 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -49,7 +49,7 @@ RewriteResponse StringsRewriter::postRewrite(TNode node) { retNode = rewriteStringLeq(node); } - else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER) + else if (nk == STRING_TO_LOWER || nk == STRING_TO_UPPER) { retNode = rewriteStrConvert(node); } @@ -151,7 +151,7 @@ Node StringsRewriter::rewriteIntToStr(Node node) Node StringsRewriter::rewriteStrConvert(Node node) { Kind nk = node.getKind(); - Assert(nk == STRING_TOLOWER || nk == STRING_TOUPPER); + Assert(nk == STRING_TO_LOWER || nk == STRING_TO_UPPER); NodeManager* nm = NodeManager::currentNM(); if (node[0].isConst()) { @@ -162,14 +162,14 @@ Node StringsRewriter::rewriteStrConvert(Node node) // transform it // upper 65 ... 90 // lower 97 ... 122 - if (nk == STRING_TOUPPER) + if (nk == STRING_TO_UPPER) { if (newChar >= 97 && newChar <= 122) { newChar = newChar - 32; } } - else if (nk == STRING_TOLOWER) + else if (nk == STRING_TO_LOWER) { if (newChar >= 65 && newChar <= 90) { @@ -188,21 +188,21 @@ Node StringsRewriter::rewriteStrConvert(Node node) { concatBuilder << nm->mkNode(nk, nc); } - // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 ) + // to_lower( x1 ++ x2 ) --> to_lower( x1 ) ++ to_lower( x2 ) Node retNode = concatBuilder.constructNode(); return returnRewrite(node, retNode, Rewrite::STR_CONV_MINSCOPE_CONCAT); } - else if (node[0].getKind() == STRING_TOLOWER - || node[0].getKind() == STRING_TOUPPER) + else if (node[0].getKind() == STRING_TO_LOWER + || node[0].getKind() == STRING_TO_UPPER) { - // tolower( tolower( x ) ) --> tolower( x ) - // tolower( toupper( x ) ) --> tolower( x ) + // to_lower( to_lower( x ) ) --> to_lower( x ) + // to_lower( toupper( x ) ) --> to_lower( x ) Node retNode = nm->mkNode(nk, node[0][0]); return returnRewrite(node, retNode, Rewrite::STR_CONV_IDEM); } else if (node[0].getKind() == STRING_ITOS) { - // tolower( str.from.int( x ) ) --> str.from.int( x ) + // to_lower( str.from.int( x ) ) --> str.from.int( x ) return returnRewrite(node, node[0], Rewrite::STR_CONV_ITOS); } return node; diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h index 52f1e44d7..0ceaa5a41 100644 --- a/src/theory/strings/strings_rewriter.h +++ b/src/theory/strings/strings_rewriter.h @@ -57,7 +57,7 @@ class StringsRewriter : public SequencesRewriter /** rewrite string convert * * This is the entry point for post-rewriting terms n of the form - * str.tolower( s ) and str.toupper( s ) + * str.to_lower( s ) and str.toupper( s ) * Returns the rewritten form of n. */ Node rewriteStrConvert(Node n); diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 84a290f3c..01e821aba 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -159,7 +159,7 @@ void TermRegistry::preRegisterTerm(TNode n) || k == STRING_STOI || k == STRING_REPLACE || k == STRING_SUBSTR || k == STRING_REPLACE_ALL || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL || k == STRING_CONTAINS || k == STRING_LEQ - || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV + || k == STRING_TO_LOWER || k == STRING_TO_UPPER || k == STRING_REV || k == STRING_UPDATE) { std::stringstream ss; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 7b1facde1..af3d2db22 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -156,8 +156,8 @@ void TheoryStrings::finishInit() d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_ALL, eagerEval); - d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval); - d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_TO_LOWER, eagerEval); + d_equalityEngine->addFunctionKind(kind::STRING_TO_UPPER, eagerEval); d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval); // memberships are not relevant for model building diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index ff17efa0e..8a4bc3dd5 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -849,7 +849,7 @@ Node StringsPreprocess::reduce(Node t, nm->mkNode(ITE, noMatch, k.eqNode(x), nm->mkNode(AND, lemmas))); retNode = k; } - else if (t.getKind() == STRING_TOLOWER || t.getKind() == STRING_TOUPPER) + else if (t.getKind() == STRING_TO_LOWER || t.getKind() == STRING_TO_UPPER) { Node x = t[0]; Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); @@ -864,11 +864,12 @@ Node StringsPreprocess::reduce(Node t, Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one)); Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one)); - Node lb = nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65)); + Node lb = + nm->mkConstInt(Rational(t.getKind() == STRING_TO_UPPER ? 97 : 65)); Node ub = - nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90)); + nm->mkConstInt(Rational(t.getKind() == STRING_TO_UPPER ? 122 : 90)); Node offset = - nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? -32 : 32)); + nm->mkConstInt(Rational(t.getKind() == STRING_TO_UPPER ? -32 : 32)); Node res = nm->mkNode( ITE, diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 9deecc921..75d8dd628 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -349,8 +349,8 @@ void printConcatTrace(std::vector& n, const char* c) bool isStringKind(Kind k) { - return k == STRING_STOI || k == STRING_ITOS || k == STRING_TOLOWER - || k == STRING_TOUPPER || k == STRING_LEQ || k == STRING_LT + return k == STRING_STOI || k == STRING_ITOS || k == STRING_TO_LOWER + || k == STRING_TO_UPPER || k == STRING_LEQ || k == STRING_LT || k == STRING_FROM_CODE || k == STRING_TO_CODE; } diff --git a/test/regress/cli/regress0/strings/parser-syms.cvc.smt2 b/test/regress/cli/regress0/strings/parser-syms.cvc.smt2 index b71360c2c..ce7bc3907 100644 --- a/test/regress/cli/regress0/strings/parser-syms.cvc.smt2 +++ b/test/regress/cli/regress0/strings/parser-syms.cvc.smt2 @@ -4,5 +4,5 @@ (declare-fun x () String) (declare-fun y () String) (assert (= (str.++ (str.rev "abc") "d") x)) -(assert (= (str.++ (str.tolower "ABC") (str.toupper "abc")) y)) +(assert (= (str.++ (str.to_lower "ABC") (str.to_upper "abc")) y)) (check-sat) diff --git a/test/regress/cli/regress0/strings/tolower-rrs.smt2 b/test/regress/cli/regress0/strings/tolower-rrs.smt2 index 217255807..4eb4bce6f 100644 --- a/test/regress/cli/regress0/strings/tolower-rrs.smt2 +++ b/test/regress/cli/regress0/strings/tolower-rrs.smt2 @@ -7,9 +7,9 @@ (declare-fun y () Int) (assert (or -(not (= (str.tolower (str.toupper (str.tolower x))) (str.tolower x))) -(not (= (str.tolower (str.++ x "A")) (str.++ (str.tolower x) "a"))) -(not (= (str.tolower (str.from_int y)) (str.from_int y))) +(not (= (str.to_lower (str.to_upper (str.to_lower x))) (str.to_lower x))) +(not (= (str.to_lower (str.++ x "A")) (str.++ (str.to_lower x) "a"))) +(not (= (str.to_lower (str.from_int y)) (str.from_int y))) )) (check-sat) diff --git a/test/regress/cli/regress0/strings/tolower-simple.smt2 b/test/regress/cli/regress0/strings/tolower-simple.smt2 index 5de5a2447..4252d7d0d 100644 --- a/test/regress/cli/regress0/strings/tolower-simple.smt2 +++ b/test/regress/cli/regress0/strings/tolower-simple.smt2 @@ -5,7 +5,7 @@ (declare-const y String) (declare-const z String) -(assert (= (str.tolower "aBCDef") x)) +(assert (= (str.to_lower "aBCDef") x)) (assert (= x (str.++ y "c" z))) (check-sat) diff --git a/test/regress/cli/regress1/strings/rev-conv1.smt2 b/test/regress/cli/regress1/strings/rev-conv1.smt2 index ca20076cb..9ee103895 100644 --- a/test/regress/cli/regress1/strings/rev-conv1.smt2 +++ b/test/regress/cli/regress1/strings/rev-conv1.smt2 @@ -3,7 +3,7 @@ (set-logic ALL) (set-info :status sat) (declare-fun x () String) -(assert (= (str.rev (str.toupper x)) "CBA")) +(assert (= (str.rev (str.to_upper x)) "CBA")) (assert (not (= x "ABC"))) (assert (not (= x "abc"))) (check-sat) diff --git a/test/regress/cli/regress1/strings/tolower-find.smt2 b/test/regress/cli/regress1/strings/tolower-find.smt2 index 80c797b3e..821812b4f 100644 --- a/test/regress/cli/regress1/strings/tolower-find.smt2 +++ b/test/regress/cli/regress1/strings/tolower-find.smt2 @@ -4,8 +4,8 @@ (declare-const x String) (declare-const y String) -(assert (= (str.tolower x) "abcde")) -(assert (= (str.tolower y) "abcde")) +(assert (= (str.to_lower x) "abcde")) +(assert (= (str.to_lower y) "abcde")) (assert (not (= x "abcde"))) (assert (not (= y "abcde"))) (assert (not (= x y))) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index b31aa9ad1..e32f4a8e9 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -3301,7 +3301,7 @@ TEST_F(TestApiBlackSolver, proj_issue422) Term t234 = slv.mkTerm(Kind::SET_CHOOSE, {t212}); Term t250 = slv.mkTerm(Kind::STRING_REPLACE_RE_ALL, {t1, t92, t1}); Term t259 = slv.mkTerm(Kind::STRING_REPLACE_ALL, {t234, t234, t250}); - Term t263 = slv.mkTerm(Kind::STRING_TOLOWER, {t259}); + Term t263 = slv.mkTerm(Kind::STRING_TO_LOWER, {t259}); Term t272 = slv.mkTerm(Kind::BITVECTOR_SDIV, {t211, t66}); Term t276 = slv.mkTerm(slv.mkOp(Kind::BITVECTOR_ZERO_EXTEND, {71}), {t272}); Term t288 = slv.mkTerm(Kind::EQUAL, {t263, t1}); -- 2.30.2