Better BV quantifier instantiation

[nunoplopes]

Z3 doesn't finish on the following test case unless you reduce the bit-width to 8. This is from one of our benchmarks and our tactic can't do it either.

(declare-fun isundef_%b () (_ BitVec 1))
(declare-fun isundef_%a () (_ BitVec 1))
(declare-fun undef!3 () (_ BitVec 32))
(declare-fun undef!2 () (_ BitVec 32))
(declare-fun np_%b () Bool)
(declare-fun np_%a () Bool)

(assert (let ((a!1 (forall ((undef!0 (_ BitVec 32)) (undef!1 (_ BitVec 32)))
             (! (not (or (not (and np_%a np_%b)) (= undef!0 undef!2)))
                :weight 0)))
      (a!2 (forall ((undef!0 (_ BitVec 32)) (undef!1 (_ BitVec 32)))
             (! (not (or (not (and np_%a np_%b)) (= undef!1 undef!3)))
                :weight 0)))
      (a!3 (forall ((undef!0 (_ BitVec 32)) (undef!1 (_ BitVec 32)))
             (! (not (or (not (and np_%a np_%b))
                         (= (bvadd undef!0 undef!1) (bvadd undef!2 undef!3))))
                :weight 0))))
  (or (and a!1 (= isundef_%a #b1) (= #b0 isundef_%b))
      (and a!2 (= #b0 isundef_%a) (= isundef_%b #b1))
      (and a!3 (= isundef_%a #b1) (= isundef_%b #b1)))))
(check-sat)

One thing is realize is that (bvadd x y) can take any value if x,y are unconstrained. It seems Z3 doesn't know this trick. Most BV functions have similar behavior that we could take advantage of.

@NikolajBjorner feel free to close this if you feel this is not easily actionable. You know better the qe-light/qe algorithms to know if we can plugin this trick easily or not. Thank you!

[NikolajBjorner]

z3 nuno.smt2 /v:10 sat.euf=true /st
boom

[NikolajBjorner]

qe_lite uses mbp::bv_solve_plugin defined in qe/mbp_solve_plugin.cpp. it could be extended to solve equations of forms other than the current setting.