title: Expressing bitvectors with don't care in SMT
body: <p>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.</p>
  
  <p>My current implemntation is:</p>
  
  <pre><code>(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))
      )
  )
  </code></pre>
  
  <p>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?</p>