class Z3::RoundingModeSort

# File lib/z3/sort/rounding_mode_sort.rb, line 3
def initialize
  super LowLevel.mk_fpa_rounding_mode_sort
end

# File lib/z3/sort/rounding_mode_sort.rb, line 7
def expr_class
  RoundingModeExpr
end

# File lib/z3/sort/rounding_mode_sort.rb, line 15
def inspect
  "RoundingModeSort"
end

# 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

# 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

# File lib/z3/sort/rounding_mode_sort.rb, line 11
def to_s
  "RoundingMode"
end

# File lib/z3/sort/rounding_mode_sort.rb, line 31
def towards_negative
  RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_negative, self)
end

# File lib/z3/sort/rounding_mode_sort.rb, line 35
def towards_positive
  RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_positive, self)
end

# File lib/z3/sort/rounding_mode_sort.rb, line 27
def towards_zero
  RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_zero, self)
end