regression: <=lex no longer can compare matrix and list

[ott2]

As of late 2018, conjure supported specs of the form:

given n : int(1..)
letting ind be domain int(1..n)
find P : matrix indexed by [ind] of bool
such that P <=lex [ P[n+1-i] | i : ind ]

(this finds bit strings representing numbers that can't be increased by considering their bits in reverse order). This worked fine in 112ccfc (2018-07-30), and was accepted by 4ff0e49 (2017-10-23) but gave the wrong results. However, now 0f68543 (2019-10-07) gives a "should never happen"

rule_FlattenLex: flatten isn't defined for this reference fellow...

If this is as intended, some advice about how to do this would be appreciated.

[ozgurakgun]

Thanks @ott2 - I think this is because it's a boolean list. A recent commit seems to have broken it. Definitely a regression, will look at fixing it.

[ott2]

A similar but possibly unrelated error occurs for integer lists (I'm trying to generate latin squares); the above is meant as a small yet still interesting example.

flattener:  TypeMatrix (TypeInt TagInt) (TypeInt TagInt)
            TypeList (TypeInt TagInt)

This used to work in late 2018.

[ott2]

A somewhat related issue is that equality cannot be taken between a matrix and a list:

given n : int(1..) $ length
letting ind be domain int(1..n)
find P : matrix indexed by [ind] of bool
such that P = [ P[n+1-i] | i : ind ]

(this is meant to find Boolean palindromes) yields:

Savile Row stdout: ERROR: Unexpected matrix in binary numerical/logical operator: (P=[P[((3 + 1) - i)]|i : int(1..3), () ;int(1..)])

Savile Row stderr: ERROR: Failed type checking after substituting in lettings.

However, unlike the case with <=lex I don't have any evidence that this ever worked, so this isn't obviously a regression.

[fraser-dunlop]

@ott2 Going back to your first example.

given n : int(1..)
letting ind be domain int(1..n)
find P : matrix indexed by [ind] of bool
such that P .<= [ P[n+1-i] | i : ind ]

This works for me.

@ozgurakgun I think the problem here is less of a regression and more of an undocumented change in semantics (my bad - this should be documented somewhere).

The failing rule here is a partial function that assumes that we have arrived at a <=lex via reduction from .<= operator.

To resolve this we need to deprecate something. As far as I am aware ~< and ~<= have been canned. I suggest we do the same for <lex and <=lex in the input language (keep them internally as they are refined to from .< and .<=). Does this sound reasonable?

[fraser-dunlop]

Re: deprecating <lex and <=lex. I suggest we remove them from the input language and output a helpful error message that tells the user to use .< or .<=. Either that or rewrite from <lex to .< as a preprocessing step.

[ozgurakgun]

Let's talk about this. I am not confident in making .< surface language. I think eventually we want < to work for everything and then we can deprecate <lex. .< and ~< were never intended to be user-facing.

We should make sure <lex still works though, since otherwise old models will break unnecessarily.

[SaadAttieh]

Side point, not sure if I should make it a separate issue. But I proposed a refinement for equality between list comprehension with conditions and a variable sized sequence. It wasn’t simple though. What are your thoughts?

…

On 28 Oct 2019, at 11:09, Özgür Akgün ***@***.***> wrote: Let's talk about this. I am not confident in making .< surface language. I think eventually we want < to work for everything and then we can deprecate <lex. .< and ~< were never intended to be user-facing. We should make sure <lex still works though, since otherwise old models will break unnecessarily. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#456?email_source=notifications&email_token=ABNOACUY4OCCMX27QK62EKTQQ3B7LA5CNFSM4JED33RKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOECMQGVI#issuecomment-546898773>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABNOACVBHSKJZ2UH4RLI2GLQQ3B7LANCNFSM4JED33RA>.

[SaadAttieh]

I’ll paste it here, as it might be lost on slack. So we currently don't have equality between sequences and list comprehensions in Essence. I would like to propose a refinement: So we start with the expression to refine: ``` find s : sequence ... such that s = [constraint(v) | v <- generator, condition(v)] ``` I would do this in two steps. First I would add something like an enumerate function in Essence as I think it might generally be useful. so ``` enumerate([constraint(v) | v <- generator, condition(v)]) ``` should return a list of tuples, ``(index,constraint(v))``. Obviously, assuming we have this function we can then just write: ``` forAll (index,value) in enumerate([constraint(v) | v <- generator, condition(v)]) . s(index) = value, |s| = |[constraint(v) | v <- generator, condition(v)]| ``` So then the harder part, how to do enumerate. I would suggest something like this: First create and define aux vars ``` find indices : matrix indexed by [int(1..n)] of int(0..n) $where n is the maximum length of the list comprehension such that forAll i : int(2..n), i <= |listComp| . $letting v be the i'th element produced by the generator indices[i] = [indices[i-1],indices[i-1]+1; int(0..1)][toInt(condition(v))], indices[1] = toInt(condition(v1)) $v1 is first value produced by generator ``` Do the rewrite: ``` enumerate([constraint(v) | v <- generator, condition(v)]) ``` becomes ``` [(indices[i], constraint(v)) | v <- generator, condition(v), letting i be original index of v as produced by generator] ```

[ozgurakgun]

@ott2 #466 should fix this, can you test once it is merged, please. I'll let you know when it is merged as well.

[ott2]

Marking up Saad's email response above:

So we currently don't have equality between sequences and list comprehensions in Essence. I would like to propose a refinement:
So we start with the expression to refine:

find s : sequence ...
such that s = [constraint(v) | v <- generator, condition(v)]

I would do this in two steps. First I would add something like an enumerate function in Essence as I think it might generally be useful.
so

enumerate([constraint(v) | v <- generator, condition(v)])

should return a list of tuples, (index,constraint(v)).
Obviously, assuming we have this function we can then just write:

forAll (index,value) in enumerate([constraint(v) | v <- generator, condition(v)]) . s(index) = value,
|s| = |[constraint(v) | v <- generator, condition(v)]|

So then the harder part, how to do enumerate. I would suggest something like this:
First create and define aux vars

find indices : matrix indexed by [int(1..n)] of int(0..n)
$where n is the maximum length of the list comprehension
such that
forAll i : int(2..n), i <= |listComp| .
    $letting v be the i'th element produced by the generator
    indices[i] = [indices[i-1],indices[i-1]+1; int(0..1)][toInt(condition(v))],
indices[1] = toInt(condition(v1)) $v1 is first value produced by generator

Do the rewrite:

enumerate([constraint(v) | v <- generator, condition(v)])

becomes

[(indices[i], constraint(v)) | v <- generator, condition(v), letting i be original index of v as produced by generator]

[ott2]

It seems #466 is still not merged. Unfortunately this means symmetry breaking in several old models no longer works, and a new model I've been developing for latin squares also does not work. I can't make any progress on this style of modelling at all because of this, and this is blocking multiple things I'm trying to work on.

Can I ask for either <lex to be fixed again by reverting whatever broke it, or that we merge what needs to be merged so that <lex starts working with the new approach (when I would rather use < more generically)?

[ozgurakgun]

I will look into fixing this later today. Can you (could be in a private email) send me pointers to any old models that are broken by this? I can use them as test cases.

…

On Wed, 27 Nov 2019 at 10:46, András Salamon ***@***.***> wrote: It seems #466 <#466> is still not merged. Unfortunately this means symmetry breaking in several old models no longer works, and a new model I've been developing for latin squares also does not work. I can't make any progress on this style of modelling at all because of this, and this is blocking multiple things I'm trying to work on. Can I ask for either <lex to be fixed again by reverting whatever broke it, or that we merge what needs to be merged so that <lex starts working with the new approach (when I would rather use < more generically)? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#456?email_source=notifications&email_token=AABNEUR4CH2LKSLJOTSPRPLQVZFZHA5CNFSM4JED33RKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEFJDBMI#issuecomment-559034545>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABNEUQ6ZACPTT5G2GXAECLQVZFZHANCNFSM4JED33RA> .

-- Özgür Akgün

[ott2]

Here was an Essence spec for enumerating non-isomorphic Hamiltonian cycles in a grid (I think this was the basis for a nugget), with letting n be 2 being the single entry in the associated parameter file. This used to work last year and took 6s per solution for letting n be 8.

$ counting Hamiltonian cycles in an n by n grid
$ bijective path, induced bit pattern of inside/outside blocks for symmetry
$ about 6s per solution for 8x8

given n : int(1..)
letting U be n-1
letting W be n-2
letting N be n*n
letting M be U*U
letting V be M-1
letting vertices be domain int(0..N-1) $ i,j -> i*n+j 0,0 .. U,U
letting index be domain int(1..N)
letting blocks be domain int(0..V) $ i,j -> i*U+j 0,0 .. 0,U-1 1,0 .. U-1,U-1

find p : sequence (size N,bijective) of vertices
such that $ p represents a cycle
and([ |p(k)/n - p((k%N)+1)/n| + |p(k)%n - p((k%N)+1)%n| = 1 | k : index ])

$ break symmetries introduced by using p
such that p(1) = 0, p(2) = 1, p(N) = n,

$ determine 0-1 pattern of blocks outside-inside curve
$ denote block by top left corner
find P : matrix indexed by [blocks] of bool

$ use the path, right hand side is inside, LHS is outside
such that
P[0],

and([ (((u1=v1  ) /\ (u2=v2-1) /\ (u1 < W)) ->  P[ u1   *U+u2  ]) $ E
   /\ (((u1=v1-1) /\ (u2=v2  ) /\ (u2 > 0)) ->  P[ u1   *U+u2-1]) $ S
   /\ (((u1=v1  ) /\ (u2=v2+1) /\ (u1 > 0)) ->  P[(u1-1)*U+u2-1]) $ W
   /\ (((u1=v1+1) /\ (u2=v2  ) /\ (u2 < W)) ->  P[(u1-1)*U+u2  ]) $ N
   | k : index, letting u1 be p(k)/n, letting u2 be p(k)%n,
   letting v1 be p((k%N)+1)/n, letting v2 be p((k%N)+1)%n ]),

$ the rest must all be 0 (or sum of true values is 17/18 for 8x8?)
$ without this, the solution might not be canonical
and([ (((u1=v1  ) /\ (u2=v2-1) /\ (u1 > 0)) -> !P[(u1-1)*U+u2  ]) $ E
   /\ (((u1=v1-1) /\ (u2=v2  ) /\ (u2 < W)) -> !P[ u1   *U+u2  ]) $ S
   /\ (((u1=v1  ) /\ (u2=v2+1) /\ (u1 < W)) -> !P[ u1   *U+u2-1]) $ W
   /\ (((u1=v1+1) /\ (u2=v2  ) /\ (u2 > 0)) -> !P[(u1-1)*U+u2-1]) $ N
   | k : index, letting u1 be p(k)/n, letting u2 be p(k)%n,
   letting v1 be p((k%N)+1)/n, letting v2 be p((k%N)+1)%n ]),

$ ensure holes are assigned also
and([ ((k >= U) /\ (k < W*U) /\ (k%U > 0) /\ (k%U < W))
   -> (
   (( P[k-U]/\ P[k+U]/\ P[k-1]/\ P[k+1]) ->  P[k]) /\
   ((!P[k-U]/\!P[k+U]/\!P[k-1]/\!P[k+1]) -> !P[k]))
   | k : blocks ]),

$ check that a cycle is lex-first
such that $ k=   (k/U)*U + k%U
   P <=lex [ P[(W-(k/U))*U + k%U]     | k : blocks ],
   P <=lex [ P[(W-(k%U))*U + k/U]     | k : blocks ],
   P <=lex [ P[   (k%U) *U + k/U]     | k : blocks ],
   P <=lex [ P[(W-(k/U))*U + W-(k%U)] | k : blocks ],
   P <=lex [ P[   (k/U) *U + W-(k%U)] | k : blocks ],
   P <=lex [ P[   (k%U) *U + W-k/U]   | k : blocks ],
   P <=lex [ P[(W-(k%U))*U + W-k/U]   | k : blocks ],