Class: Z3::BitvecExpr

Inherits:
Expr show all
Defined in:
lib/z3/expr/bitvec_expr.rb

Instance Attribute Summary

Attributes inherited from Expr

#sort

Attributes inherited from AST

#_ast

Class Method Summary collapse

Instance Method Summary collapse

Methods inherited from Expr

#!=, #==, Add, And, Distinct, Eq, Ge, Gt, Le, Lt, Mul, Or, Sub, Xor, coerce_to_same_sort, #initialize, #inspect, new_from_pointer, sort_for_const

Methods inherited from AST

#arguments, #ast_kind, #eql?, #func_decl, #hash, #initialize, #sexpr, #simplify, #to_s

Constructor Details

This class inherits a constructor from Z3::Expr

Class Method Details

.coerce_to_same_bv_sort(*args) ⇒ Object

Raises:



279
280
281
282
283
 
# File 'lib/z3/expr/bitvec_expr.rb', line 279

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

.LShift(a, b) ⇒ Object

Signed/Unsigned work the same



296
297
298
299
 
# File 'lib/z3/expr/bitvec_expr.rb', line 296

def LShift(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvshl(a, b))
end

.Nand(*args) ⇒ Object 



333
334
335
336
337
338
 
# File 'lib/z3/expr/bitvec_expr.rb', line 333

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) ⇒ Object 



340
341
342
343
344
345
 
# File 'lib/z3/expr/bitvec_expr.rb', line 340

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) ⇒ Object 



387
388
389
390
 
# File 'lib/z3/expr/bitvec_expr.rb', line 387

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) ⇒ Object 



397
398
399
400
 
# File 'lib/z3/expr/bitvec_expr.rb', line 397

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) ⇒ Object 



301
302
303
304
 
# File 'lib/z3/expr/bitvec_expr.rb', line 301

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) ⇒ Object 



421
422
423
424
 
# File 'lib/z3/expr/bitvec_expr.rb', line 421

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) ⇒ Object 



372
373
374
375
 
# File 'lib/z3/expr/bitvec_expr.rb', line 372

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) ⇒ Object 



367
368
369
370
 
# File 'lib/z3/expr/bitvec_expr.rb', line 367

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) ⇒ Object 



382
383
384
385
 
# File 'lib/z3/expr/bitvec_expr.rb', line 382

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) ⇒ Object 



377
378
379
380
 
# File 'lib/z3/expr/bitvec_expr.rb', line 377

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) ⇒ Object 



311
312
313
314
 
# File 'lib/z3/expr/bitvec_expr.rb', line 311

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) ⇒ Object 



406
407
408
409
 
# File 'lib/z3/expr/bitvec_expr.rb', line 406

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) ⇒ Object 



416
417
418
419
 
# File 'lib/z3/expr/bitvec_expr.rb', line 416

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) ⇒ Object 



402
403
404
 
# File 'lib/z3/expr/bitvec_expr.rb', line 402

def SignedNegNoOverflow(a)
  BoolSort.new.new(LowLevel.mk_bvneg_no_overflow(a))
end

.SignedRem(a, b) ⇒ Object 



316
317
318
319
 
# File 'lib/z3/expr/bitvec_expr.rb', line 316

def SignedRem(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvsrem(a, b))
end

.SignedRShift(a, b) ⇒ Object 



285
286
287
288
 
# File 'lib/z3/expr/bitvec_expr.rb', line 285

def SignedRShift(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvashr(a, b))
end

.UnsignedAddNoOverflow(a, b) ⇒ Object 



392
393
394
395
 
# File 'lib/z3/expr/bitvec_expr.rb', line 392

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) ⇒ Object 



306
307
308
309
 
# File 'lib/z3/expr/bitvec_expr.rb', line 306

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) ⇒ Object 



352
353
354
355
 
# File 'lib/z3/expr/bitvec_expr.rb', line 352

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) ⇒ Object 



347
348
349
350
 
# File 'lib/z3/expr/bitvec_expr.rb', line 347

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) ⇒ Object 



362
363
364
365
 
# File 'lib/z3/expr/bitvec_expr.rb', line 362

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) ⇒ Object 



357
358
359
360
 
# File 'lib/z3/expr/bitvec_expr.rb', line 357

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) ⇒ Object 



411
412
413
414
 
# File 'lib/z3/expr/bitvec_expr.rb', line 411

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

.UnsignedRem(a, b) ⇒ Object 



321
322
323
324
 
# File 'lib/z3/expr/bitvec_expr.rb', line 321

def UnsignedRem(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvurem(a, b))
end

.UnsignedRShift(a, b) ⇒ Object 



290
291
292
293
 
# File 'lib/z3/expr/bitvec_expr.rb', line 290

