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

#initialize ⇒ RoundingModeSort

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_class ⇒ Object 



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

def expr_class
  RoundingModeExpr
end

#inspect ⇒ Object 



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

def inspect
  "RoundingModeSort"
end

#nearest_ties_away ⇒ Object 



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_even ⇒ Object 



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_s ⇒ Object 



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

def to_s
  "RoundingMode"
end

#towards_negative ⇒ Object 



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_positive ⇒ Object 



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_zero ⇒ Object 



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