Assertion failure in "src/lib/reasoners/intervalCalculus.ml", line 1175, when using the CDCL solver

[hra687261]

c_262_0_ae_bis.ae.txt

Running Alt-Ergo (built from the "next" branch) on the attached file with the command:

./alt-ergo --sat-solver CDCL c_262_0_ae_bis.ae

Causes the following error:

Fatal error: exception File "src/lib/reasoners/intervalCalculus.ml", line 1175, characters 4-10: Assertion failed

And when the other solvers are used (by replacing CDCL with Tableaux or Tableaux-CDCL or CDCL-Tableaux) then Alt-Ergo responds with "Valid".

Some additional interesting points:

• if we remove the axioms ax_1 and ax_2, then the answer in the four cases is:"I don't know".
• if we replace (ruqv0 * ruqv0) * (if true then ruqv0 else ur_3) in the line 14 with (ruqv0 * ruqv0) * ruqv0 or (ruqv0 * ruqv0), then AE takes too long to answer (more than 3 minutes) when the CDCL solver is used. And answers with "Valid" in the other cases.
• if we replace it with ruqv0 then the answer is "Valid" in every case.
• if we replace it with ur_3 then AE says:"I Don't Know" when the CDCL solver is used, and "Valid" in the other cases.

[bclement-ocp]

the test case in the issue is hidden by #731 but the underlying cause is probably still valid.

[bclement-ocp]

The assertion failure looks to be related to confusion in intervalCalculus about class representatives. The intervalCalculus environment is not consistent in the way it represents e.g. ur_0 * ur_0: sometimes it is the AC-term ur_0 * ur_0, and sometimes it is the purified constant !?__let2((ur_0 * ur_0)) introduced by AC(X), which is the "true" class representative.

More precisely, there is an inequality ('*' is the AC symbol for multiplication, * with no quotes is the polynomial multiplication):

-ur_0'*'ur_0'*'ur_0+ur_0+1<=0

and the normalized polynomial is tracked:

ur_0'*'ur_0'*'ur_0-ur_0 : [1;+inf[

But ur_0'*'ur_0 has !?__let2((ur_0 * ur_0)) for representative, and so in assume (around line 1740) we remove the normalized polynomial from the list of tracked polynomials — but we keep the inequality.

It is not entirely clear to me what the fix should be. I don't think we should have polynomials with non-normalized terms lying around (and the code in assume seems to agree, since it removes non-normalized polynomials from the map), but I need to look further into where a normalization step is missing.

[bclement-ocp]

I don't think we should have polynomials with non-normalized terms lying around

--enable-assertions confirms this:

$ alt-ergo --sat-solver CDCL --enable-assertions c_262_0_ae_bis.ae
[Error]-ur_0'*'ur_0'*'ur_0+ur_0+109/50 <= 0 NOT normalized
       It is equal to -!?___let2((ur_0 * ur_0))'*'ur_0+ur_0+109/50
Fatal error: exception File "src/lib/reasoners/intervalCalculus.ml", line 1336, characters 10-16: Assertion failed

[bclement-ocp]

Here is a simplified version that still exhibits the underlying cause (with --enable-assertions):

logic ac f : real, real -> real

function id_2() : real = 2.

axiom ax_1:
  f(f(id_2, 1.), 0.) <= 0.0

function f_2_1() : real = f(2., 1.)

axiom ax_2: f_2_1 <= 0.0

goal goal_1: false

It also fails with the default CDCL-Tableaux solver:

$ alt-ergo --enable-assertions --sat-solver CDCL c_262_0_ae_min.ae 
[Error]f((2),(1),(0)) <= 0 NOT normalized
       It is equal to f(f_2_1,(0))
Fatal error: exception File "src/lib/reasoners/intervalCalculus.ml", line 1327, characters 10-16: Assertion failed

The crux of the issue seems to be that after rewriting f(id_2, 1, 0) into f(2, 1, 0) we rewrite f(2, 1, 0) into f(f_2_1, 0) but we don't properly account for the transitive rewrite of f(id_2, 1, 0) into f(f_2_1, 0) in intervalCalculus (when adding -d cc we can see that we rewrite f(f_2, 1, 0) into f(f_2_1, 0) but we have the previous representative f(2, 1, 0) in the polynomial).

This looks to be related to the treatment of AC symbols — at least I didn't manage to reproduce the problem with a non-AC symbol —, even though I still do not understand exactly why. The only thing that comes to mind is that with an AC symbol, f(2, 1) is not a subterm of f(2, 1, 0) and hence does not get picked up somewhere in congruence closure. Some more investigation is needed but I'm done for today.

[bclement-ocp]

The only thing that comes to mind is that with an AC symbol, f(2, 1) is not a subterm of f(2, 1, 0) and hence does not get picked up somewhere in congruence closure.

I think I now understand the source of the issue, and that was not it.

Without AC symbols, the arithmetic engine (intervalCalculus) only ever sees aliens that are term representatives (in the sense of "the output of X.make for some term" — in other word, they have an entry in the repr table of the union-find), because no theories other than arithmetic performs simplifications on semantic values of type int or real.

This means that when the union-find updates the "touched" set during an union with a mapping r → nrr (where r is the term representative and nrr is the new normal form), we are always guaranteed that the old normal form rr (which is a term representative, and also in the equivalence class of r) will also get updated to the same new normal form: rr → nrr will be present in the "touched" set as well.

This is important, because the arithmetic engine only tracks bounds information for the normal forms — so it doesn't have any information on r, but it does have information on rr that can be used to compute information on nrr.

In the presence of AC symbols, we can end up with normal forms that are not term representatives (such as f(2, 1, 0) in the example above) — in which case the required entry rr → nrr will not be present in the "touched" set and invariants will be broken.

This can be verified by adding the lines

   predicate P(_ : real) = true
   axiom P_f_2_1_0 : P(f(f(2., 1.), 0.))

immediately after logic ac f : real, real -> real in the previous example makes the bug go away (because now we add f(2, 1, 0) to the union-find as a term representative)

Still need to figure out the right fix. Adding the entry rr → nrr in up_uf_rs seems to fix the bug, but I am not 100% sure it is the right fix — I don't understand this part of the code enough to know if it risks breaking other things or if it is conceptually the right place to fix things (I am trying to figure out what a fix on the intervalCalculus rather than the UF side of things would look like). Time to read up on AC(X) I guess.

At least I am fairly confident this is the root cause of the issue, and that it can only cause loss of precision (and crashes, as we have seen) — but probably not unsoundness.