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, #func_decl, #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:



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

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



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

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 



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

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 



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

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 



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

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 



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

def SignedAddNoUnderflow(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvadd_no_underflow(a, b))
end

.SignedDivNoOverflow(a, b) ⇒ Object 



345
346
347
348
 
# File 'lib/z3/expr/bitvec_expr.rb', line 345

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 



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

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 



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

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 



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

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 



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

def SignedLt(a, b)
  a, b = coerce_to_same_bv_sort(a, b)
  BoolSort.new.new(LowLevel.mk_bvslt(a, b))
end

.SignedMulNoOverflow(a, b) ⇒ Object 



330
331
332
333
 
# File 'lib/z3/expr/bitvec_expr.rb', line 330

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 



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

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 



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

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

.SignedRShift(a, b) ⇒ Object 



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

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 



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

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

.UnsignedGe(a, b) ⇒ Object 



276
277
278
279
 
# File 'lib/z3/expr/bitvec_expr.rb', line 276

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 



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

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 



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

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 



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

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 



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

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



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

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 



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

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 



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

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



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

def /(other)
  raise "Use signed_div or unsigned_div"
end

#<(other) ⇒ Object 



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

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

#<<(other) ⇒ Object 



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

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

#<=(other) ⇒ Object 



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

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

#>(other) ⇒ Object 



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

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

#>=(other) ⇒ Object 



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

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

#>>(other) ⇒ Object

Raises:



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

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

#add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



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

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) 


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

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

#coerce(other) ⇒ Object 



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

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

#div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#lshift(other) ⇒ Object 



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

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

#mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

def mul_no_overflow?(other)
  raise "Use signed_mul_no_overflow? or unsigned_mul_no_overflow?"
end

#mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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) 


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

def neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#nor(other) ⇒ Object 



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

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

#rotate_left(num) ⇒ Object 



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

def rotate_left(num)
  sort.new(LowLevel.mk_rotate_left(num, self))
end

#rotate_right(num) ⇒ Object 



63
64
65
 
# File 'lib/z3/expr/bitvec_expr.rb', line 63

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

#rshift(other) ⇒ Object

Raises:



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

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

#sign_ext(size) ⇒ Object 



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

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) 


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

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

#signed_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


92
93
94
 
# File 'lib/z3/expr/bitvec_expr.rb', line 92

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

#signed_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_ge(other) ⇒ Object 



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

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

#signed_gt(other) ⇒ Object 



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

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

#signed_le(other) ⇒ Object 



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

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

#signed_lshift(other) ⇒ Object 



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

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

#signed_lt(other) ⇒ Object 



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

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

#signed_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


102
103
104
 
# File 'lib/z3/expr/bitvec_expr.rb', line 102

def signed_neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#signed_rshift(other) ⇒ Object 



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

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

#unsigned_add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_ge(other) ⇒ Object 



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

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

#unsigned_gt(other) ⇒ Object 



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

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

#unsigned_le(other) ⇒ Object 



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

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

#unsigned_lshift(other) ⇒ Object 



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

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

#unsigned_lt(other) ⇒ Object 



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

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

#unsigned_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

def unsigned_neg_no_overflow?
  raise "There is no unsigned negation"
end

#unsigned_rshift(other) ⇒ Object 



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

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_ext(size) ⇒ Object 



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

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