у = 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.

 Christoph Wintersteiger29 июн. 2016 г., 21:16
Да, именно так SMT определяет эти операторы / функции. Повторяющаяся тема, которая всегда имеет ровно 50% сторонников и 50% противников :)
 Douglas B. Staple29 июн. 2016 г., 21:26
Большое спасибо, Кристоф. Я столкнулся с этим, пытаясь выяснить, или нет(and (= y (^ x 0.5)) (< x 0.0)) должно быть SAT или UNSAT. Для согласованности с остальной частью SMT, я думаю, этот пример sqrt также должен быть SAT. Теперь мне просто нужно выяснить, как заставить Z3 на самом деле дать SAT для этого примера sqrt.

Ваш ответ на вопрос