class Z3::BitvecExpr

# File lib/z3/expr/bitvec_expr.rb, line 295
def LShift(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvshl(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 332
def Nand(*args)
  args = coerce_to_same_bv_sort(*args)
  args.inject do |a,b|
    a.sort.new(LowLevel.mk_bvnand(a, b))
  end
end

# File lib/z3/expr/bitvec_expr.rb, line 339
def Nor(*args)
  args = coerce_to_same_bv_sort(*args)
  args.inject do |a,b|
    a.sort.new(LowLevel.mk_bvnor(a, b))
  end
end

# File lib/z3/expr/bitvec_expr.rb, line 386
def SignedAddNoOverflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvadd_no_overflow(a, b, true))
end

# File lib/z3/expr/bitvec_expr.rb, line 396
def SignedAddNoUnderflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvadd_no_underflow(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 300
def SignedDiv(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvsdiv(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 420
def SignedDivNoOverflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvsdiv_no_overflow(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 371
def SignedGe(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvsge(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 366
def SignedGt(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvsgt(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 381
def SignedLe(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvsle(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 376
def SignedLt(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvslt(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 310
def SignedMod(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvsmod(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 405
def SignedMulNoOverflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvmul_no_overflow(a, b, true))
end

# File lib/z3/expr/bitvec_expr.rb, line 415
def SignedMulNoUnderflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvmul_no_underflow(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 401
def SignedNegNoOverflow(a)
  BoolSort.new.new(LowLevel.mk_bvneg_no_overflow(a))
end

# File lib/z3/expr/bitvec_expr.rb, line 284
def SignedRShift(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvashr(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 315
def SignedRem(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvsrem(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 391
def UnsignedAddNoOverflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvadd_no_overflow(a, b, false))
end

# File lib/z3/expr/bitvec_expr.rb, line 305
def UnsignedDiv(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvudiv(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 351
def UnsignedGe(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvuge(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 346
def UnsignedGt(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvugt(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 361
def UnsignedLe(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvule(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 356
def UnsignedLt(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvult(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 410
def UnsignedMulNoOverflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvmul_no_overflow(a, b, false))
end

# File lib/z3/expr/bitvec_expr.rb, line 289
def UnsignedRShift(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvlshr(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 320
def UnsignedRem(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvurem(a, b))
end

# File lib/z3/expr/bitvec_expr.rb, line 325
def Xnor(*args)
  args = coerce_to_same_bv_sort(*args)
  args.inject do |a,b|
    a.sort.new(LowLevel.mk_bvxnor(a, b))
  end
end

# File lib/z3/expr/bitvec_expr.rb, line 278
def coerce_to_same_bv_sort(*args)
  args = coerce_to_same_sort(*args)
  raise Z3::Exception, "Bitvec value with same size expected" unless args[0].is_a?(BitvecExpr)
  args
end

# File lib/z3/expr/bitvec_expr.rb, line 7
def !
  sort.new(LowLevel.mk_bvnot(self))
end

# File lib/z3/expr/bitvec_expr.rb, line 63
def %(other)
  raise Z3::Exception, "Use signed_mod or signed_rem or unsigned_rem"
end

# File lib/z3/expr/bitvec_expr.rb, line 15
def &(other)
  Expr.And(self, other)
end

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

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

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

# File lib/z3/expr/bitvec_expr.rb, line 11
def -@
  sort.new(LowLevel.mk_bvneg(self))
end

# File lib/z3/expr/bitvec_expr.rb, line 51
def /(other)
  raise Z3::Exception, "Use signed_div or unsigned_div"
end

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

# File lib/z3/expr/bitvec_expr.rb, line 185
def <<(other)
  BitvecExpr.LShift(self, other)
end

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

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

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

# File lib/z3/expr/bitvec_expr.rb, line 169
def >>(other)
  raise Z3::Exception, "Use #signed_rshift or #unsigned_rshift for Bitvec, not >>"
end

# File lib/z3/expr/bitvec_expr.rb, line 23
def ^(other)
  Expr.Xor(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 19
def |(other)
  Expr.Or(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 3
def ~
  sort.new(LowLevel.mk_bvnot(self))
end

# File lib/z3/expr/bitvec_expr.rb, line 265
def abs
  self.negative?.ite(-self, self)
end

# File lib/z3/expr/bitvec_expr.rb, line 105
def add_no_overflow?(other)
  raise Z3::Exception, "Use #signed_add_no_overflow? or #unsigned_add_no_overflow? for Bitvec, not #add_no_overflow?"
end

# File lib/z3/expr/bitvec_expr.rb, line 119
def add_no_underflow?(other)
  BitvecExpr.SignedAddNoUnderflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 269
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/bitvec_expr.rb, line 92
def concat(other)
  raise Z3::Exception, "Can only concatenate another Bitvec" unless other.is_a?(BitvecExpr)
  BitvecSort.new(sort.size + other.sort.size).new(LowLevel.mk_concat(self, other))
end

# File lib/z3/expr/bitvec_expr.rb, line 159
def div_no_overflow?(other)
  BitvecExpr.SignedDivNoOverflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 87
def extract(hi, lo)
  raise Z3::Exception, "Trying to extract bits out of range" unless sort.size > hi and hi >= lo and lo >= 0
  BitvecSort.new(hi - lo + 1).new(LowLevel.mk_extract(hi, lo, self))
end

# File lib/z3/expr/bitvec_expr.rb, line 197
def lshift(other)
  BitvecExpr.LShift(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 139
def mul_no_overflow?(other)
  raise "Use signed_mul_no_overflow? or unsigned_mul_no_overflow?"
end

# File lib/z3/expr/bitvec_expr.rb, line 149
def mul_no_underflow?(other)
  BitvecExpr.SignedMulNoUnderflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 31
def nand(other)
  BitvecExpr.Nand(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 135
def neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

# File lib/z3/expr/bitvec_expr.rb, line 261
def negative?
  self.signed_lt 0
end

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

# File lib/z3/expr/bitvec_expr.rb, line 35
def nor(other)
  BitvecExpr.Nor(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 257
def positive?
  self.signed_gt 0
end

# File lib/z3/expr/bitvec_expr.rb, line 79
def rotate_left(num)
  sort.new(LowLevel.mk_rotate_left(num, self))
end

# File lib/z3/expr/bitvec_expr.rb, line 83
def rotate_right(num)
  sort.new(LowLevel.mk_rotate_right(num, self))
end

# File lib/z3/expr/bitvec_expr.rb, line 181
def rshift(other)
  raise Z3::Exception, "Use #signed_rshift or #unsigned_rshift for Bitvec, not #rshift"
end

# File lib/z3/expr/bitvec_expr.rb, line 101
def sign_ext(size)
  BitvecSort.new(sort.size + size).new(LowLevel.mk_sign_ext(size, self))
end

# File lib/z3/expr/bitvec_expr.rb, line 112
def signed_add_no_overflow?(other)
  BitvecExpr.SignedAddNoOverflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 122
def signed_add_no_underflow?(other)
  BitvecExpr.SignedAddNoUnderflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 55
def signed_div(other)
  BitvecExpr.SignedDiv(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 162
def signed_div_no_overflow?(other)
  BitvecExpr.SignedDivNoOverflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 221
def signed_ge(other)
  BitvecExpr.SignedGe(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 217
def signed_gt(other)
  BitvecExpr.SignedGt(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 229
def signed_le(other)
  BitvecExpr.SignedLe(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 189
def signed_lshift(other)
  BitvecExpr.LShift(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 225
def signed_lt(other)
  BitvecExpr.SignedLt(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 67
def signed_mod(other)
  BitvecExpr.SignedMod(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 142
def signed_mul_no_overflow?(other)
  BitvecExpr.SignedMulNoOverflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 152
def signed_mul_no_underflow?(other)
  BitvecExpr.SignedMulNoUnderflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 132
def signed_neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

# File lib/z3/expr/bitvec_expr.rb, line 71
def signed_rem(other)
  BitvecExpr.SignedRem(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 173
def signed_rshift(other)
  BitvecExpr.SignedRShift(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 115
def unsigned_add_no_overflow?(other)
  BitvecExpr.UnsignedAddNoOverflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 125
def unsigned_add_no_underflow?(other)
  raise "Unsigned + cannot underflow"
end

# File lib/z3/expr/bitvec_expr.rb, line 59
def unsigned_div(other)
  BitvecExpr.UnsignedDiv(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 165
def unsigned_div_no_overflow?(other)
  raise "Unsigned / cannot underflow"
end

# File lib/z3/expr/bitvec_expr.rb, line 237
def unsigned_ge(other)
  BitvecExpr.UnsignedGe(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 233
def unsigned_gt(other)
  BitvecExpr.UnsignedGt(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 245
def unsigned_le(other)
  BitvecExpr.UnsignedLe(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 193
def unsigned_lshift(other)
  BitvecExpr.LShift(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 241
def unsigned_lt(other)
  BitvecExpr.UnsignedLt(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 145
def unsigned_mul_no_overflow?(other)
  BitvecExpr.UnsignedMulNoOverflow(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 155
def unsigned_mul_no_underflow?(other)
  raise "Unsigned + cannot underflow"
end

# File lib/z3/expr/bitvec_expr.rb, line 129
def unsigned_neg_no_overflow?
  raise "There is no unsigned negation"
end

# File lib/z3/expr/bitvec_expr.rb, line 75
def unsigned_rem(other)
  BitvecExpr.UnsignedRem(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 177
def unsigned_rshift(other)
  BitvecExpr.UnsignedRShift(self, other)
end

# File lib/z3/expr/bitvec_expr.rb, line 27
def xnor(other)
  BitvecExpr.Xnor(self, other)
end

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

# File lib/z3/expr/bitvec_expr.rb, line 97
def zero_ext(size)
  BitvecSort.new(sort.size + size).new(LowLevel.mk_zero_ext(size, self))
end