Wrong range for ex4

[LouisCaixuran]

Hi,

I tried the benchmark ex4 and got the following result

python3 src/exp_use_default.py ex4_gaussian
RESULTS for ex4_gaussian
Volume: 0.02
Took 2.48 seconds to generate the invariant. Confirmed for FP: OK.
Ranges: {'x0': (-0.2, 0.2), 'x1': (-0.1, 0.2), 'x2': (-0.2, 0.1)}
Invariant: 0.04*x0 + -0.07*x1 + 0.5*x0^2 + -1.0*x0*x1 + -0.58*x0*x2 + 0.84*x1^2 + 0.28*x1*x2 + 0.63*x2^2 <= 0.01

However, seems the range is not correct

x0=0
x1=0
x2=0
in0=-0.8


for i in range(100):
    x0 = 0.9379 * x0 - 0.0381 * x1 - 0.0414 * x2 + 0.0237 * in0 
    x1 = -0.0404 * x0 + 0.968 * x1 - 0.0179 * x2 + 0.0143 * in0
    x2 = 0.0142 * x0 - 0.0197 * x1 + 0.9823 * x2 + 0.0077 * in0


print("x0:", x0)
print("x1:", x1)
print("x2:", x2)

would give the following result

x0: -0.07220538508329073
x1: -0.08225353230561162
x2: -0.2951334698552336

where x2 is out of range.

I wonder if there is any guarantee that the range of pine would always be correct? If yes, i wonder if this is a bug?

[izycheva]

Thanks for reporting! It was indeed a bug, the solver returned "UNKNOWN" for the candidate invariant, and because of some copy-paste error it wasn't caught. The invariant shouldn't have been confirmed.

[LouisCaixuran]

Thanks a lot for the update. Just for a double check, it seems after fixing the bug, there is no invarianet found for ex4-ex8 in the benchmark?

[izycheva]

It is possible, in general, Pine's procedure is incomplete, so it may miss some invariants even if they exist.

It seems, for ex4 benchmark the bug is somewhere in the solver API, because while the API returns 'UNKNOWN', the command line Z3 returns 'SAT'. I opened an issue in Z3 repo, let's see what they say. Meanwhile I have a workaround in mind, but I need a bit of time to implement and test it, since Pine is my free-time project :).

Note also that for the experiments in the paper describing Pine we used a different version of the solver (the one available in 2020) and I do not recall having any 'UNKNOWN's in the logs back then.