Search code examples
z3smtbitvector

Expressing bitvectors with don't care in SMT

I want to define a function that takes in a bitvector and returns true if bits at certain position satisfy some values. Eg: I need to return true if bitvector is 1x00x01x where x denotes don't care.

My current implemntation is:

(define-fun function_i ((i (_ BitVec 8))) Bool
    (and true
        (= #b1 ((_ extract 1 1) i))
        (= #b0 ((_ extract 2 2) i))
        (= #b0 ((_ extract 4 4) i))
        (= #b0 ((_ extract 5 5) i))
        (= #b1 ((_ extract 7 7) i))
    )
)

This is for one variable and there could be many variables with 32 sized bitvectors. I am worried this kind of implementation slows down z3. Would the extract function slow down the solver? Is there a better way to implement this?

Solution

  • That's fine. A more compact way is (i & 1101) == 1000 (force first bit 1, 2nd 0 and last 0, 3rd bit can be 0 or 1)