class
Z3::BitvecSort
- Z3::BitvecSort
- Reference
- Object
Defined in:
z3/bitvec_sort.crConstructors
Instance Method Summary
-
#==(other : BitvecSort)
Z3 hash-conses its sorts, so two Bitvec sorts of the same size are one sort
- #[](expr : BitvecExpr)
- #[](v : Int)
- #cast(value) : BitvecExpr
- #from_ast(ast : LibZ3::Ast) : BitvecExpr
- #size : UInt32
- #to_s(io)
- #to_unsafe : LibZ3::Sort
- #var(name : String)
Constructor Detail
Instance Method Detail
def ==(other : BitvecSort)
#
Z3 hash-conses its sorts, so two Bitvec sorts of the same size are one sort