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 Z3::Exception, "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) 


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

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 



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

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
46
47
48
49
50
51
52
53
 
# File 'lib/z3/sort/float_sort.rb', line 34

def from_const(val)
  if val.is_a?(Integer)
    val_f = val.to_f
    raise Z3::Exception, "Out of range" unless val_f == val
    val = val_f
  elsif !val.is_a?(Float)
    raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
  end

  # A Ruby Float is a double, so this is exact for the double sort
  double = FloatSort.new(:double)
  return new(LowLevel.mk_fpa_numeral_double(val, self)) if self == double

  # For every other sort the value has to be rounded, and Z3_mk_fpa_numeral_double
  # gets that wrong - it returns NaN on overflow and misencodes denormals. Build the
  # exact double instead, and let Z3 round it to this sort the way IEEE says to.
  exact = FloatExpr.new(LowLevel.mk_fpa_numeral_double(val, double), double)
  rounding_mode = RoundingModeSort.new.nearest_ties_even
  new(LowLevel.mk_fpa_to_fp_float(rounding_mode, exact, self)).simplify
end

#inspect ⇒ Object 



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

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

#nan ⇒ Object 



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

def nan
  new LowLevel.mk_fpa_nan(self)
end

#negative_infinity ⇒ Object 



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

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

#negative_zero ⇒ Object 



94
95
96
 
# File 'lib/z3/sort/float_sort.rb', line 94

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

#positive_infinity ⇒ Object 



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

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

#positive_zero ⇒ Object 



90
91
92
 
# File 'lib/z3/sort/float_sort.rb', line 90

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

#sbits ⇒ Object 



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

def sbits
  LowLevel.fpa_get_sbits(self)
end

#to_s ⇒ Object 



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

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