QF_NRA 中是否包含除以零？

Question

QF_NRA 中是否包含被零除？

SMT-LIB 标准在这件事上令人困惑。 paper where the standard is defined 根本没有讨论这一点，实际上 NRA 和 QF_NRA 并没有出现在该文档的任何地方。在standard website 上提供了一些信息。实数的定义包括：

- all terms of the form (/ m n) or (/ (- m) n) where 
  - m is a numeral other than 0,
  - n is a numeral other than 0 and 1,
  - as integers, m and n have no common factors besides 1.

当涉及到常量值时，这会从分母中明确排除零。但是，后来，除法被定义为：

- / as a total function that coincides with the real division function 
  for all inputs x and y where y is non-zero,

接下来是一个注释：

Since in SMT-LIB logic all function symbols are interpreted as total
  functions, terms of the form (/ t 0) *are* meaningful in every 
  instance of Reals. However, the declaration imposes no constraints
  on their value. This means in particular that 
  - for every instance theory T and
  - for every closed terms t1 and t2 of sort Real, 
  there is a model of T that satisfies (= t1 (/ t2 0)). 

这似乎是矛盾的，因为第一个引用说 (/ m 0) 不是 QV_NRA 中的数字，但后一个引用说 / 是一个函数，使得 (= t1 (/ t2 0)) 可以满足任何 t1 和 @ 987654331@.

事实上，除以零似乎包含在 SMT-LIB 中，尽管声明 (/ m n) 仅在 n 非零时才为实数。这与我之前的一个问题有关：y=1/x, x=0 satisfiable in the reals?

Answer 1

第一句话说 (/m 0) 不是数字

没有，但它没有说明它是什么数字。

但后面的引用说 / 是一个函数，使得 (= t1 (/t2 0)) 对于任何 t1 和 t2 都可以满足

这是正确的。

您需要摆脱“不允许被零除！”的学校心态。它是未定义的。未定义意味着没有公理指定这是什么值。 （在学校也是如此。）

f(1234) 是什么？它是未定义的，所以 Z3 可以选择任何数字。 a / 0 和 f(a) 之间没有区别，其中 f 是一些未解释的函数。 Z3可以填写任何它喜欢的功能。

因此，a / 0 == b 是可满足的，任何a 和b 都可以。但是(a / 0) == (a / 0) + 1 是假的。

数学运算符只是函数。该标准部分指定了这些功能。