Angeben anfänglicher Modellwerte für Z3

Question

Wie werden anfängliche "weiche" Werte für das Modell angegeben? Dieses anfängliche Modell ist das Ergebnis der Lösung einer ähnlichen Abfrage, und es ist wahrscheinlich, dass dieses Modell über korrekte Teile verfügt oder sogar für die aktuelle Abfrage wahr sein kann.

Derzeit bin simuliert ich dies mit einer inkrementellen Lösung und 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 

Ist dies wirklich die Anfangswerte für trans_sought angeben trans_assumed zu sein?

Inkrementeller Modus des Lösens ist langsam im Vergleich zu sequenziellen. Gibt es bessere Möglichkeiten, erste Werte einzuführen?

Answer 1

Ich denke, das ist ein guter Ansatz, aber Sie können mehr boolesche Variablen verwenden. Im Moment ist es ein "Alles" oder "Nichts" Ansatz. Wenn in Ihrem Skript (check-sat p) ausgeführt wird, sucht Z3 nach einem Modell, bei dem trans_assumed und trans_sought dieselbe Interpretation haben. Wenn ein solches Modell nicht existiert, kehrt es mit dem ungesättigten Kern zurück, der enthält. Wenn (check) ausgeführt wird, ist Z3 frei, zu false zuzuordnen, und der universelle Quantifizierer ist im Wesentlichen ein egal. Das heißt, trans_assumed und trans_sought können völlig unterschiedlich sein.

Wenn Sie mehrere boolesche Variablen verwenden, um die Interpretation von trans_sought zu steuern, haben Sie mehr Flexibilität. Wenn der Rest Ihres Problems frei von Quantifizierern ist, sollten Sie den universellen Quantifizierer entfernen. Dies kann gemacht werden, wenn Sie nur den Wert von trans_sought in einer endlichen Anzahl von Punkten interessieren.

Angenommen, wir haben das trans_assumed(0) = 1 und trans_assumed(1) = 10. Dann können wir schreiben:

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

In dieser Codierung können wir (check-sat p0 p1), fragen (check-sat p0), (check-sat p1)