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:



278
279
280
281
282
 
# 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

.LShift(a, b) ⇒ Object

Signed/Unsigned work the same



295
296
297
298
 
# 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) ⇒ Object 



332
333
334
335
336
337
 
# 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) ⇒ Object 



339
340
341
342
343
344
 
# 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) ⇒ Object 



386
387
388
389
 
# 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) ⇒ Object 



396
397
398
399
 
# 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) ⇒ Object 



300
301
302
303
 
# 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) ⇒ Object 



420
421
422
423
 
# 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) ⇒ Object 



371
372
373
374
 
# 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) ⇒ Object 



366
367
368
369
 
# 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) ⇒ Object 



381
382
383
384
 
# 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) ⇒ Object 



376
377
378
379
 
# 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) ⇒ Object 



310
311
312
313
 
# 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) ⇒ Object 



405
406
407
408
 
# 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) ⇒ Object 



415
416
417
418
 
# 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) ⇒ Object 



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

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

.SignedRem(a, b) ⇒ Object 



315
316
317
318
 
# 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

.SignedRShift(a, b) ⇒ Object 



284
285
286
287
 
# 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

.UnsignedAddNoOverflow(a, b) ⇒ Object 



391
392
393
394
 
# 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) ⇒ Object 



305
306
307
308
 
# 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) ⇒ Object 



351
352
353
354
 
# 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) ⇒ Object 



346
347
348
349
 
# 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) ⇒ Object 



361
362
363
364
 
# 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) ⇒ Object 



356
357
358
359
 
# 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) ⇒ Object 



410
411
412
413
 
# 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

.UnsignedRem(a, b) ⇒ Object 



320
321
322
323
 
# 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

.UnsignedRShift(a, b) ⇒ Object 



289
290
291
292
 
# 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

.Xnor(*args) ⇒ Object 



325
326
327
328
329
330
 
# 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

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 



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

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

#<<(other) ⇒ Object 



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

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

#<=(other) ⇒ Object 



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

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

#>(other) ⇒ Object 



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

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

#>=(other) ⇒ Object 



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

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

#>>(other) ⇒ Object

Raises:



169
170
171
 
# 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) ⇒ Object 



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

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

#abs ⇒ Object 



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

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

#add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



105
106
107
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#coerce(other) ⇒ Object 



269
270
271
272
273
 
# 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) ⇒ Object

Raises:



92
93
94
95
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#extract(hi, lo) ⇒ Object

Raises:



87
88
89
90
 
# 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) ⇒ Object 



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

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

#mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


139
140
141
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


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

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) 


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

def neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#negative? ⇒ Boolean

Returns:

  • (Boolean) 


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

def negative?
  self.signed_lt 0
end

#nonzero? ⇒ Boolean

Returns:

  • (Boolean) 


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

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) 


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

def positive?
  self.signed_gt 0
end

#rotate_left(num) ⇒ Object 



79
80
81
 
# 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) ⇒ Object 



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

def rotate_right(num)
  sort.new(LowLevel.mk_rotate_right(num, self))
end

#rshift(other) ⇒ Object

Raises:



181
182
183
 
# 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) ⇒ Object 



101
102
103
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


112
113
114
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


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

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) 


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

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

#signed_ge(other) ⇒ Object 



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

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

#signed_gt(other) ⇒ Object 



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

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

#signed_le(other) ⇒ Object 



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

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

#signed_lshift(other) ⇒ Object 



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

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

#signed_lt(other) ⇒ Object 



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

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) 


142
143
144
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

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 



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

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

#unsigned_add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


115
116
117
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


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

def unsigned_add_no_underflow?(other)
  raise "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) 


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

def unsigned_div_no_overflow?(other)
  raise "Unsigned / cannot underflow"
end

#unsigned_ge(other) ⇒ Object 



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

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

#unsigned_gt(other) ⇒ Object 



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

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

#unsigned_le(other) ⇒ Object 



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

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

#unsigned_lshift(other) ⇒ Object 



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

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

#unsigned_lt(other) ⇒ Object 



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

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

#unsigned_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


145
146
147
 
# 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) ⇒ Boolean

Returns:

  • (Boolean) 


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

def unsigned_mul_no_underflow?(other)
  raise "Unsigned + cannot underflow"
end

#unsigned_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

def unsigned_neg_no_overflow?
  raise "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 



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

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) 


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

def zero?
  self == 0
end

#zero_ext(size) ⇒ Object 



97
98
99
 
# 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) ⇒ 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