Z3::StringExpr
Inherits Z3::RangeIndexing < Reference < Object
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.
Constructors
Instance methods
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.
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.