def UnsignedRShift(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  a.sort.new(LowLevel.mk_bvlshr(a, b))
end

.Xnor(*args) ⇒ Object 



326
327
328
329
330
331
 
# File 'lib/z3/expr/bitvec_expr.rb', line 326

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

Instance Method Details

#! ⇒ Object 



7
8
9
 
# File 'lib/z3/expr/bitvec_expr.rb', line 7

def !
  sort.new(LowLevel.mk_bvnot(self))
end

#%(other) ⇒ Object

Raises:



63
64
65
 
# 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) ⇒ Object 



15
16
17
 
# File 'lib/z3/expr/bitvec_expr.rb', line 15

def &(other)
  Expr.And(self, other)
end

#*(other) ⇒ Object 



47
48
49
 
# File 'lib/z3/expr/bitvec_expr.rb', line 47

def *(other)
  Expr.Mul(self, other)
end

#+(other) ⇒ Object 



39
40
41
 
# File 'lib/z3/expr/bitvec_expr.rb', line 39

def +(other)
  Expr.Add(self, other)
end

#-(other) ⇒ Object 



43
44
45
 
# File 'lib/z3/expr/bitvec_expr.rb', line 43

def -(other)
  Expr.Sub(self, other)
end

#-@ ⇒ Object 



11
12
13
 
# File 'lib/z3/expr/bitvec_expr.rb', line 11

def -@
  sort.new(LowLevel.mk_bvneg(self))
end

#/(other) ⇒ Object

Raises:



51
52
53
 
# File 'lib/z3/expr/bitvec_expr.rb', line 51

def /(other)
  raise Z3::Exception, "Use signed_div or unsigned_div"
end

#<(other) ⇒ Object 



214
215
216
 
# File 'lib/z3/expr/bitvec_expr.rb', line 214

def <(other)
  Expr.Lt(self, other)
end

#<<(other) ⇒ Object 



186
187
188
 
# File 'lib/z3/expr/bitvec_expr.rb', line 186

def <<(other)
  BitvecExpr.LShift(self, other)
end

#<=(other) ⇒ Object 



210
211
212
 
# File 'lib/z3/expr/bitvec_expr.rb', line 210

def <=(other)
  Expr.Le(self, other)
end

#>(other) ⇒ Object 



202
203
204
 
# File 'lib/z3/expr/bitvec_expr.rb', line 202

def >(other)
  Expr.Gt(self, other)
end

#>=(other) ⇒ Object 



206
207
208
 
# File 'lib/z3/expr/bitvec_expr.rb', line 206

def >=(other)
  Expr.Ge(self, other)
end

#>>(other) ⇒ Object

Raises:



170
171
172
 
# File 'lib/z3/expr/bitvec_expr.rb', line 170

def >>(other)
  raise Z3::Exception, "Use #signed_rshift or #unsigned_rshift for Bitvec, not >>"
end

#^(other) ⇒ Object 



23
24
25
 
# File 'lib/z3/expr/bitvec_expr.rb', line 23

def ^(other)
  Expr.Xor(self, other)
end

#abs ⇒ Object 



266
267
268
 
# File 'lib/z3/expr/bitvec_expr.rb', line 266

def abs
  self.negative?.ite(-self, self)
end

#add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



109
110
111
 
# File 'lib/z3/expr/bitvec_expr.rb', line 109

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) ⇒ Boolean

Returns:

  • (Boolean) 


120
121
122
 
# File 'lib/z3/expr/bitvec_expr.rb', line 120

def add_no_underflow?(other)
  BitvecExpr.SignedAddNoUnderflow(self, other)
end

#coerce(other) ⇒ Object 



270
271
272
273
274
 
# File 'lib/z3/expr/bitvec_expr.rb', line 270

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) ⇒ Object

Raises:



94
95
96
97
 
# File 'lib/z3/expr/bitvec_expr.rb', line 94

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) ⇒ Boolean

Returns:

  • (Boolean) 


160
161
162
 
# File 'lib/z3/expr/bitvec_expr.rb', line 160

def div_no_overflow?(other)
  BitvecExpr.SignedDivNoOverflow(self, other)
end

#extract(hi, lo) ⇒ Object

Raises:



89
90
91
92
 
# File 'lib/z3/expr/bitvec_expr.rb', line 89

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) ⇒ Object 



198
199
200
 
# File 'lib/z3/expr/bitvec_expr.rb', line 198

def lshift(other)
  BitvecExpr.LShift(self, other)
end

#mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



140
141
142
 
# File 'lib/z3/expr/bitvec_expr.rb', line 140

def mul_no_overflow?(other)
  raise Z3::Exception, "Use signed_mul_no_overflow? or unsigned_mul_no_overflow?"
end

#mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


150
151
152
 
