class Z3::BitvecSort
Public Class Methods
new(n)
click to toggle source
Calls superclass method
# 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
Public Instance Methods
>(other)
click to toggle 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
expr_class()
click to toggle source
# File lib/z3/sort/bitvec_sort.rb, line 8 def expr_class BitvecExpr end
from_const(val)
click to toggle 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
inspect()
click to toggle source
# File lib/z3/sort/bitvec_sort.rb, line 28 def inspect "BitvecSort(#{size})" end
size()
click to toggle source
# File lib/z3/sort/bitvec_sort.rb, line 20 def size LowLevel.get_bv_sort_size(self) end
to_s()
click to toggle source
# File lib/z3/sort/bitvec_sort.rb, line 24 def to_s "Bitvec(#{size})" end