class Z3::SeqExpr

Overview

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.

Included Modules

Defined in:

z3/seq_expr.cr

Constructors

Instance Method Summary

Constructor Detail

def self.new(expr : LibZ3::Ast, sort : SeqSort) #

[View source]

Instance Method Detail

def !=(other) #
Description copied from class Object

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.


[View source]
def *(count : Int) #

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.


[View source]
def +(other) #

Crystal Array#+ is concatenation, and so is seq.++


[View source]
def ==(other) #
Description copied from class Reference

Returns false (other can only be a Value here).


[View source]
def [](offset : IntExpr | Int, len : IntExpr | Int) #

[View source]
def [](index : IntExpr | Int) : AnyExpr #

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.


[View source]
def [](range : Range) #

[View source]
def at(index : IntExpr | Int) #

Crystal Array#at - the element, same as xs[i]


[View source]
def element_sort #

[View source]
def elements : Array(AnyExpr) #

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).


[View source]
def empty? #

[View source]
def ends_with?(element_or_subsequence) #

[View source]
def first(n : IntExpr | Int) #

[View source]
def first #

[View source]
def gsub(pattern, replacement) #

[View source]
def includes?(element_or_subsequence) #

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


[View source]
def index(element_or_subsequence, offset : IntExpr | Int = 0) #

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.


[View source]
def inspect(io) #

[View source]
def last(n : IntExpr | Int) #

[View source]
def last #

[View source]
def length #

Crystal Array has both #size and #length, so this has both too


[View source]
def rindex(element_or_subsequence) #

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.


[View source]
def same_term?(other : AnyExpr) #

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.


[View source]
def simplify #

[View source]
def size #

[View source]
def sort : Z3::SeqSort #

[View source]
def starts_with?(element_or_subsequence) #

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.


[View source]
def sub(pattern, replacement) #

Crystal's Array has nothing like these, so they keep String's names along with String's first-one versus every-one split


[View source]
def to_s(io) #

[View source]
def to_unsafe : LibZ3::Ast #

[View source]