Z3 Bedingte Anweisung

Question

Wie schreibe ich eine bedingte Anweisung in Z3.

eg: 
if (a%2==0){ 
value=1 
} 

Ich versuche, dies in Z3 Solver von Microsoft Research zu erreichen, aber bisher kein Glück

Answer 1

nachschlagen SSA Form: https://en.wikipedia.org/wiki/Static_single_assignment_form

Im Wesentlichen werden Sie Ihr Programm ändern müssen schauen so etwas wie:

value_0 = 0 
value_1 = (a%2 == 0) ? 1 : value_0 

Sobald es in dieser so genannten statischen Einzelzuordnung Form ist, können Sie nun jede Zeile mehr übersetzen oder weniger direkt; mit der letzten Zuweisung an value_N ist der Endwert von value.

Loops werden problematisch sein: Die übliche Strategie ist es, sie bis zu einer bestimmten Anzahl zu entrollen (beschränkte Modellprüfung), und hoffe, dass dies ausreicht. Wenn Sie feststellen, dass das letzte Abrollen nicht ausreicht, können Sie an dieser Stelle einen nicht interpretierten Wert generieren. was dazu führen könnte, dass Ihre Beweise mit falschen Gegenbeispielen versagen; Aber das ist das Beste, was Sie ohne ein Schema tun können, das den richtigen Umgang mit Induktions- und Loop-Invarianten beinhaltet.

Beachten Sie, dass dieses Studiengebiet "symbolische Ausführung" genannt wird und eine lange Geschichte hat, mit aktiver Forschung wird immer noch durchgeführt. Vielleicht möchten Sie Folgendes durchlesen: https://en.wikipedia.org/wiki/Symbolic_execution