Search code examples
z3bitvector

z3 bitvector operation simplified answer

Is there an easier way to get the immediate answers when doing bit-vector ops eg. a = 1 million, b = 0, what is a & b (answer: 0)

This method works but have to introduce dummy variable to store answer:

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(declare-const ans (_ BitVec 64))
(assert (= a (_ bv1000000 64)))
(assert (= b (_ bv0000000 64)))
(assert (= ans (bvand a b)))
(check-sat)
(get-model)

This method is what I'd like but my code gives a demorgan identity:

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(simplify (bvand a b))
Solution

  • You can use the model to evaluate arbitrary expressions, for instance like this:

    (declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(assert (= a (_ bv1000000 64)))
(assert (= b (_ bv0000000 64)))
(check-sat)
(eval (bvand a b))

    says

    sat
#x0000000000000000