1

QF_NRA 中是否包含除以零？

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

- 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和的函数t2。

事实上，除以零似乎包含在 SMT-LIB 中，尽管声明只有非零时才是(/ m n)实数。n这与我之前的一个问题有关：y=1/x, x=0 在实数中是否可以满足？

4

1 回答 1

0

第一个引号说 (/ m 0) 不是数字

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

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

这是对的。

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

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

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

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

于 2016-10-21T20:05:58.870 回答