class Z3::IntExpr

# 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

# 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

# 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

# File lib/z3/expr/int_expr.rb, line 7
def %(other)
  IntExpr.Mod(self, other)
end

# File lib/z3/expr/int_expr.rb, line 3
def mod(other)
  IntExpr.Mod(self, other)
end

# File lib/z3/expr/int_expr.rb, line 11
def rem(other)
  IntExpr.Rem(self, other)
end

# 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