Class: Z3::RoundingModeSort

Inherits:
Sort
  • Object
show all
Defined in:
lib/z3/sort/rounding_mode_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

#initializeRoundingModeSort

Returns a new instance of RoundingModeSort.



3
4
5
# File 'lib/z3/sort/rounding_mode_sort.rb', line 3

def initialize
  super LowLevel.mk_fpa_rounding_mode_sort
end

Instance Method Details

#expr_classObject



7
8
9
# File 'lib/z3/sort/rounding_mode_sort.rb', line 7

def expr_class
  RoundingModeExpr
end

#inspectObject



15
16
17
# File 'lib/z3/sort/rounding_mode_sort.rb', line 15

def inspect
  "RoundingModeSort"
end

#nearest_ties_awayObject



19
20
21
# 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_evenObject



23
24
25
# 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_sObject



11
12
13
# File 'lib/z3/sort/rounding_mode_sort.rb', line 11

def to_s
  "RoundingMode"
end

#towards_negativeObject



31
32
33
# File 'lib/z3/sort/rounding_mode_sort.rb', line 31

def towards_negative
  RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_negative, self)
end

#towards_positiveObject



35
36
37
# File 'lib/z3/sort/rounding_mode_sort.rb', line 35

def towards_positive
  RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_positive, self)
end

#towards_zeroObject



27
28
29
# File 'lib/z3/sort/rounding_mode_sort.rb', line 27

def towards_zero
  RoundingModeExpr.new(LowLevel.mk_fpa_round_toward_zero, self)
end