class Z3::IntExpr

# File lib/z3/expr/int_expr.rb, line 54
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 59
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 48
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 19
def divisible_by?(other)
  BoolSort.new.new(LowLevel.mk_divides(IntSort.new.cast(other), self))
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 23
def to_bv(size)
  BitvecSort.new(size).new(LowLevel.mk_int2bv(size, self))
end

# File lib/z3/expr/int_expr.rb, line 27
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} into Integer"
    end
  end
end