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.Angeben anfänglicher Modellwerte für Z3
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?
Oh, klingt interessant! Wie ich verstanden habe, schlagen Sie feinkörnige Annahmen über gleiche Teile von Modellen vor. Dies kann jedoch zu vielen "check-sat p.." -Aufrufen mit unterschiedlichen Annahmen führen. Das kann teuer sein (hm, fragwürdig, da es inkrementell ist). Ich versuche das zu vermeiden und lasse Z3-Heuristiken entscheiden, welche Teile des Modells erhalten bleiben sollen. es ist in Ordnung, wenn 'trans_assumed' und' trans_sought' völlig verschieden sind! Ich möchte nur, dass Z3 mit 'trans_assumed' beginnt und dann Z3 kann es mit seinen eigenen Heuristiken. Wird Z3 'trans_assumed' optimieren oder beginnt es mit einem komplett neuen? – Ayrat
Z3 wird ein neues Modell für '(check-sat)' erstellen, aber es wird die Lemmas wiederverwenden, die im ersten '(check-sat p)' gelernt wurden. Jedoch wird jedes Lemma, das von 'p' abhängt, automatisch deaktiviert, wenn Z3' p' zu 'false' zuweist. Die Verwendung von Randomisierung kann ebenfalls ein Problem sein. Ich denke, Sie können mit einer instabilen Lösung enden (d. H. Es funktioniert nicht immer). –