class Z3::BitvecSort

# 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

# 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

# File lib/z3/sort/bitvec_sort.rb, line 8
def expr_class
  BitvecExpr
end

# 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

# File lib/z3/sort/bitvec_sort.rb, line 28
def inspect
  "BitvecSort(#{size})"
end

# File lib/z3/sort/bitvec_sort.rb, line 20
def size
  LowLevel.get_bv_sort_size(self)
end

# File lib/z3/sort/bitvec_sort.rb, line 24
def to_s
  "Bitvec(#{size})"
end