class Z3::IntExpr
Public Class Methods
Mod(a, b)
click to toggle source
# File lib/z3/expr/int_expr.rb, line 36 def Mod(a, b) a, b = coerce_to_same_int_sort(a, b) a.sort.new(LowLevel.mk_mod(a, b)) end
Rem(a, b)
click to toggle source
# File lib/z3/expr/int_expr.rb, line 41 def Rem(a, b) a, b = coerce_to_same_int_sort(a, b) a.sort.new(LowLevel.mk_rem(a, b)) end
coerce_to_same_int_sort(*args)
click to toggle source
# File lib/z3/expr/int_expr.rb, line 30 def coerce_to_same_int_sort(*args) args = coerce_to_same_sort(*args) raise Z3::Exception, "Int value expected" unless args[0].is_a?(IntExpr) args end
Public Instance Methods
%(other)
click to toggle source
# File lib/z3/expr/int_expr.rb, line 7 def %(other) IntExpr.Mod(self, other) end
mod(other)
click to toggle source
# File lib/z3/expr/int_expr.rb, line 3 def mod(other) IntExpr.Mod(self, other) end
rem(other)
click to toggle source
# File lib/z3/expr/int_expr.rb, line 11 def rem(other) IntExpr.Rem(self, other) end
to_i()
click to toggle source
# File lib/z3/expr/int_expr.rb, line 15 def to_i if ast_kind == :numeral LowLevel.get_numeral_string(self).to_i else obj = simplify if obj.ast_kind == :numeral LowLevel.get_numeral_string(obj).to_i else raise Z3::Exception, "Can't convert expression #{to_s} to Integer" end end end