conjure
conjure copied to clipboard
Published
20 hours ago •
conjure-cp
conjure-cp
new allDiff sequence refinement caused long running cyclic_graph test failure
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
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)])
What is this behaviour dependent on? I get the non allDiff version on my laptop.
