class Z3::BitvecExpr

Public Class Methods

Source

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

Signed/Unsigned work the same

Nand (*args)

Source

# File lib/z3/expr/bitvec_expr.rb, line 422
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 429
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 476
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 486
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 390
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 510
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 461
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 456
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 471
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 466
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 400
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 495
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 505
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)

Source

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

SignedRShift (a, b)

Source

# File lib/z3/expr/bitvec_expr.rb, line 374
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)

Source

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

SignedSubNoOverflow (a, b)

Source

# File lib/z3/expr/bitvec_expr.rb, line 515
def SignedSubNoOverflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvsub_no_overflow(a, b))
end

SignedSubNoUnderflow (a, b)

Source

# File lib/z3/expr/bitvec_expr.rb, line 520
def SignedSubNoUnderflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvsub_no_underflow(a, b, true))
end

UnsignedAddNoOverflow (a, b)

Source

# File lib/z3/expr/bitvec_expr.rb, line 481
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 395
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 441
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 436
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 451
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 446
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 500
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 379
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)

Source

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

UnsignedSubNoUnderflow (a, b)

Source

# File lib/z3/expr/bitvec_expr.rb, line 525
def UnsignedSubNoUnderflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvsub_no_underflow(a, b, false))
end

Xnor (*args)

Source

# File lib/z3/expr/bitvec_expr.rb, line 415
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)

Source

# File lib/z3/expr/bitvec_expr.rb, line 368
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

! ()

Source

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

% (other)

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)

Source

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

* (other)

Source

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

+ (other)

Source

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

- (other)

Source

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

-@ ()

Source

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

/ (other)

Source

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

< (other)

Source

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

<< (other)

Source

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

<= (other)

Source

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

> (other)

Source

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

>= (other)

Source

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

>> (other)

Source

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

^ (other)

Source

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

| (other)

Source

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

~ ()

Source

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

abs ()

Source

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

add_no_overflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 176
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)

Source

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

all_bits_set? ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 126
def all_bits_set?
  redand == 1
end

any_bits_set? ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 130
def any_bits_set?
  redor == 1
end

bit (index)

Source

# File lib/z3/expr/bitvec_expr.rb, line 106
def bit(index)
  raise Z3::Exception, "Trying to take a bit out of range" unless index.is_a?(Integer) and index.between?(0, sort.size - 1)
  BoolSort.new.new(LowLevel.mk_bit2bool(index, self))
end

A single bit, as a Bool. Deliberately not [] - that would read like extract with a one-bit range, which gives a Bitvec(1) instead

coerce (other)

Source

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

concat (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 99
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)

Source

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

extract (hi, lo)

Source

# File lib/z3/expr/bitvec_expr.rb, line 94
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)

Source

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

mul_no_overflow? (other)

Source

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

mul_no_underflow? (other)

Source

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

nand (other)

Source

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

neg_no_overflow? ()

Source

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

negative? ()

Source

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

nonzero? ()

Source

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

nor (other)

Source

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

positive? ()

Source

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

redand ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 118
def redand
  BitvecSort.new(1).new(LowLevel.mk_bvredand(self))
end

Z3 answers these with a one-bit Bitvec rather than a Bool, which is what all_bits_set? and any_bits_set? are for

redor ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 122
def redor
  BitvecSort.new(1).new(LowLevel.mk_bvredor(self))
end

repeat (count)

Source

# File lib/z3/expr/bitvec_expr.rb, line 111
def repeat(count)
  raise Z3::Exception, "Repeat count must be a positive Integer" unless count.is_a?(Integer) and count >= 1
  BitvecSort.new(sort.size * count).new(LowLevel.mk_repeat(count, self))
end

rotate_left (num)

Source

# File lib/z3/expr/bitvec_expr.rb, line 82
def rotate_left(num)
  return sort.new(LowLevel.mk_ext_rotate_left(self, sort.cast(num))) if num.is_a?(Expr)
  raise Z3::Exception, "Rotation amount must be a nonnegative Integer" unless num.is_a?(Integer) and num >= 0
  sort.new(LowLevel.mk_rotate_left(num, self))
end

An Integer rotates by a fixed amount, a Bitvec of the same size by whatever it turns out to be - Z3 has a separate operation for each, and the fixed one gives the solver much more to work with, so a literal never goes through the other

rotate_right (num)

Source

# File lib/z3/expr/bitvec_expr.rb, line 88
def rotate_right(num)
  return sort.new(LowLevel.mk_ext_rotate_right(self, sort.cast(num))) if num.is_a?(Expr)
  raise Z3::Exception, "Rotation amount must be a nonnegative Integer" unless num.is_a?(Integer) and num >= 0
  sort.new(LowLevel.mk_rotate_right(num, self))
end

rshift (other)

Source

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

sign_ext (size)

Source

