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.
Instance Method Details
#>(other) ⇒ Object
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) return true if other.is_a?(RealSort) false
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
#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
|
#to_s ⇒ Object
62
63
64
|
# File 'lib/z3/sort/float_sort.rb', line 62
def to_s
"Float(#{ebits}, #{sbits})"
end
|