Z3::SeqExpr
Inherits Z3::RangeIndexing < Reference < Object
Z3 has no String sort of its own - a String is a Seq(Char), and str.++ is the
same operation as seq.++. The Exprs still don't share a hierarchy, because the
Crystal side of them doesn't: a SeqExpr should read like a Crystal Array and a
StringExpr like a Crystal String, and those two have no common ancestor either.
Where a seq and a string operation really are one Z3 operation, they share the
API call, not a superclass.
That split is what settles the element-versus-subsequence question. Every Z3 seq operation takes a subsequence, but Crystal's Array#includes? / #index take an element, and Crystal wins - as it does everywhere the two disagree: a bare element is wrapped into a one element sequence, while a SeqExpr of this very sort or a Crystal Array is taken as the subsequence it already is.
A Seq only knows its element sort at runtime, so everything which hands back an
element hands back an AnyExpr - xs[0].as(IntExpr) is how you get back to a
sort Crystal can typecheck.
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 Array#* repeats. Only the Integer form - Array#*(String) is #join, and there's no joining a sequence of arbitrary element sort into a String.
Crystal Array#[]. xs[i] is the element (seq.nth), xs[i, len] and xs[range]
are subsequences (seq.extract).
An index is an offset, and a negative one is not counted from the end the way
Crystal's is - see StringExpr#[] for why. Counting from the end is
xs[xs.length - 1], which is what #last does. Out of range is whatever Z3 says: a
subsequence is empty, and an element is left unspecified, so an out of range
xs[i] is a term the solver may pick any value for. It denotes an element, and no
element is nil.
The elements of a sequence value, each an expression of the element sort. There is
no #value, the way every other sort has one: the element sort is only known at
runtime, so the best a Crystal Array could be is an Array of unions - call #value
on the elements you want instead, as in xs.elements.map(&.as(IntExpr).value).
Crystal Array#includes? takes an element, so that's what this expects - pass a SeqExpr of this sort, or a Crystal Array, to ask about a subsequence instead
Crystal Array#index. This denotes an Int, so there's no nil available for it to
be when there's no match - seq.indexof answers -1, and that's what comes back. It
also takes a starting offset, which Crystal's Array#index doesn't.
Crystal Array#rindex. Z3's seq.last_indexof takes no offset, so neither does
this - and as of Z3 4.16 it builds fine but answers an out of range value for
every sequence of non-characters, so only StringExpr#rindex is any use yet.
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 seq.prefixof takes the prefix first and the sequence second. Crystal's Array
has no #starts_with?, so String's spelling is reused.
Crystal's Array has nothing like these, so they keep String's names along with String's first-one versus every-one split