error bounding norm: num_of_float: inf

[smcallis]

I'm trying to bound this program, which crosses two vectors and then crosses those results to get the sin of the angle between them:

Variables
  real x0 in [0,1.0000000000000004];
  real y0 in [0,1.0000000000000004];
  real z0 in [0,1.0000000000000004];

  real x1 in [0,1.0000000000000004];
  real y1 in [0,1.0000000000000004];
  real z1 in [0,1.0000000000000004];

  real x2 in [0,1.0000000000000004];
  real y2 in [0,1.0000000000000004];
  real z2 in [0,1.0000000000000004];

  real x3 in [0,1.0000000000000004];
  real y3 in [0,1.0000000000000004];
  real z3 in [0,1.0000000000000004];  

Expressions
  c00 rnd64= +(y0*z1-z0*y1);                      // |i j  k |  
  c01 rnd64= -(x0*z1-z0*x1);                      // |x0 y0 z0|
  c02 rnd64= +(x0*y1-y0*x1);                      // |x1 y1 z1|

  c10 rnd64= +(y2*z3-z2*y3);                      // |i  j  k |  
  c11 rnd64= -(x2*z3-z2*x3);                      // |x2 y2 z2|
  c12 rnd64= +(x2*y3-y2*x3);                      // |x3 y3 z3|

  c0 rnd64 = +(c01*c12-c02*c11);                  // |i   j   k  |
  c1 rnd64 = -(c00*c12-c02*c10);                  // |c00 c01 c02|
  c2 rnd64 = +(c00*c11-c01*c10);                  // |c10 c11 c12|
  
  norm2 = c0*c0+c1*c1+c2*c2;
  norm  = sqrt(c0*c0+c1*c1+c2*c2);

It seems to do fine until it gets to norm() and then it errors out with:

**ERROR**: num_of_float: inf

But I don't think those terms should ever be infinite, so I'm wondering if I'm doing something obviously wrong.

[monadius]

Nothing is wrong in your example. But it cannot be analyzed by FPTaylor because the expression under the square root can be 0. FPTaylor needs to find derivatives to compute error bounds. But the derivative of sqrt(x) is not defined when x = 0. Moreover, FPTaylor computes the following bounds for norm2: [-2.552581e-14, 9.703126] (with --opt-max-iters=100000). FPTaylor does not apply monotonicity rounding rules so it cannot prove that rnd(x * x) >= 0 for all x.

I am leaving this issue open because this issue should be fixed eventually. Probably, it will be necessary to implement a case analysis for sqrt(x) and similar functions and apply different error bounding rules for cases when x is close to 0 and when x >= eps > 0 for some eps.

[smcallis]

Thank you for the quick response =D. That makes sense that the derivative is undefined there..