class Z3::BitvecExpr

Public Class Methods

LShift(a, b) click to toggle source

Signed/Unsigned work the same

# 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
Nand(*args) click to toggle source
# 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
Nor(*args) click to toggle source
# 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
SignedAddNoOverflow(a, b) click to toggle source
# 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
SignedAddNoUnderflow(a, b) click to toggle source
# 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
SignedDiv(a, b) click to toggle source
# 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
SignedDivNoOverflow(a, b) click to toggle source
# 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
SignedGe(a, b) click to toggle source
# 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
SignedGt(a, b) click to toggle source
# 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
SignedLe(a, b) click to toggle source
# 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
SignedLt(a, b) click to toggle source
# 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
SignedMod(a, b) click to toggle source
# 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
SignedMulNoOverflow(a, b) click to toggle source
# 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
SignedMulNoUnderflow(a, b) click to toggle source
# 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
SignedNegNoOverflow(a) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 401
def SignedNegNoOverflow(a)
  BoolSort.new.new(LowLevel.mk_bvneg_no_overflow(a))
end
SignedRShift(a, b) click to toggle source
# 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
SignedRem(a, b) click to toggle source
# 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
UnsignedAddNoOverflow(a, b) click to toggle source
# 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
UnsignedDiv(a, b) click to toggle source
# 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
UnsignedGe(a, b) click to toggle source
# 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
UnsignedGt(a, b) click to toggle source
# 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
UnsignedLe(a, b) click to toggle source
# 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
UnsignedLt(a, b) click to toggle source
# 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
UnsignedMulNoOverflow(a, b) click to toggle source
# 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
UnsignedRShift(a, b) click to toggle source
# 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
UnsignedRem(a, b) click to toggle source
# 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
Xnor(*args) click to toggle source
# 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
coerce_to_same_bv_sort(*args) click to toggle source
# 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

Public Instance Methods

!() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 7
def !
  sort.new(LowLevel.mk_bvnot(self))
