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:



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

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



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

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 



267
268
269
270
271
272
 
# File 'lib/z3/expr/bitvec_expr.rb', line 267

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 



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

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 



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

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 



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

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 



355
356
357
358
 
# File 'lib/z3/expr/bitvec_expr.rb', line 355

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 



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

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 



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

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 



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

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 



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

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 



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

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 



350
351
352
353
 
# File 'lib/z3/expr/bitvec_expr.rb', line 350

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 



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

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

.SignedRShift(a, b) ⇒ Object 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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

#<<(other) ⇒ Object 



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

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

#<=(other) ⇒ Object 



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

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

#>(other) ⇒ Object 



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

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

#>=(other) ⇒ Object 



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

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

#>>(other) ⇒ Object

Raises:



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

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:



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

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) 


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

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

#coerce(other) ⇒ Object 



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

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:



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

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) 


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

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

#extract(hi, lo) ⇒ Object

Raises:



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

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 



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

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

#mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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) 


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

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:



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

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

#sign_ext(size) ⇒ Object 



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

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) 


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

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

#signed_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_ge(other) ⇒ Object 



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

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

#signed_gt(other) ⇒ Object 



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

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

#signed_le(other) ⇒ Object 



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

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

#signed_lshift(other) ⇒ Object 



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

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

#signed_lt(other) ⇒ Object 



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

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

#signed_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

def signed_neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#signed_rshift(other) ⇒ Object 



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

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

#unsigned_add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_ge(other) ⇒ Object 



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

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

#unsigned_gt(other) ⇒ Object 



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

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

#unsigned_le(other) ⇒ Object 



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

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

#unsigned_lshift(other) ⇒ Object 



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

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

#unsigned_lt(other) ⇒ Object 



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

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

#unsigned_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_rshift(other) ⇒ Object 



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

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 



77
78
79
 
# File 'lib/z3/expr/bitvec_expr.rb', line 77

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