class Z3::RealSort

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

# File lib/z3/sort/real_sort.rb, line 29
def >(other)
  raise ArgumentError unless other.is_a?(Sort)
  other.is_a?(IntSort)
end

# File lib/z3/sort/real_sort.rb, line 7
def expr_class
  RealExpr
end

# 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

# 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