end
%(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 63
def %(other)
  raise Z3::Exception, "Use signed_mod or signed_rem or unsigned_rem"
end
&(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 15
def &(other)
  Expr.And(self, other)
end
*(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 47
def *(other)
  Expr.Mul(self, other)
end
+(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 39
def +(other)
  Expr.Add(self, other)
end
-(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 43
def -(other)
  Expr.Sub(self, other)
end
-@() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 11
def -@
  sort.new(LowLevel.mk_bvneg(self))
end
/(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 51
def /(other)
  raise Z3::Exception, "Use signed_div or unsigned_div"
end
<(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 213
def <(other)
  Expr.Lt(self, other)
end
<<(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 185
def <<(other)
  BitvecExpr.LShift(self, other)
end
<=(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 209
def <=(other)
  Expr.Le(self, other)
end
>(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 201
def >(other)
  Expr.Gt(self, other)
end
>=(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 205
def >=(other)
  Expr.Ge(self, other)
end
>>(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 169
def >>(other)
  raise Z3::Exception, "Use #signed_rshift or #unsigned_rshift for Bitvec, not >>"
end
^(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 23
def ^(other)
  Expr.Xor(self, other)
end
abs() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 265
def abs
  self.negative?.ite(-self, self)
end
add_no_overflow?(other) click to toggle source
# 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
add_no_underflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 119
def add_no_underflow?(other)
  BitvecExpr.SignedAddNoUnderflow(self, other)
end
coerce(other) click to toggle source
# 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
concat(other) click to toggle source
# 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
div_no_overflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 159
def div_no_overflow?(other)
  BitvecExpr.SignedDivNoOverflow(self, other)
end
extract(hi, lo) click to toggle source
# 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
lshift(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 197
def lshift(other)
  BitvecExpr.LShift(self, other)
end
mul_no_overflow?(other) click to toggle source
# 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
mul_no_underflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 149
def mul_no_underflow?(other)
  BitvecExpr.SignedMulNoUnderflow(self, other)
end
nand(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 31
def nand(other)
  BitvecExpr.Nand(self, other)
end
neg_no_overflow?() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 135
def neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end
negative?() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 261
def negative?
  self.signed_lt 0
end
nonzero?() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 253
def nonzero?
  self != 0
end
nor(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 35
def nor(other)
  BitvecExpr.Nor(self, other)
end
positive?() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 257
def positive?
  self.signed_gt 0
end
rotate_left(num) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 79
def rotate_left(num)
  sort.new(LowLevel.mk_rotate_left(num, self))
end
rotate_right(num) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 83
def rotate_right(num)
  sort.new(LowLevel.mk_rotate_right(num, self))
end
rshift(other) click to toggle source
# 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
sign_ext(size) click to toggle source
# 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
signed_add_no_overflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 112
def signed_add_no_overflow?(other)
  BitvecExpr.SignedAddNoOverflow(self, other)
end
signed_add_no_underflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 122
def signed_add_no_underflow?(other)
  BitvecExpr.SignedAddNoUnderflow(self, other)
end
signed_div(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 55
def signed_div(other)
  BitvecExpr.SignedDiv(self, other)
end
signed_div_no_overflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 162
def signed_div_no_overflow?(other)
  BitvecExpr.SignedDivNoOverflow(self, other)
end
signed_ge(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 221
def signed_ge(other)
  BitvecExpr.SignedGe(self, other)
end
signed_gt(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 217
def signed_gt(other)
  BitvecExpr.SignedGt(self, other)
end
signed_le(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 229
def signed_le(other)
  BitvecExpr.SignedLe(self, other)
end
signed_lshift(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 189
def signed_lshift(other)
  BitvecExpr.LShift(self, other)
end
signed_lt(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 225
def signed_lt(other)
  BitvecExpr.SignedLt(self, other)
end
signed_mod(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 67
def signed_mod(other)
  BitvecExpr.SignedMod(self, other)
end
signed_mul_no_overflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 142
def signed_mul_no_overflow?(other)
  BitvecExpr.SignedMulNoOverflow(self, other)
end
signed_mul_no_underflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 152
def signed_mul_no_underflow?(other)
  BitvecExpr.SignedMulNoUnderflow(self, other)
end
signed_neg_no_overflow?() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 132
def signed_neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end
signed_rem(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 71
def signed_rem(other)
  BitvecExpr.SignedRem(self, other)
end
signed_rshift(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 173
def signed_rshift(other)
  BitvecExpr.SignedRShift(self, other)
end
unsigned_add_no_overflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 115
def unsigned_add_no_overflow?(other)
  BitvecExpr.UnsignedAddNoOverflow(self, other)
end
unsigned_add_no_underflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 125
def unsigned_add_no_underflow?(other)
  raise "Unsigned + cannot underflow"
end
unsigned_div(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 59
def unsigned_div(other)
  BitvecExpr.UnsignedDiv(self, other)
end
unsigned_div_no_overflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 165
def unsigned_div_no_overflow?(other)
  raise "Unsigned / cannot underflow"
end
unsigned_ge(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 237
def unsigned_ge(other)
  BitvecExpr.UnsignedGe(self, other)
end
unsigned_gt(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 233
def unsigned_gt(other)
  BitvecExpr.UnsignedGt(self, other)
end
unsigned_le(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 245
def unsigned_le(other)
  BitvecExpr.UnsignedLe(self, other)
end
unsigned_lshift(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 193
def unsigned_lshift(other)
  BitvecExpr.LShift(self, other)
end
unsigned_lt(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 241
def unsigned_lt(other)
  BitvecExpr.UnsignedLt(self, other)
end
unsigned_mul_no_overflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 145
def unsigned_mul_no_overflow?(other)
  BitvecExpr.UnsignedMulNoOverflow(self, other)
end
unsigned_mul_no_underflow?(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 155
def unsigned_mul_no_underflow?(other)
  raise "Unsigned + cannot underflow"
end
unsigned_neg_no_overflow?() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 129
def unsigned_neg_no_overflow?
  raise "There is no unsigned negation"
end
unsigned_rem(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 75
def unsigned_rem(other)
  BitvecExpr.UnsignedRem(self, other)
end
unsigned_rshift(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 177
def unsigned_rshift(other)
  BitvecExpr.UnsignedRShift(self, other)
end
xnor(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 27
def xnor(other)
  BitvecExpr.Xnor(self, other)
end
zero?() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 249
def zero?
  self == 0
end
zero_ext(size) click to toggle source
# 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
|(other) click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 19
def |(other)
  Expr.Or(self, other)
end
~() click to toggle source
# File lib/z3/expr/bitvec_expr.rb, line 3
def ~
  sort.new(LowLevel.mk_bvnot(self))
end