new allDiff sequence refinement caused long running cyclic_graph test failure

[fraser-dunlop]

Something is up with exhaustive.mildly_interesting.cyclic_graph. It is failing on azure linux and mac with a what looks like a machine variable numbering issue. It is a long running test which passes locally for me. I think it will time out on travis. Any ideas on the cause @ozgurakgun ?

2020-02-21T17:14:34.8554211Z     mildly_interesting.cyclic_graph:                                                                  FAIL
2020-02-21T17:14:34.8555023Z       Exception: files differ.
2020-02-21T17:14:34.8555280Z       1,3c1,3
2020-02-21T17:14:34.8555623Z       <     and([!(or([g_RelationAsSet_Explicit_1[q12] = g_RelationAsSet_Explicit_2[q14] /\
2020-02-21T17:14:34.8559407Z       <                g_RelationAsSet_Explicit_2[q12] = g_RelationAsSet_Explicit_1[q14]
2020-02-21T17:14:34.8560324Z       <                    | q12 : int(1..fin1)])
2020-02-21T17:14:34.8561721Z       ---
2020-02-21T17:14:34.8562389Z       >     and([!(or([g_RelationAsSet_Explicit_1[q11] = g_RelationAsSet_Explicit_2[q13] /\
2020-02-21T17:14:34.8562995Z       >                g_RelationAsSet_Explicit_2[q11] = g_RelationAsSet_Explicit_1[q13]
2020-02-21T17:14:34.8563518Z       >                    | q11 : int(1..fin1)])
2020-02-21T17:14:34.8563877Z       4,6c4,6
2020-02-21T17:14:34.8564517Z       <            or([or([g_RelationAsSet_Explicit_1[q8] = g_RelationAsSet_Explicit_2[q14] /\
2020-02-21T17:14:34.8565054Z       <                    g_RelationAsSet_Explicit_2[q8] = path_ExplicitBounded_Values[1]
2020-02-21T17:14:34.8565536Z       <                        | q8 : int(1..fin1)])
2020-02-21T17:14:34.8566094Z       ---
2020-02-21T17:14:34.8566543Z       >            or([or([g_RelationAsSet_Explicit_1[q7] = g_RelationAsSet_Explicit_2[q13] /\
2020-02-21T17:14:34.8567083Z       >                    g_RelationAsSet_Explicit_2[q7] = path_ExplicitBounded_Values[1]
2020-02-21T17:14:34.8567543Z       >                        | q7 : int(1..fin1)])
2020-02-21T17:14:34.8567890Z       7,9c7,9
2020-02-21T17:14:34.8568475Z       <                or([g_RelationAsSet_Explicit_1[q6] = path_ExplicitBounded_Values[path_ExplicitBounded_Length] /\
2020-02-21T17:14:34.8574461Z       <                    g_RelationAsSet_Explicit_2[q6] = g_RelationAsSet_Explicit_1[q14]
2020-02-21T17:14:34.8575035Z       <                        | q6 : int(1..fin1)])
2020-02-21T17:14:34.8575632Z       ---
2020-02-21T17:14:34.8579335Z       >                or([g_RelationAsSet_Explicit_1[q5] = path_ExplicitBounded_Values[path_ExplicitBounded_Length] /\
2020-02-21T17:14:34.8580176Z       >                    g_RelationAsSet_Explicit_2[q5] = g_RelationAsSet_Explicit_1[q13]
2020-02-21T17:14:34.8580885Z       >                        | q5 : int(1..fin1)])
2020-02-21T17:14:34.8581439Z       10,12c10,12
2020-02-21T17:14:34.8582004Z       <                and([and([or([g_RelationAsSet_Explicit_1[q10] = path_ExplicitBounded_Values[x] /\
2020-02-21T17:14:34.8583020Z       <                              g_RelationAsSet_Explicit_2[q10] = path_ExplicitBounded_Values[x + 1]
2020-02-21T17:14:34.8583567Z       <                                  | q10 : int(1..fin1)]),
2020-02-21T17:14:34.8584261Z       ---
2020-02-21T17:14:34.8584650Z       >                and([and([or([g_RelationAsSet_Explicit_1[q9] = path_ExplicitBounded_Values[x] /\
2020-02-21T17:14:34.8585400Z       >                              g_RelationAsSet_Explicit_2[q9] = path_ExplicitBounded_Values[x + 1]
2020-02-21T17:14:34.8585832Z       >                                  | q9 : int(1..fin1)]),
2020-02-21T17:14:34.8586137Z       13,16c13,15
2020-02-21T17:14:34.8586464Z       <                      and([path_ExplicitBounded_Values[q2] != path_ExplicitBounded_Values[q3]
2020-02-21T17:14:34.8587284Z       <                               | q2 : int(1..n - 2), q3 : int(1..n - 2), q2 < q3, q2 <= path_ExplicitBounded_Length,
2020-02-21T17:14:34.8587824Z       <                                 q3 <= path_ExplicitBounded_Length])]))
2020-02-21T17:14:34.8588179Z       <              | q14 : int(1..fin1)])
2020-02-21T17:14:34.8588583Z       ---
2020-02-21T17:14:34.8588885Z       >                      allDiff([path_ExplicitBounded_Values[q2]
2020-02-21T17:14:34.8589943Z       >                                   | q2 : int(1..n - 2), q2 <= path_ExplicitBounded_Length])]))
2020-02-21T17:14:34.8590407Z       >              | q13 : int(1..fin1)])
2020-02-21T17:14:34.8590669Z       
2020-02-21T17:14:34.8590879Z       CallStack (from HasCallStack):
2020-02-21T17:14:34.8591283Z         error, called at src/test/Conjure/ModelAllSolveAll.hs:501:14 in main:Conjure.ModelAllSolveAll
2020-02-21T17:14:34.8591796Z         assert, called at src/test/Conjure/ModelAllSolveAll.hs:384:21 in main:Conjure.ModelAllSolveAll

[fraser-dunlop]

Looks like the issue is actually that we are generating allDiff instead of an equivalent expected expression. That is pushing off the numbering and triggering the rest of the errors.

2020-02-21T17:14:34.8586137Z       13,16c13,15
2020-02-21T17:14:34.8586464Z       <                      and([path_ExplicitBounded_Values[q2] != path_ExplicitBounded_Values[q3]
2020-02-21T17:14:34.8587284Z       <                               | q2 : int(1..n - 2), q3 : int(1..n - 2), q2 < q3, q2 <= path_ExplicitBounded_Length,
2020-02-21T17:14:34.8587824Z       <                                 q3 <= path_ExplicitBounded_Length])]))
2020-02-21T17:14:34.8588179Z       <              | q14 : int(1..fin1)])
2020-02-21T17:14:34.8588583Z       ---
2020-02-21T17:14:34.8588885Z       >                      allDiff([path_ExplicitBounded_Values[q2]
2020-02-21T17:14:34.8589943Z       >                                   | q2 : int(1..n - 2), q2 <= path_ExplicitBounded_Length])]))
2020-02-21T17:14:34.8590407Z       >              | q13 : int(1..fin1)])

[fraser-dunlop]

What is this behaviour dependent on? I get the non allDiff version on my laptop.

[fraser-dunlop]

Suspect this commit a8d91d8

[fraser-dunlop]

Turns out this issue does occur locally for me. There is no magic...

[ozgurakgun]

is this resolved?