class Z3::RealSort
Public Class Methods
new()
click to toggle source
Calls superclass method
# File lib/z3/sort/real_sort.rb, line 3 def initialize super LowLevel.mk_real_sort end
Public Instance Methods
>(other)
click to toggle source
# 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()
click to toggle source
# File lib/z3/sort/real_sort.rb, line 7 def expr_class RealExpr end
from_const(val)
click to toggle source
# 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)
click to toggle source
# 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