class Z3::BitvecSort
Public Class Methods
Source
# File lib/z3/sort/bitvec_sort.rb, line 3 def initialize(n) raise Z3::Exception, "Bitvec width must be positive" unless n >= 1 super LowLevel.mk_bv_sort(n) end
Calls superclass method
Public Instance Methods
Source
# File lib/z3/sort/bitvec_sort.rb, line 32 def >(other) raise ArgumentError unless other.is_a?(Sort) return true if other.is_a?(IntSort) # This is nasty... return true if other.is_a?(BitvecSort) and size > other.size false end
Source
# File lib/z3/sort/bitvec_sort.rb, line 12 def from_const(val) if val.is_a?(Integer) new LowLevel.mk_numeral(val.to_s, self) else raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}" end end
Source
# File lib/z3/sort/bitvec_sort.rb, line 20 def size LowLevel.get_bv_sort_size(self) end