У меня есть программа, которая сортирует переменные, и я пытаюсь проверить ее достоверность с Z3, но у меня есть один сегмент кода, где переменные меняются местами, и я не знаю, как смоделировать его в синтаксисе SMT. Вот исходный код сегмента:Как моделировать переменную swap в SMT (Z3)?
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?
Да, но как я могу использовать 'ite' для назначения, я имею в виду' ite' я могу сделать что-то вроде '(жет (<х) ху)', но как я могу убедитесь, что если 'x
typos
Вы понимаете, что вы вообще не можете назначать Z3? Значения и константы неизменяемы. '=' не присваивает. 'и' не присваивает. 'assert' не присваивает. – usr
Да, я понимаю, но я просто не понимаю, как я могу перевести свой выше сегмент кода в синтаксис SMT. Можете ли вы дать полный пример с 'ITE', как вы предложили, чтобы я мог видеть, что вы имеете в виду. Потому что то, что вы написали, имеет смысл, но я не вижу, как его перевести на SMT. – typos