# File 'lib/z3/expr/bitvec_expr.rb', line 150

def mul_no_underflow?(other)
  BitvecExpr.SignedMulNoUnderflow(self, other)
end

#nand(other) ⇒ Object 



31
32
33
 
# File 'lib/z3/expr/bitvec_expr.rb', line 31

def nand(other)
  BitvecExpr.Nand(self, other)
end

#neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


136
137
138
 
# File 'lib/z3/expr/bitvec_expr.rb', line 136

def neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#negative? ⇒ Boolean

Returns:

  • (Boolean) 


262
263
264
 
# File 'lib/z3/expr/bitvec_expr.rb', line 262

def negative?
  self.signed_lt 0
end

#nonzero? ⇒ Boolean

Returns:

  • (Boolean) 


254
255
256
 
# File 'lib/z3/expr/bitvec_expr.rb', line 254

def nonzero?
  self != 0
end

#nor(other) ⇒ Object 



35
36
37
 
# File 'lib/z3/expr/bitvec_expr.rb', line 35

def nor(other)
  BitvecExpr.Nor(self, other)
end

#positive? ⇒ Boolean

Returns:

  • (Boolean) 


258
259
260
 
# File 'lib/z3/expr/bitvec_expr.rb', line 258

def positive?
  self.signed_gt 0
end

#rotate_left(num) ⇒ Object

Raises:



79
80
81
82
 
# File 'lib/z3/expr/bitvec_expr.rb', line 79

def rotate_left(num)
  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

#rotate_right(num) ⇒ Object

Raises:



84
85
86
87
 
# File 'lib/z3/expr/bitvec_expr.rb', line 84

def rotate_right(num)
  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) ⇒ Object

Raises:



182
183
184
 
# File 'lib/z3/expr/bitvec_expr.rb', line 182

def rshift(other)
  raise Z3::Exception, "Use #signed_rshift or #unsigned_rshift for Bitvec, not #rshift"
end

#sign_ext(size) ⇒ Object

Raises:



104
105
106
107
 
# File 'lib/z3/expr/bitvec_expr.rb', line 104

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) ⇒ Boolean

Returns:

  • (Boolean) 


113
114
115
 
# File 'lib/z3/expr/bitvec_expr.rb', line 113

def signed_add_no_overflow?(other)
  BitvecExpr.SignedAddNoOverflow(self, other)
end

#signed_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


123
124
125
 
# File 'lib/z3/expr/bitvec_expr.rb', line 123

def signed_add_no_underflow?(other)
  BitvecExpr.SignedAddNoUnderflow(self, other)
end

#signed_div(other) ⇒ Object 



55
56
57
 
# File 'lib/z3/expr/bitvec_expr.rb', line 55

def signed_div(other)
  BitvecExpr.SignedDiv(self, other)
end

#signed_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


163
164
165
 
# File 'lib/z3/expr/bitvec_expr.rb', line 163

def signed_div_no_overflow?(other)
  BitvecExpr.SignedDivNoOverflow(self, other)
end

#signed_ge(other) ⇒ Object 



222
223
224
 
# File 'lib/z3/expr/bitvec_expr.rb', line 222

def signed_ge(other)
  BitvecExpr.SignedGe(self, other)
end

#signed_gt(other) ⇒ Object 



218
219
220
 
# File 'lib/z3/expr/bitvec_expr.rb', line 218

def signed_gt(other)
  BitvecExpr.SignedGt(self, other)
end

#signed_le(other) ⇒ Object 



230
231
232
 
# File 'lib/z3/expr/bitvec_expr.rb', line 230

def signed_le(other)
  BitvecExpr.SignedLe(self, other)
end

#signed_lshift(other) ⇒ Object 



190
191
192
 
# File 'lib/z3/expr/bitvec_expr.rb', line 190

def signed_lshift(other)
  BitvecExpr.LShift(self, other)
end

#signed_lt(other) ⇒ Object 



226
227
228
 
# File 'lib/z3/expr/bitvec_expr.rb', line 226

def signed_lt(other)
  BitvecExpr.SignedLt(self, other)
end

#signed_mod(other) ⇒ Object 



67
68
69
 
# File 'lib/z3/expr/bitvec_expr.rb', line 67

def signed_mod(other)
  BitvecExpr.SignedMod(self, other)
end

#signed_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


143
144
145
 
# File 'lib/z3/expr/bitvec_expr.rb', line 143

def signed_mul_no_overflow?(other)
  BitvecExpr.SignedMulNoOverflow(self, other)
end

#signed_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


153
154
155
 
# File 'lib/z3/expr/bitvec_expr.rb', line 153

def signed_mul_no_underflow?(other)
  BitvecExpr.SignedMulNoUnderflow(self, other)