# File lib/z3/expr/bitvec_expr.rb, line 171
def sign_ext(size)
  raise Z3::Exception, "Extension size must be a nonnegative Integer" unless size.is_a?(Integer) and size >= 0
  BitvecSort.new(sort.size + size).new(LowLevel.mk_sign_ext(size, self))
end

signed_add_no_overflow? (other)

Source

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

signed_add_no_underflow? (other)

Source

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

signed_div (other)

Source

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

signed_div_no_overflow? (other)

Source

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

signed_ge (other)

Source

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

signed_gt (other)

Source

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

signed_le (other)

Source

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

signed_lshift (other)

Source

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

signed_lt (other)

Source

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

signed_mod (other)

Source

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

signed_mul_no_overflow? (other)

Source

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

signed_mul_no_underflow? (other)

Source

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

signed_neg_no_overflow? ()

Source

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

signed_rem (other)

Source

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

signed_rshift (other)

Source

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

signed_sub_no_overflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 202
def signed_sub_no_overflow?(other)
  BitvecExpr.SignedSubNoOverflow(self, other)
end

signed_sub_no_underflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 212
def signed_sub_no_underflow?(other)
  BitvecExpr.SignedSubNoUnderflow(self, other)
end

signed_to_i ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 142
def signed_to_i
  IntSort.new.new(LowLevel.mk_bv2int(self, true))
end

signed_value ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 154
def signed_value
  v = unsigned_value
  v >= (1 << (sort.size - 1)) ? v - (1 << sort.size) : v
end

sub_no_overflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 199
def sub_no_overflow?(other)
  BitvecExpr.SignedSubNoOverflow(self, other)
end

Subtraction is addition’s mirror image: only signed can overflow, and both signs can underflow - so which of these takes a sign is the other way round

sub_no_underflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 209
def sub_no_underflow?(other)
  raise Z3::Exception, "Use #signed_sub_no_underflow? or #unsigned_sub_no_underflow? for Bitvec, not #sub_no_underflow?"
end

to_i ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 138
def to_i
  raise Z3::Exception, "Use #signed_to_i or #unsigned_to_i for Bitvec, not #to_i"
end

to_i and friends build a Z3 Int expression out of this one. value and friends leave Z3 and give back a Ruby Integer, which only works on a literal. Both come in pairs because a Bitvec carries no sign of its own - the same eight bits are 200 read one way and -56 read the other.

unsigned_add_no_overflow? (other)

Source

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

unsigned_add_no_underflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 193
def unsigned_add_no_underflow?(other)
  raise Z3::Exception, "Unsigned + can't underflow"
end

unsigned_div (other)

Source

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

unsigned_div_no_overflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 255
def unsigned_div_no_overflow?(other)
  raise Z3::Exception, "Unsigned / can't overflow"
end

unsigned_ge (other)

Source

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

unsigned_gt (other)

Source

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

unsigned_le (other)

Source

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

unsigned_lshift (other)

Source

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

unsigned_lt (other)

Source

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

unsigned_mul_no_overflow? (other)

Source

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

unsigned_mul_no_underflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 245
def unsigned_mul_no_underflow?(other)
  raise Z3::Exception, "Unsigned * can't underflow"
end

unsigned_neg_no_overflow? ()

Source

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

unsigned_rem (other)

Source

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

unsigned_rshift (other)

Source

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

unsigned_sub_no_overflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 205
def unsigned_sub_no_overflow?(other)
  raise Z3::Exception, "Unsigned - can't overflow"
end

unsigned_sub_no_underflow? (other)

Source

# File lib/z3/expr/bitvec_expr.rb, line 215
def unsigned_sub_no_underflow?(other)
  BitvecExpr.UnsignedSubNoUnderflow(self, other)
end

unsigned_to_i ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 146
def unsigned_to_i
  IntSort.new.new(LowLevel.mk_bv2int(self, false))
end

unsigned_value ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 160
def unsigned_value
  obj = ast_kind == :numeral ? self : simplify
  raise Z3::Exception, "Can't convert expression #{self} into Integer" unless obj.ast_kind == :numeral
  LowLevel.get_numeral_string(obj).to_i
end

Z3 prints a Bitvec numeral as its unsigned value, so this is the one it gives us

value ()

Source

# File lib/z3/expr/bitvec_expr.rb, line 150
def value
  raise Z3::Exception, "Use #signed_value or #unsigned_value for Bitvec, not #value"
end

xnor (other)

Source

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

zero? ()

Source

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

zero_ext (size)

Source

# File lib/z3/expr/bitvec_expr.rb, line 166
def zero_ext(size)
  raise Z3::Exception, "Extension size must be a nonnegative Integer" unless size.is_a?(Integer) and size >= 0
  BitvecSort.new(sort.size + size).new(LowLevel.mk_zero_ext(size, self))
end