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

У меня есть программа, которая сортирует переменные, и я пытаюсь проверить ее правильность с помощью 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?


z3 smt formal-verification
person typos    schedule 29.10.2016    source источник

Ответы (2)


arrow_upward
4
arrow_downward

Вы должны изучить Single Static Assignment [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

person Marco    schedule 30.10.2016

arrow_upward
0
arrow_downward

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

(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 на самом деле являются константами, и вы не можете их поменять местами. В каждой модели они принимают только одно значение. В константах нет временной составляющей. = означает "равно?" а не "сделать равным!".

person usr    schedule 29.10.2016
comment
Да, но как я могу использовать ite для присваивания, я имею в виду, что в ite я могу сделать что-то вроде (ite (< x y) x y), но как я могу гарантировать, что если x < y, то значение результата действительно равно x? - person typos; 29.10.2016
comment
Вы понимаете, что в Z3 вообще нельзя назначать? Значения и константы неизменяемы. = не назначает. and не назначает. assert не назначает. - person usr; 29.10.2016
comment
Да, я понимаю, но я просто не понимаю, как я могу перевести мой сегмент кода выше в синтаксис SMT. Можете ли вы привести полный пример с ITE, как вы предложили, чтобы я мог понять, что вы имеете в виду. Потому что то, что вы написали, имеет смысл, но я не вижу, как это перевести на SMT. - person typos; 30.10.2016
comment
Хорошо, перевод прямолинейный. Непроверено: (ite (> s1 s2) s1 s2) как выражение для result1 (или как там его зовут). Вам не нужно объявлять константу. Вы можете просто использовать это выражение, которое обычно проще. Но если вам нужна/хотите константу: (declare-fun result1 () Int) (assert (= result1 (ite (> s1 s2) s1 s2))). Как это. - person usr; 30.10.2016