Is it possible to use both bit-blast and soft-assert with the z3 solver?

I'm trying to use the z3 smt solver to allocate values to variables subject to constraints. As well as hard constraints I have some soft constraints (e.g. a != c). I expected to be able to specify the hard constraints with assert and the soft constraints as soft-assert and this works if I solve with (check-sat).

Some of the files are large and complex and only solve in a reasonable time if I turn on bit-blasting using (check-sat-using (then simplify solve-eqs bit-blast sat)). When I do this the soft asserts seem to be ignored (example below or at rise4fun). Is this expected? Is it possible to use both bit-blast solving and soft-assert at the same time?

The following SMT code defines 4 bitvectors, a, b, c & d which should all be able to take unique values but are only forced to do so by soft asserts. Using the check-sat (line 39) works as expected but the check-sat-using (line 38) assigns b and d to the same value.

(set-option :produce-models true)
(set-logic QF_BV)

;; Declaring all the variables
(declare-const a (_ BitVec 2))
(declare-const b (_ BitVec 2))
(declare-const c (_ BitVec 2))
(declare-const d (_ BitVec 2))

(assert (or (= a #b00)
            (= a #b01)
            (= a #b10)
            (= a #b11)))

(assert (or (= b #b00)
            (= b #b01)
            (= b #b10)
            (= b #b11)))

(assert (or (= c #b00)
            (= c #b01)
            (= c #b10)
            (= c #b11)))

(assert (or (= d #b00)
            (= d #b01)
            (= d #b10)
            (= d #b11)))

;; Soft constraints to limit reuse
(assert-soft (not (= a b)))
(assert-soft (not (= a c)))
(assert-soft (not (= a d)))
(assert-soft (not (= b c)))
(assert-soft (not (= b d)))
(assert-soft (not (= c d)))

(check-sat-using (then simplify solve-eqs bit-blast sat))
;;(check-sat)
(get-value (a
            b
            c
            d))

Solution

Great question! When you use assert-soft the optimization engine kicks in by default. You can see this by using your program with the (check-sat) clause, and running with higher verbosity. I've put your program in a file called a.smt2:

$ z3 -v:3 a.smt2
(optimize:check-sat)
(sat.solver)
(optimize:sat)
(maxsmt)
(opt.maxres [0:6])
(sat.solver)
(opt.maxres [0:0])
found optimum
sat
((a #b01)
 (b #b00)
 (c #b11)
 (d #b10))

So, we can see z3 is treating this as an optimization problem, which takes soft-constraints into account and gives you the "disjointness" you're seeking.

Let's do the same, but this time we'll use the check-sat call that specifies the tactics to use. We get:

$ z3 -v:3 a.smt2
(smt.searching)
sat
((a #b11)
 (b #b11)
 (c #b11)
 (d #b10))

And this confirms your suspicion: When you tell z3 exactly what to do, it doesn't do the optimization pass. In hindsight, this is to be expected, but I do agree that it's rather surprising.

The question is then whether we can tell z3 to do the optimization explicitly. However I'm not sure if this is even possible within the tactic language. I think this question is well worthy of asking at their issues site (https://github.com/Z3Prover/z3/issues) and see if there's a magic incantation you can use to kick off the maxres engine from the tactic language. (This may not be possible due to a number of reasons, but there's no reason to speculate here.) Please report back here what you find out!