class Z3::RoundingModeSort
Public Class Methods
new()
click to toggle source
Calls superclass method
# File lib/z3/sort/rounding_mode_sort.rb, line 3 def initialize super LowLevel.mk_fpa_rounding_mode_sort end
Public Instance Methods
expr_class()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 7 def expr_class RoundingModeExpr end
inspect()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 15 def inspect "RoundingModeSort" end
nearest_ties_away()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 19 def nearest_ties_away RoundingModeExpr.new(LowLevel.mk_fpa_round_nearest_ties_to_away, self) end
nearest_ties_even()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 23 def nearest_ties_even RoundingModeExpr.new(LowLevel.mk_fpa_round_nearest_ties_to_even, self) end
to_s()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 11 def to_s "RoundingMode" end
towards_negative()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 31 def towards_negative RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_negative, self) end
towards_positive()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 35 def towards_positive RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_positive, self) end
towards_zero()
click to toggle source
# File lib/z3/sort/rounding_mode_sort.rb, line 27 def towards_zero RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_zero, self) end