QF_NRA 中是否包含被零除？

Question

QF_NRA中是否包含被零除？

SMT-LIB 标准在这件事上令人困惑。 paper where the standard is defined simply does not discuss this point, in fact NRA and QF_NRA do not appear anywhere in that document. Some information is provided on the 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 和 t2.

实际情况是 SMT-LIB 中似乎包含被零除，尽管声明如果 n 不为零，(/ m n) 只是一个实数。这与我之前的一个问题有关：

Answer 1

the first quote says that (/ m 0) is not a number

没有，但没有说明是什么号码。

but the latter quote says that / is a function such that (= t1 (/ t2 0)) is satisfiable for any t1 and t2

这是正确的。

你需要摆脱那种说 "division by zero is not allowed!" 的学校心态。它是未定义的。未定义意味着没有指定这是什么值的公理。（在学校也是如此。）

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

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

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

QF_NRA 中是否包含被零除？

Is division by zero included in QF_NRA?

theorem-proving

smt

z3

cvc4