Herbie fails on multi variable input about herbie HOT 11 CLOSED

This sounds like a problem in our mixed-precision support. I'll take a look!

from herbie.

@pavpanchekha
Similar issue, tried with double precision, it works, single precision, fails. Note input is the same with out the first half (-((az - dz) - (vz/vx) * (ax - dx)) - ((bz - az) - in the numerator.

(((bz - az) - ((vz/vx) * (bx - ax)))*gz) / (((dz - cz) - (bz - az)) - (vz/vx) * ((dx - cx) - (bx - ax)))*gz + ((cz - az) - (vz/vx) * (cx - ax))

herbie shell --seed 2042407083 
(FPCore (bz az vz vx bx ax gz dz cz dx cx)
  :name "(((bz - az) - ((vz/vx) * (bx - ax)))*gz) / (((dz - cz) - (bz - az)) - (vz/vx) * ((dx - cx) - (bx - ax)))*gz + ((cz - az) - (vz/vx) * (cx - ax))"
  (+ (* (/ (* (- (- bz az) (* (/ vz vx) (- bx ax))) gz) (- (- (- dz cz) (- bz az)) (* (/ vz vx) (- (- dx cx) (- bx ax))))) gz) (- (- cz az) (* (/ vz vx) (- cx ax)))))

flonum->ordinal: contract violation expected: Float given: +inf.f in: the 1st argument of (-> Float any) contract from: <pkgs>/math-lib/math/private/flonum/flonum-bits.rkt blaming: <pkgs>/herbie/interface.rkt (assuming the contract is correct) at: <pkgs>/math-lib/math/private/flonum/flonum-bits.rkt:9.9 L C

from herbie.

Thanks for the nice test cases. We're working on it!

from herbie.

Hi @Cazadorro. I think I've fixed the issue you were seeing. I was having a bit of trouble reproducing your exact error, but I believe I've tracked down what was causing the issue. Let me know if the latest version fixes it. Thanks!

from herbie.

@DavidThien It now claims it cannot sample enough valid points with both inputs for single precision, again, both appear to work for double precision with out such an issue.

from herbie.

Hi @Cazadorro, I'm swapping back in for @DavidThien since he's going camping for a few days. I took a quick look and with varying seeds it seems that the single-precision version usually samples fine—is that not what is happening for you? Usually "Cannot sample enough valid points" is best solved by adding a precondition giving ranges for the various variables. Even if you don't have precise ranges, adding loose ones usually helps: maybe the max value for az isn't totally clear, but it's definitely less than 100, for example. A combination of lower and upper bound usually helps the most.

from herbie.

Ah—I'm guessing you're running these online. To get @DavidThien's fixes you'll need to run Herbie from source; you can find instructions online and it isn't too hard. We usually only restart the online demo every release, to avoid freezing out users if something goes wrong.

from herbie.

@pavpanchekha I was not running these online, I ran them locally via herbie web, at first I used rackets package manager to download, then I cloned the repo, removed the package, then added herbie again according to the instructions based on the cloned repo. But now that I think about it I might have forgotten to change branches to what ever the latest was. Is there a need to switch branches? if so I'll update later tonight.

from herbie.

@pavpanchekha Also there are no ranges for these variables, except for the vz vx variables. These variables are actually based on this GLSL equation:

float solve_for_g(
const in vec3 a, 
const in vec3 b, 
const in vec3 c, 
const in vec3 d, 
const in ScreenRay ray,
in float f){
    vec3 A = b-a;
    vec3 B = c-a;
    vec3 C = (d-c) - (b-a);
    vec3 D = a - ray.origin;

    float vy_x = ray.direction.y / ray.direction.x;
    float vz_x = ray.direction.z / ray.direction.x;
    float Ayx = (A.y - vy_x * A.x); 
    float Byx = (B.y - vy_x * B.x); 
    float Cyx = (C.y - vy_x * C.x); 
    float Dyx = (D.y - vy_x * D.x); 

    float Azx = (A.z - vz_x * A.x); 
    float Bzx = (B.z - vz_x * B.x); 
    float Czx = (C.z - vz_x * C.x); 
    float Dzx = (D.z - vz_x * D.x);

    return (-Dzx - Azx*f) / (Czx*f + Bzx);
}

where a, b,c,d are arbitrary points, each pair corresponding to a line, and ray direction being normalized overall.

In the equation above. az = A.z, bz = B.z, cz = C.z, dz = D.z and so on and so forth. vz corresponding to ray.direction.z etc, gz corresponds with f ... It is really jus the expanded form of

(-Dzx - Azx*f) / (Czx*f + Bzx);

eg:

(-((A.z - D.z) - (ray.direction.z/ray.direction.x) * (A.x - D.x)) - ((B.z - A.z) - ((ray.direction.z/ray.direction.x) * (B.x - A.x)))*f) / (((D.z - C.z) - (B.z - A.z)) - (ray.direction.z/ray.direction.x) * ((D.x - C.x) - (B.x - A.x)))*f + ((C.z - A.z) - (ray.direction.z/ray.direction.x) * (C.x - A.x))
There's nothing I can really do about restricting the range on the A,B,C,D parameters,

f (aka gz) should be between 0 and 1, ray.direction.xyz (or vx,vy,vz) should all be between -1 and 1, but it would be great to have some sort of normalization constraint as well (since I know ray.direction is normalized). These are the only constraints to be applied.

from herbie.

I'm not sure exactly what branch you're on, but current master seems to work for me (commit f316bcef3de0492d34dcdbc4c663eb04d00305c4). If the variables don't have ranges, there's not much you can do for those. It's still worth adding the ranges for the variables you have (f and gz?). For vx, vy, and vz, you can give arbitrary mathematical expressions for the precondition, but I would give ranges as well, since Herbie isn't too smart and since ranges help it out a lot. So maybe your precondition would be -1 <= vx <= 1 and -1 <= vy <= 1 and -1 <= vz <= 1 and vx*vx + vy*vy + vz*vz <= 1

from herbie.

Hi @Cazadorro just wanted to follow up to see if the issue was fixed after doing the trick. Herbie isn't very smart in how it samples points right now, so it isn't always able to find enough. This is definitely something that we're looking to improve in the future, but for now, tricks like adding in preconditions can help a lot.

from herbie.