Also renames str.tolower -> str.to_lower, str.toupper -> str.to_upper.
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
; str.replaceall
; str.replace_re
; str.replace_re_all
- ; str.tolower
- ; str.toupper
+ ; str.to_lower
+ ; str.to_upper
; str.rev
; str.leq
))))))))
(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)
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),
{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},
/**
* 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
* @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,
* 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<Term>&) const
- * - Solver::mkTerm(const Op&, const std::vector<Term>&) const
- *
- * - Create Op of this kind with:
- * - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
+ * - Solver::mkCardinalityConstraint(const Sort&, uint32_t) const
*/
CARDINALITY_CONSTRAINT,
/**
*/
INTS_DIVISION,
/**
- * Integer modulus, modulus by `0` undefined.
+ * Integer modulus, modulus by 0 undefined.
*
* - Arity: `2`
* - `1:` Term of Sort Int
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
*
* - 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<Term>&) const
* 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<Term>&) const
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
*/
- STRING_TOLOWER,
+ STRING_TO_LOWER,
/**
* String to upper case.
*
* - Create Op of this kind with:
* - Solver::mkOp(Kind, const std::vector<uint32_t>&) const
*/
- STRING_TOUPPER,
+ STRING_TO_UPPER,
/**
* String reverse.
*
* 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
*
* 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
*
*/
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<Term>&) 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
/**
* 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<Term>&) const
/**
* 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<Term>&) const
* 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
*/
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<Term>&) const
{
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.++");
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" ;
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);
|| 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<Node> new_nodes;
Node res = d_preproc.simplify(n, new_nodes);
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 \
typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
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_TO_UPPER "SimpleTypeRule<RString, AString>"
+typerule STRING_TO_LOWER "SimpleTypeRule<RString, AString>"
### sequence specific operators
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);
{
retNode = rewriteStringLeq(node);
}
- else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER)
+ else if (nk == STRING_TO_LOWER || nk == STRING_TO_UPPER)
{
retNode = rewriteStrConvert(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())
{
// 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)
{
{
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;
/** 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);
|| 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;
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
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");
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,
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;
}
(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)
(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)
(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)
(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)
(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)))
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});
projects / cvc5.git / commitdiff