Как моделировать переменную swap в SMT (Z3)?

Question

У меня есть программа, которая сортирует переменные, и я пытаюсь проверить ее достоверность с Z3, но у меня есть один сегмент кода, где переменные меняются местами, и я не знаю, как смоделировать его в синтаксисе SMT. Вот исходный код сегмента:

if (x > y) { 
    temp = x; 
    x = y; 
    y = temp; 
} 

И относительно SMT я написал утверждение, но я предполагаю, что это не совсем правильно, что:

(declare-fun x() Int) 
(declare-fun y() Int) 
(declare-fun temp() Int) 

(assert (=> (> s1 s2) (and (= tmp s1) (= s1 s2) (= s2 tmp)))) 

Любые идеи, как сделать назначение переменной в SMT?

Answer 1

Вы должны изучить одностадийное назначение [1]. Таким образом, вы можете переписать исходный код следующим образом.

if (x0 > y0) { 
    temp0 = x0; 
    x1 = y0; 
    y1 = temp0; 
} 

Таким образом, становится ясно, что у вас есть два разных экземпляра x и y. Первый (x0, y0) - тот, который вы сравниваете в условии if. Второй (x1, y1) является результатом операции.

Это вводит неявное понятие времени, которое также упрощает запись свойств вашего кода. Например,

((x1 = x0) & (y1 = y0)) | ((x1 = y0) | (y1 = x0)) 

Конечно, это может потребовать корректировки других частей вашего кода, так что вы используете правильные переменные.

[1] https://en.wikipedia.org/wiki/Static_single_assignment_form

Answer 2

Мы можем переписать то, что вы хотите использовать одно выражение в виде кортежа:

(result1, result2) = x > y ? (x, y) : (y, x) 

Z3 поддерживает кортежи, но я менее опытен с этим. Это, наверное, проще взорвать это на части:

result1 = x > y ? x : y 
result2 = x > y ? y : x 

И в ?: оператора карты в ITE в Z3.

Для этого вам даже не нужны «временные переменные» (но, очевидно, вы можете).

(утверждают (=> (> s1 s2) (и (= TMP s1) (= s1 s2) (= s2 TMP))))

Я думаю, что это показательно, что вы не «Не понимаю, что Z3« переменные »на самом деле являются константами, и вы не можете их поменять. В каждой модели они принимают только одно значение. Для констант нет временной составляющей. = означает «равен?» а не «сделать его равным!».