class
Z3::SeqSort
- Z3::SeqSort
- Reference
- Object
Defined in:
z3/seq_sort.crConstructors
-
.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
- .new(element_sort : AnySort)
Instance Method Summary
-
#==(other : SeqSort)
Z3 hash-conses its sorts, so two Seq sorts over the same element sort are one sort
- #[](expr : SeqExpr)
-
#[](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
- #cast(value) : SeqExpr
- #element_sort : Z3::BitvecSort | Z3::BoolSort.class | Z3::CharSort.class | Z3::IntSort.class | Z3::RealSort.class | Z3::SeqSort | Z3::StringSort.class
- #empty
- #from_ast(ast : LibZ3::Ast) : SeqExpr
- #to_s(io)
- #to_unsafe : LibZ3::Sort
-
#unit(value)
The one element sequence holding
value, which is what every sequence value is built out of - #var(name : String)
Constructor Detail
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
Instance Method Detail
Z3 hash-conses its sorts, so two Seq sorts over the same element sort are one sort
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
The one element sequence holding value, which is what every sequence value is
built out of