class
Z3::StringExpr
- Z3::StringExpr
- Reference
- Object
Overview
This reads like Crystal's String - see SeqExpr for why the two don't share a hierarchy even though Z3 models a String as a Seq(Char).
Where Crystal and SMT-LIB disagree, Crystal wins: #includes? rather than
contains?, #sub / #gsub rather than replace / replace_all, and the
receiver back in front of #starts_with?.
Where Crystal answers nil there's nothing to answer with, because every one of
these is a subexpression - s[i] can appear as s[i] + "!", or under an #==, or
buried in a term a model hands back - so it has to denote a String, and no String
is nil. Those return whatever Z3 returns, and the method comments say what it is.
Included Modules
Defined in:
z3/string_expr.crConstructors
Instance Method Summary
-
#!=(other)
Returns
trueif this object is not equal to other. -
#*(count : Int)
Crystal String#* repeats.
-
#+(other)
Crystal String#+ is concatenation, and so is
str.++ -
#<(other)
str.</str.<=are lexicographic, and have nothing to do with#== - #<=(other)
-
#==(other)
Returns
false(other can only be aValuehere). - #>(other)
- #>=(other)
- #[](offset : IntExpr | Int, len : IntExpr | Int)
-
#[](index : IntExpr | Int)
Crystal String#[].
- #[](range : Range)
- #const?
- #empty?
- #ends_with?(suffix : StringExpr | String)
- #gsub(pattern : StringExpr | String, replacement : StringExpr | String)
-
#includes?(substring : StringExpr | String)
Crystal String#includes? - a substring, not a character
-
#index(substring : StringExpr | String, offset : IntExpr | Int = 0)
Crystal String#index.
- #inspect(io)
-
#length
str.lenandseq.lenare one Z3 operation, so SeqExpr#length is the same call -
#rindex(substring : StringExpr | String)
Crystal String#rindex.
-
#same_term?(other : AnyExpr)
Whether this is the same term as
other. - #simplify
- #size
- #sort
-
#starts_with?(prefix : StringExpr | String)
Z3's
str.prefixoftakes the prefix first and the string second, the opposite way round from Crystal's String#starts_with? -
#sub(pattern : StringExpr | String, replacement : StringExpr | String)
Crystal String#sub and #gsub, split the same way:
str.replacereplaces the first occurrence,str.replace_allevery one. -
#to_code
The code point of a one character string, as a Z3 Int, or -1 for a string of any other length.
-
#to_i
Crystal String#to_i, so this is the symbolic
str.to_int- not IntExpr#to_i, which goes the other way and gives a Crystal Int32. - #to_s(io)
- #to_unsafe : LibZ3::Ast
-
#value : String
Every sort which can hand back a Crystal object spells it #value.
Constructor Detail
Instance Method Detail
Returns true if this object is not equal to other.
By default this method is implemented as !(self == other)
so there's no need to override this unless there's a more efficient
way to do it.
Crystal String#* repeats. Z3 has no repetition operator, so it's Crystal side concatenation, and the count has to be a Crystal Integer rather than an IntExpr.
Returns false (other can only be a Value here).
Crystal String#[]. s[i] is a one character String (str.at), s[i, len] and
s[range] are substrings (str.substr).
An index is an offset, and that's the whole of it - a negative one is not counted
from the end the way Crystal's is. Only a literal could ever be recognized as
negative, and s[-1] meaning the last character while s[i] with i == -1 means
something else is worse than not emulating it at all: an index has to mean the
same thing however it's spelled. So a negative index is simply out of range, and
out of range is whatever Z3 says, which is "". Counting from the end is
s[s.length - 1], which works for a symbolic offset too.
Crystal String#includes? - a substring, not a character
Crystal String#index. This denotes an Int, so there's no nil available for it to
be when there's no match - str.indexof answers -1, and that's what comes back.
Crystal String#rindex. Z3's seq.last_indexof takes no offset, so neither does this.
Whether this is the same term as other. Z3 hash-conses its expressions, so
this is structural equality - Z3.int("a") + 1 built twice is one term. It is
a named method rather than #== because #== builds a Z3 expression instead of
answering a Crystal Bool - see the Limitations section of the README.
Z3's str.prefixof takes the prefix first and the string second, the opposite
way round from Crystal's String#starts_with?
Crystal String#sub and #gsub, split the same way: str.replace replaces the first
occurrence, str.replace_all every one. We have no regular expressions yet, so
the pattern is a String, matched unanchored exactly as Crystal's String one is.
The code point of a one character string, as a Z3 Int, or -1 for a string of any other length. StringSort.from_code is this backwards.
Crystal String#to_i, so this is the symbolic str.to_int - not IntExpr#to_i,
which goes the other way and gives a Crystal Int32. #value is the one that gives
a Crystal object back.
str.to_int isn't quite Crystal's String#to_i, though: it takes a non-negative
run of digits and answers -1 for anything else, where Crystal takes a sign, parses
a digit prefix and raises on failure. This returns what Z3 returns.
Every sort which can hand back a Crystal object spells it #value. Deliberately not #to_s - that's the printed form of any AST, and it has to work on all of them.