class Z3::RoundingModeSort
Public Class Methods
Source
# File lib/z3/sort/rounding_mode_sort.rb, line 3 def initialize super LowLevel.mk_fpa_rounding_mode_sort end
Calls superclass method
Public Instance Methods
Source
# File lib/z3/sort/rounding_mode_sort.rb, line 7 def expr_class RoundingModeExpr end
Source
# File lib/z3/sort/rounding_mode_sort.rb, line 15 def inspect "RoundingModeSort" end
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
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
Source
# File lib/z3/sort/rounding_mode_sort.rb, line 31 def towards_negative RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_negative, self) end
Source
# File lib/z3/sort/rounding_mode_sort.rb, line 35 def towards_positive RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_positive, self) end
Source
# File lib/z3/sort/rounding_mode_sort.rb, line 27 def towards_zero RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_zero, self) end