Class: Z3::FloatSort

Inherits:
Sort show all
Defined in:
lib/z3/sort/float_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(e, s = nil) ⇒ FloatSort

Returns a new instance of FloatSort.



3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
 
# File 'lib/z3/sort/float_sort.rb', line 3

def initialize(e, s=nil)
  if s.nil?
    case e
    when 16
      super LowLevel.mk_fpa_sort_16
    when 32
      super LowLevel.mk_fpa_sort_32
    when 64
      super LowLevel.mk_fpa_sort_64
    when 128
      super LowLevel.mk_fpa_sort_128
    when :half
      super LowLevel.mk_fpa_sort_half
    when :single
      super LowLevel.mk_fpa_sort_single
    when :double
      super LowLevel.mk_fpa_sort_double
    when :quadruple
      super LowLevel.mk_fpa_sort_quadruple
    else
      raise "Unknown float type #{e}, use FloatSort.new(exponent_bits, significant_bits)"
    end
  else
    super LowLevel.mk_fpa_sort(e, s)
  end
end

Instance Method Details

#>(other) ⇒ Object

Raises:

  • (ArgumentError) 


47
48
49
50
51
52
 
# File 'lib/z3/sort/float_sort.rb', line 47

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?(RealSort) # This is nasty...
  false
end

#ebits ⇒ Object 



54
55
56
 
# File 'lib/z3/sort/float_sort.rb', line 54

def ebits
  LowLevel.fpa_get_ebits(self)
end

#expr_class ⇒ Object 



30
31
32
 
# File 'lib/z3/sort/float_sort.rb', line 30

def expr_class
  FloatExpr
end

#from_const(val) ⇒ Object 



34
35
36
37
38
39
40
41
42
43
44
45
 
# File 'lib/z3/sort/float_sort.rb', line 34

def from_const(val)
  if val.is_a?(Float)
    new LowLevel.mk_fpa_numeral_double(val, self)
  elsif val.is_a?(Integer)
    val_f = val.to_f
    # FIXME, there are other constructors
    raise Z3::Exception, "Out of range" unless val_f == val
    new LowLevel.mk_fpa_numeral_double(val_f, self)
  else
    raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
  end
end

#inspect ⇒ Object 



66
67
68
 
# File 'lib/z3/sort/float_sort.rb', line 66

def inspect
  "FloatSort(#{ebits}, #{sbits})"
end

#nan ⇒ Object 



70
71
72
 
# File 'lib/z3/sort/float_sort.rb', line 70

def nan
  new LowLevel.mk_fpa_nan(self)
end

#negative_infinity ⇒ Object 



78
79
80
 
# File 'lib/z3/sort/float_sort.rb', line 78

def negative_infinity
  new LowLevel.mk_fpa_inf(self, true)
end

#negative_zero ⇒ Object 



86
87
88
 
# File 'lib/z3/sort/float_sort.rb', line 86

def negative_zero
  new LowLevel.mk_fpa_zero(self, true)
end

#positive_infinity ⇒ Object 



74
75
76
 
# File 'lib/z3/sort/float_sort.rb', line 74

def positive_infinity
  new LowLevel.mk_fpa_inf(self, false)
end

#positive_zero ⇒ Object 



82
83
84
 
# File 'lib/z3/sort/float_sort.rb', line 82

def positive_zero
  new LowLevel.mk_fpa_zero(self, false)
end

#sbits ⇒ Object 



58
59
60
 
# File 'lib/z3/sort/float_sort.rb', line 58

def sbits
  LowLevel.fpa_get_sbits(self)
end

#to_s ⇒ Object 



62
63
64
 
# File 'lib/z3/sort/float_sort.rb', line 62

def to_s
  "Float(#{ebits}, #{sbits})"
end