end

#signed_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


133
134
135
 
# File 'lib/z3/expr/bitvec_expr.rb', line 133

def signed_neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#signed_rem(other) ⇒ Object 



71
72
73
 
# File 'lib/z3/expr/bitvec_expr.rb', line 71

def signed_rem(other)
  BitvecExpr.SignedRem(self, other)
end

#signed_rshift(other) ⇒ Object 



174
175
176
 
# File 'lib/z3/expr/bitvec_expr.rb', line 174

def signed_rshift(other)
  BitvecExpr.SignedRShift(self, other)
end

#unsigned_add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


116
117
118
 
# File 'lib/z3/expr/bitvec_expr.rb', line 116

def unsigned_add_no_overflow?(other)
  BitvecExpr.UnsignedAddNoOverflow(self, other)
end

#unsigned_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



126
127
128
 
# File 'lib/z3/expr/bitvec_expr.rb', line 126

def unsigned_add_no_underflow?(other)
  raise Z3::Exception, "Unsigned + cannot underflow"
end

#unsigned_div(other) ⇒ Object 



59
60
61
 
# File 'lib/z3/expr/bitvec_expr.rb', line 59

def unsigned_div(other)
  BitvecExpr.UnsignedDiv(self, other)
end

#unsigned_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



166
167
168
 
# File 'lib/z3/expr/bitvec_expr.rb', line 166

def unsigned_div_no_overflow?(other)
  raise Z3::Exception, "Unsigned / cannot overflow"
end

#unsigned_ge(other) ⇒ Object 



238
239
240
 
# File 'lib/z3/expr/bitvec_expr.rb', line 238

def unsigned_ge(other)
  BitvecExpr.UnsignedGe(self, other)
end

#unsigned_gt(other) ⇒ Object 



234
235
236
 
# File 'lib/z3/expr/bitvec_expr.rb', line 234

def unsigned_gt(other)
  BitvecExpr.UnsignedGt(self, other)
end

#unsigned_le(other) ⇒ Object 



246
247
248
 
# File 'lib/z3/expr/bitvec_expr.rb', line 246

def unsigned_le(other)
  BitvecExpr.UnsignedLe(self, other)
end

#unsigned_lshift(other) ⇒ Object 



194
195
196
 
# File 'lib/z3/expr/bitvec_expr.rb', line 194

def unsigned_lshift(other)
  BitvecExpr.LShift(self, other)
end

#unsigned_lt(other) ⇒ Object 



242
243
244
 
# File 'lib/z3/expr/bitvec_expr.rb', line 242

def unsigned_lt(other)
  BitvecExpr.UnsignedLt(self, other)
end

#unsigned_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


146
147
148
 
# File 'lib/z3/expr/bitvec_expr.rb', line 146

def unsigned_mul_no_overflow?(other)
  BitvecExpr.UnsignedMulNoOverflow(self, other)
end

#unsigned_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



156
157
158
 
# File 'lib/z3/expr/bitvec_expr.rb', line 156

def unsigned_mul_no_underflow?(other)
  raise Z3::Exception, "Unsigned * cannot underflow"
end

#unsigned_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean)

Raises:



130
131
132
 
# File 'lib/z3/expr/bitvec_expr.rb', line 130

def unsigned_neg_no_overflow?
  raise Z3::Exception, "There is no unsigned negation"
end

#unsigned_rem(other) ⇒ Object 



75
76
77
 
# File 'lib/z3/expr/bitvec_expr.rb', line 75

def unsigned_rem(other)
  BitvecExpr.UnsignedRem(self, other)
end

#unsigned_rshift(other) ⇒ Object 



178
179
180
 
# File 'lib/z3/expr/bitvec_expr.rb', line 178

def unsigned_rshift(other)
  BitvecExpr.UnsignedRShift(self, other)
end

#xnor(other) ⇒ Object 



27
28
29
 
# File 'lib/z3/expr/bitvec_expr.rb', line 27

def xnor(other)
  BitvecExpr.Xnor(self, other)
end

#zero? ⇒ Boolean

Returns:

  • (Boolean) 


250
251
252
 
# File 'lib/z3/expr/bitvec_expr.rb', line 250

def zero?
  self == 0
end

#zero_ext(size) ⇒ Object

Raises:



99
100
101
102
 
# File 'lib/z3/expr/bitvec_expr.rb', line 99

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

#|(other) ⇒ Object 



19
20
21
 
# File 'lib/z3/expr/bitvec_expr.rb', line 19

def |(other)
  Expr.Or(self, other)
end

#~ ⇒ Object 



3
4
5
 
# File 'lib/z3/expr/bitvec_expr.rb', line 3

def ~
  sort.new(LowLevel.mk_bvnot(self))
end