class Z3::ArithExpr

# File lib/z3/expr/arith_expr.rb, line 79
def Div(a,b)
  a, b = coerce_to_same_arith_sort(a, b)
  a.sort.new(LowLevel.mk_div(a, b))
end

# File lib/z3/expr/arith_expr.rb, line 84
def Power(a, b)
  # Wait, is this even legitimate that it's I**I and R**R?
  a, b = coerce_to_same_arith_sort(a, b)
  a.sort.new(LowLevel.mk_power(a, b))
end

# File lib/z3/expr/arith_expr.rb, line 73
def coerce_to_same_arith_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Int or Real value expected" unless args[0].is_a?(IntExpr) or args[0].is_a?(RealExpr)
  args
end

# File lib/z3/expr/arith_expr.rb, line 11
def *(other)
  Expr.Mul(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 19
def **(other)
  ArithExpr.Power(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 3
def +(other)
  Expr.Add(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 7
def -(other)
  Expr.Sub(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 39
def -@
  sort.new(LowLevel.mk_unary_minus(self))
end

# File lib/z3/expr/arith_expr.rb, line 15
def /(other)
  ArithExpr.Div(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 35
def <(other)
  Expr.Lt(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 31
def <=(other)
  Expr.Le(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 23
def >(other)
  Expr.Gt(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 27
def >=(other)
  Expr.Ge(self, other)
end

# File lib/z3/expr/arith_expr.rb, line 59
def abs
  (self < 0).ite(-self, self)
end

# File lib/z3/expr/arith_expr.rb, line 66
def coerce(other)
  other_sort = Expr.sort_for_const(other)
  max_sort = [sort, other_sort].max
  [max_sort.from_const(other), max_sort.from_value(self)]
end

# File lib/z3/expr/arith_expr.rb, line 55
def negative?
  self < 0
end

# File lib/z3/expr/arith_expr.rb, line 47
def nonzero?
  self != 0
end

# File lib/z3/expr/arith_expr.rb, line 51
def positive?
  self > 0
end

# File lib/z3/expr/arith_expr.rb, line 43
def zero?
  self == 0
end