CODEWITHSUNDEEP
z3smtreliability
Shadow
Shadow

Reputation: 5

Anyone know how to covert a signed bitvector to signed int in Z3?

(>  (bv2int (bvxor ((_ int2bv 32) x1) ((_ int2bv 32) y1))) 0)

x1 and y1 is two signed int, and after the xor. How can i convert them back as a signed int?

Upvotes: 0

Views: 284

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

You can use int2bv and bv2int, but for the most part, those functions will be treated as uninterpreted (see e.g. the API doc). If you need the actual semantics, you will have to implement them yourself. It's not at all hard (just a big sum over if-then-elses of 2^i*x1[i] terms), but the constraints you obtain this way are highly non-linear, so it's likely that the integer theory will give up and return unknown. See for instance Z3 Performance with Non-Linear Arithmetic, How does Z3 handle non-linear integer arithmetic?, and Z3 : Questions About Z3 int2bv?.

Upvotes: 1

Related Questions