Cannot index an empty matrix

[SaadAttieh]

letting s be []
find a : int(1..5)
such that
a = s[1]

Conjure output:

Generating models for test.essence
Generated models: model000001.eprime
Saved under: conjure-output
Savile Row: model000001.eprime
Error:
    Savile Row stdout: 
    Savile Row stderr: such that a = ([] : `matrix indexed by [?] of ?`)[1]

---------------------------------------^
ERROR: Successfully parsed 'matrix indexed by'.
ERROR: Failed when parsing rest of structure following line:5 column:39

    Savile Row exit-code: 1

[pwn1]

Savile Row can't parse those question marks.

[SaadAttieh]

Yeah, I did think that wasn't eprime syntax. :P On 22 Jul 2019, at 1:42 pm, Peter Nightingale [email protected] wrote:

Savile Row can't parse those question marks.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[ozgurakgun]

@pwn1 - SR seems to assume that [] is the same as ([] : matrix indexed by [int()] of int)

So this is UNSAT (with or without the type annotation)

letting s be ([] : `matrix indexed by [int()] of int`)
find a : int(1..5)
such that a = s[1]

And this has 1 solution with the type annotation, and it is UNSAT without

letting s be ([] : `matrix indexed by [int()] of bool`)
find a : bool
such that
a = s[1]

[pwn1]

OK, that should be documented I suppose.