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:



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

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



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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

.SignedRShift(a, b) ⇒ Object 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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 



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

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

#%(other) ⇒ Object 



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

def %(other)
  raise "Use signed_mod or signed_rem or unsigned_rem"
end

#&(other) ⇒ Object 



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

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

#*(other) ⇒ Object 



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

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

#+(other) ⇒ Object 



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

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

#-(other) ⇒ Object 



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

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

#-@ ⇒ Object 



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

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

#/(other) ⇒ Object 



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

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

#<(other) ⇒ Object 



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

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

#<<(other) ⇒ Object 



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

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

#<=(other) ⇒ Object 



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

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

#>(other) ⇒ Object 



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

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

#>=(other) ⇒ Object 



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

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

#>>(other) ⇒ Object

Raises:



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

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

#^(other) ⇒ Object 



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

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

#add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean)

Raises:



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

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) 


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

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

#coerce(other) ⇒ Object 



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

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) 


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

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

#lshift(other) ⇒ Object 



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

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

#mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#nand(other) ⇒ Object 



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

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

#neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

def neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#nor(other) ⇒ Object 



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

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

#rotate_left(num) ⇒ Object 



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

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

#rotate_right(num) ⇒ Object 



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

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

#rshift(other) ⇒ Object

Raises:



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

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

#sign_ext(size) ⇒ Object 



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

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) 


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

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

#signed_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_ge(other) ⇒ Object 



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

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

#signed_gt(other) ⇒ Object 



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

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

#signed_le(other) ⇒ Object 



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

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

#signed_lshift(other) ⇒ Object 



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

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

#signed_lt(other) ⇒ Object 



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

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

#signed_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#signed_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

def signed_neg_no_overflow?
  BitvecExpr.SignedNegNoOverflow(self)
end

#signed_rshift(other) ⇒ Object 



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

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

#unsigned_add_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_add_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_div_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_ge(other) ⇒ Object 



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

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

#unsigned_gt(other) ⇒ Object 



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

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

#unsigned_le(other) ⇒ Object 



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

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

#unsigned_lshift(other) ⇒ Object 



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

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

#unsigned_lt(other) ⇒ Object 



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

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

#unsigned_mul_no_overflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_mul_no_underflow?(other) ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_neg_no_overflow? ⇒ Boolean

Returns:

  • (Boolean) 


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

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

#unsigned_rshift(other) ⇒ Object 



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

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

#xnor(other) ⇒ Object 



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

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

#zero_ext(size) ⇒ Object 



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

def zero_ext(size)
  BitvecSort.new(sort.size + size).new(LowLevel.mk_zero_ext(size, self))
end

#|(other) ⇒ Object 



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

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