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