Class: Z3::BitvecSort

Inherits:
Sort show all
Defined in:
lib/z3/sort/bitvec_sort.rb

Instance Attribute Summary

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from Sort

#<, #<=, #<=>, #==, #>=, #cast, #eql?, from_pointer, #from_value, #hash, #new, #value_class, #var

Methods inherited from AST

#arguments, #ast_kind, #eql?, #func_decl, #hash, #sexpr, #simplify

Constructor Details

#initialize(n) ⇒ BitvecSort

Returns a new instance of BitvecSort.

Raises:



3
4
5
6
 
# 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

Instance Method Details

#>(other) ⇒ Object

Raises:

  • (ArgumentError) 


32
33
34
35
36
37
 
# 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 ⇒ Object 



8
9
10
 
# File 'lib/z3/sort/bitvec_sort.rb', line 8

def expr_class
  BitvecExpr
end

#from_const(val) ⇒ Object 



12
13
14
15
16
17
18
 
# 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 ⇒ Object 



28
29
30
 
# File 'lib/z3/sort/bitvec_sort.rb', line 28

def inspect
  "BitvecSort(#{size})"
end

#size ⇒ Object 



20
21
22
 
# File 'lib/z3/sort/bitvec_sort.rb', line 20

def size
  LowLevel.get_bv_sort_size(self)
end

#to_s ⇒ Object 



24
25
26
 
# File 'lib/z3/sort/bitvec_sort.rb', line 24

def to_s
  "Bitvec(#{size})"
end