class Z3::Expr

# File lib/z3/expr/expr.rb, line 152
def Add(*args)
  raise Z3::Exception if args.empty?
  args = coerce_to_same_sort(*args)
  case args[0]
  when ArithExpr
    args[0].sort.new(LowLevel.mk_add(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(LowLevel.mk_bvadd(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Int/Real/Bitvec"
  end
end

# File lib/z3/expr/expr.rb, line 108
def And(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when BoolExpr
    BoolSort.new.new(Z3::LowLevel.mk_and(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(Z3::LowLevel.mk_bvand(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Bool and Bitvec"
  end
end

# File lib/z3/expr/expr.rb, line 103
def Distinct(*args)
  args = coerce_to_same_sort(*args)
  BoolSort.new.new(LowLevel.mk_distinct(args))
end

# File lib/z3/expr/expr.rb, line 98
def Eq(a, b)
  a, b = coerce_to_same_sort(a, b)
  BoolSort.new.new(LowLevel.mk_eq(a, b))
end

# File lib/z3/expr/expr.rb, line 62
def Ge(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_ge(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_ge or #unsigned_ge for Bitvec, not >="
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

# File lib/z3/expr/expr.rb, line 50
def Gt(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_gt(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_gt or #unsigned_gt for Bitvec, not >"
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

# File lib/z3/expr/expr.rb, line 86
def Le(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_le(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_le or #unsigned_le for Bitvec, not <="
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

# File lib/z3/expr/expr.rb, line 74
def Lt(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_lt(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_lt or #unsigned_lt for Bitvec, not <"
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end

# File lib/z3/expr/expr.rb, line 181
def Mul(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when ArithExpr
    args[0].sort.new(LowLevel.mk_mul(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(LowLevel.mk_bvmul(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} values, only Int/Real/Bitvec"
  end
end

# File lib/z3/expr/expr.rb, line 122
def Or(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when BoolExpr
    BoolSort.new.new(Z3::LowLevel.mk_or(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(Z3::LowLevel.mk_bvor(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Bool and Bitvec"
  end
end

# File lib/z3/expr/expr.rb, line 167
def Sub(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when ArithExpr
    args[0].sort.new(LowLevel.mk_sub(args))
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(LowLevel.mk_bvsub(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} values, only Int/Real/Bitvec"
  end
end

# File lib/z3/expr/expr.rb, line 136
def Xor(*args)
  args = coerce_to_same_sort(*args)
  case args[0]
  when BoolExpr
    args.inject do |a, b|
      BoolSort.new.new(Z3::LowLevel.mk_xor(a, b))
    end
  when BitvecExpr
    args.inject do |a, b|
      a.sort.new(Z3::LowLevel.mk_bvxor(a, b))
    end
  else
    raise Z3::Exception, "Can't perform logic operations on #{args[0].sort} exprs, only Bool and Bitvec"
  end
end

# File lib/z3/expr/expr.rb, line 24
def coerce_to_same_sort(*args)
  # This will raise exception unless one of the sorts is highest
  max_sort = args.map { |a| a.is_a?(Expr) ? a.sort : Expr.sort_for_const(a) }.max
  args.map do |a|
    max_sort.cast(a)
  end
end

# File lib/z3/expr/expr.rb, line 5
def initialize(_ast, sort)
  super(_ast)
  @sort = sort
  raise Z3::Exception, "Values must have AST kind numeral, app, or quantifier" unless [:numeral, :app, :quantifier].include?(ast_kind)
end

# File lib/z3/expr/expr.rb, line 45
def new_from_pointer(_ast)
  _sort = Z3::VeryLowLevel.Z3_get_sort(Z3::LowLevel._ctx_pointer, _ast)
  Sort.from_pointer(_sort).new(_ast)
end

# File lib/z3/expr/expr.rb, line 32
def sort_for_const(a)
  case a
  when TrueClass, FalseClass
    BoolSort.new
  when Integer
    IntSort.new
  when Float, Rational
    RealSort.new
  else
    raise Z3::Exception, "No idea how to autoconvert `#{a.class}': `#{a.inspect}'"
  end
end

# File lib/z3/expr/expr.rb, line 19
def !=(other)
  Expr.Distinct(self, other)
end

# File lib/z3/expr/expr.rb, line 15
def ==(other)
  Expr.Eq(self, other)
end

# File lib/z3/expr/expr.rb, line 11
def inspect
  "#{sort.to_s}<#{to_s}>"
end