Specifying initial model values for Z3

问题:

How to specify initial 'soft' values for the model? This initial model is the result of solving a similar query, and it is likely that this model has a correct pieces or even may be true for the current query.

Currently I am simulating this with an incremental solving and hard/soft constraints:

(define-fun trans_assumed ((a Int)) Int
; an initial model, which may be (partially) true
)

(declare-fun trans_sought ((a Int)) Int) 

(declare-const p Bool)
(assert (=> p (forall ((a Int)) (= (trans_assumed a) (trans_sought a)))))
(check-sat p) ; in hope that trans_assumed values will be used as initial below

; add here the main constraints for trans_sought function

(check-sat) ; Z3 will use trans_assumed as a starting point for trans_sought

Does this really specify initial values for trans_sought to be trans_assumed?

Incremental mode of solving is slow compared to sequential. Any better ways of introducing initial values?

回答1:

I think this is a good approach, but you may consider using more Boolean variables. Right now, it is a "all" or "nothing" approach. In your script, when (check-sat p) is executed, Z3 will look for a model where trans_assumed and trans_sought have the same interpretation. If such model does not exist, it will return with the unsat core containing p. When (check) is executed, Z3 is free to assign p to false, and the universal quantifier is essentially a don't care. That is, trans_assumed and trans_sought can be completely different.

If you use multiple Boolean variables to control the interpretation of trans_sought, you will have more flexibility. If the rest of your problem is quantifier free, you should consider dropping the universal quantifier. This can be done if you only care about the value of trans_sought in a finite number of points.

Suppose we have that trans_assumed(0) = 1 and trans_assumed(1) = 10. Then, we can write:

assert (=> p0 (= (trans_sought 0) 1)))
assert (=> p1 (= (trans_sought 1) 10)))

In this encoding, we can query (check-sat p0 p1), (check-sat p0), (check-sat p1)