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, #func_decl, #sexpr, #simplify

Constructor Details

#initialize(n) ⇒ BitvecSort

Returns a new instance of BitvecSort.



3
4
5
 
# File 'lib/z3/sort/bitvec_sort.rb', line 3

def initialize(n)
  super LowLevel.mk_bv_sort(n)
end

Instance Method Details

#>(other) ⇒ Object

Raises:

  • (ArgumentError) 


31
32
33
34
35
36
 
# File 'lib/z3/sort/bitvec_sort.rb', line 31

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 



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

def expr_class
  BitvecExpr
end

#from_const(val) ⇒ Object 



11
12
13
14
15
16
17
 
# File 'lib/z3/sort/bitvec_sort.rb', line 11

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 



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

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

#size ⇒ Object 



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

def size
  LowLevel.get_bv_sort_size(self)
end

#to_s ⇒ Object 



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

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