у = 1 / х, х = 0 выполнимо в реалах?
В SMT-LIB:
(declare-fun y () Real)
(declare-fun x () Real)
(assert (= 0.0 x))
(assert (= y (/ 1.0 x)))
(check-sat)
Должна ли эта модель быть SAT или UNSAT?
Ответы на вопрос(1)
Решение Вопроса
поэтому этот пример - SAT в SMT-LIB. И Z3, и CVC4 действительно возвращают SAT для примера в вопросе.
Я нашел это нелогичным. Я думаю, что было бы математически более оправданным сказать, чтоy=1/x, x=0 неудовлетворительно в реалах. В Mathematica эквивалентный код возвращает пустой список, указывающий на то, что решения не существует, т.е.FindInstance[Element[x, Reals] && Element[y, Reals] && x == 0 && y == 1/x, {x, y}] возвращается{}
Тем не менее,/ определяется таким образом в SMT-LIB, Итак, что касается Z3 или CVC4, эта проблема - SAT.
Да, именно так SMT определяет эти операторы / функции. Повторяющаяся тема, которая всегда имеет ровно 50% сторонников и 50% противников :)
Большое спасибо, Кристоф. Я столкнулся с этим, пытаясь выяснить, или нет
(and (= y (^ x 0.5)) (< x 0.0)) должно быть SAT или UNSAT. Для согласованности с остальной частью SMT, я думаю, этот пример sqrt также должен быть SAT. Теперь мне просто нужно выяснить, как заставить Z3 на самом деле дать SAT для этого примера sqrt.