I have a set of optimization problems in QF_BV. How can I efficiently solve them? For example, how can I use (check-sat-using (then simplify bit-blast) ...?
What follows is a fragment of a problem.
(declare-const p1_1 (_ BitVec 36))
(declare-const ps1_1 (_ BitVec 36))
(declare-const pe1_1 (_ BitVec 36))
(assert (= (_ bv0 36) (bvand ps1_1 (bvadd ps1_1 (_ bv1 36)))))
(assert (= (_ bv0 36) (bvand pe1_1 (bvadd pe1_1 (_ bv1 36)))))
(assert (and
(= p1_1 (bvxor ps1_1 pe1_1))
(not (= (_ bv0 36) (bvlshr ps1_1 (_ bv4 36))))
(=> (not (= p1_1 (_ bv0 36))) (= (concat ps1_1 #b1) (bvlshr (concat pe1_1 #b1) (_ bv4 37))))
))
(assert-soft (not (= p1_1 (_ bv0 36))) :weight 1)
(check-sat)
(get-model)
(get-objectives)
The optimizing engine (i.e., the engine that's used when you have assert-soft) doesn't work with tactics as far as I'm aware. It has its own solver and thus doesn't benefit from the general machinery of tactics.
You might want to ask and double check at https://github.com/Z3Prover/z3/discussions to see if there might be some other trick to orchestrate the behavior of the optimizing solver. (Though I doubt such a facility exists as of today.) Please report back here what you find!