Class: Z3::RealSort

Inherits:
Sort show all
Defined in:
lib/z3/sort/real_sort.rb

Instance Attribute Summary

Attributes inherited from AST

#_ast

Instance Method Summary collapse

Methods inherited from Sort

#<, #<=, #<=>, #==, #>=, #cast, #eql?, from_pointer, #hash, #inspect, #new, #to_s, #value_class, #var

Methods inherited from AST

#arguments, #ast_kind, #func_decl, #sexpr, #simplify, #to_s

Constructor Details

#initialize ⇒ RealSort

Returns a new instance of RealSort.



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

def initialize
  super LowLevel.mk_real_sort
end

Instance Method Details

#>(other) ⇒ Object

Raises:

  • (ArgumentError) 


29
30
31
32
 
# File 'lib/z3/sort/real_sort.rb', line 29

def >(other)
  raise ArgumentError unless other.is_a?(Sort)
  other.is_a?(IntSort)
end

#expr_class ⇒ Object 



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

def expr_class
  RealExpr
end

#from_const(val) ⇒ Object 



11
12
13
14
15
16
17
 
# File 'lib/z3/sort/real_sort.rb', line 11

def from_const(val)
  if val.is_a?(Integer) or (val.is_a?(Float) and val.finite?) or val.is_a?(Rational)
    new LowLevel.mk_numeral(val.to_s, self)
  else
    raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
  end
end

#from_value(val) ⇒ Object 



19
20
21
22
23
24
25
26
27
 
# File 'lib/z3/sort/real_sort.rb', line 19

def from_value(val)
  if val.is_a?(IntExpr)
    new LowLevel.mk_int2real(val)
  elsif val.is_a?(RealExpr)
    val
  else
    raise Z3::Exception, "Cannot convert #{val.class} to #{self.class}"
  end
end