2

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?

Community
  • 1
  • 1
Ayrat
  • 1,221
  • 1
  • 18
  • 36

1 Answers1

3

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)

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Oh, sounds interesting! As i understood, you suggest to fine-grain assumptions about equal pieces of models. But this may result in many `check-sat p..` calls with different assumptions. That may be expensive(hm, questionable since it is incremental). I am trying to avoid this and let Z3 heuristics to choose what pieces of the model should remain. it is OK if `trans_assumed` and `trans_sought` are completely different! i just want Z3 to start with `trans_assumed` and then Z3 can _tweak_ it using its own heuristics. Will Z3 tweak `trans_assumed` or it startS with a completely new one? – Ayrat Mar 28 '12 at 10:47
  • 1
    Z3 will create a new model for `(check-sat)`, but it will re-use the lemmas learned in the first `(check-sat p)`. However, any lemma that depends on `p` will be automatically disabled if Z3 assigns `p` to `false`. The use of randomization may also be an issue. I think you may end with a unstable solution (i.e., it doesn't always work). – Leonardo de Moura Mar 28 '12 at 15:03