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