y = 1/x、x = 0実数で充足可能か？ SMT-LIBでは

Question

：

(declare-fun y() Real) 
(declare-fun x() Real) 
(assert (= 0.0 x)) 
(assert (= y (/ 1.0 x))) 
(check-sat) 

このモデルは、土やUNSATべきか？

Answer 1

SMT-LIB 2.0および2.5では、すべての機能が合計であるため、この例はSMT-LIBのSATです。 Z3とCVC4の両方は、質問の例で実際にSATを返します。

私はこれを直感的に見つけました。私はy=1/x, x=0が実際には満足できないと言っても、それは数学的にはより正当だと思う。 Mathematicaでは、同等のコード、すなわち、それにもかかわらずFindInstance[Element[x, Reals] && Element[y, Reals] && x == 0 && y == 1/x, {x, y}]戻り{}

、/is defined this way in SMT-LIB、解が存在しないことを示す、空のリストを返します。したがって、Z3またはCVC4に関する限り、この問題はSATです。