1

Is division by zero included in QF_NRA?

The SMT-LIB standard is confusing in this matter. The 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. Reals are defined as including:

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

This explicitly excludes zero from the denominator when it comes to constant values. However, later, division is defined as:

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

This is followed up by a note:

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)).

This is seemingly contradictory, because the first quote says that (/ m 0) is not a number in QV_NRA, but the latter quote says that / is a function such that (= t1 (/ t2 0)) is satisfiable for any t1 and t2.

The de-facto reality on the ground is that division by zero seems to be included in SMT-LIB, despite the statement that (/ m n) is only a Real number if n is nonzero. This is related to a previous question of mine: y=1/x, x=0 satisfiable in the reals?

Douglas B. Staple
  • 10,510
  • 8
  • 31
  • 58

1 Answers1

0

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

No, but it does not say what number it is.

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

This is correct.

You need to get away from the school mentality that says "division by zero is not allowed!". It is undefined. Undefined means that there is no axiom that specifies what values this is. (And this is true in school as well.)

What is f(1234)? It's undefined, so Z3 is allowed to pick any number at all. There is no difference between a / 0 and f(a) where f is some uninterpreted function. Z3 can fill in any function it likes.

Therefore, a / 0 == b is satisfiable and any a and b are OK. But (a / 0) == (a / 0) + 1 is false.

Mathematical operators are just functions. The standard partially specifies those functions.

usr
  • 168,620
  • 35
  • 240
  • 369
  • I don't have a grade-school mentality about division by zero, I understand that we can define it however we like. I think the standard is poorly worded and confusing as to _how_ `(/ m 0)` is defined _in SMT-LIB_, specifically regarding whether or not `(/ m 0)` is a Real in SMT-LIB. Besides the advice regarding what I "need" to do, this answer is correct. – Douglas B. Staple Oct 23 '16 at 17:08
  • The mistake was me misinterpreting the first quote as implying that `(/ m 0)` is not a Real _in SMT-LIB_. The first quote is from the definition of what _is_ a Real, and makes no statement about what is not a Real. So as far as I can tell, they could have omitted the bit where they said "m is a numeral other than 0". – Douglas B. Staple Oct 23 '16 at 17:10
  • Many people think that division by zero ist "off limits" so may this answer help future visitors. It seemed you were sharing that belief but your statements were about m/0 not being a real at all (which I know nothing about but your interpretation seems correct). It's also architecturally required by the Z3 data structures to assign each term a sort. There is no sort for "any mathematical object at all". Also, if m/0 was not a real then the sort would depend on model values and in general not be determined to be a particular sort. – usr Oct 23 '16 at 18:16