class

Z3::SeqSort

Inherits Reference < Object

Constructors

new(element_sort : CharSort.class)

Z3 has no String sort of its own, a String is just a Seq(Char) - so Seq(Char) has to come back as StringSort, or we'd have two Crystal classes for one Z3 sort

Source

new(element_sort : AnySort)

Source

Instance methods

==(other : SeqSort)

Z3 hash-conses its sorts, so two Seq sorts over the same element sort are one sort

Source

[](expr : SeqExpr)

Source

[](values : Array)

Z3 has no sequence literals, a sequence value is a concatenation of one element sequences - and it rejects a concatenation of fewer than two of them

Source

cast(value) : SeqExpr

Source

element_sort

Source

empty

Source

from_ast(ast : LibZ3::Ast) : SeqExpr

Source

to_s(io)

Source

to_unsafe

Source

unit(value)

The one element sequence holding value, which is what every sequence value is built out of

Source

var(name : String)

Source