more subsequence glitches

[ott2]

(Recording this from email.)

The following fails:

given m : int(1..)
find Cs : sequence (size m) of int(0..m)
such that
    exists Cz : sequence (size m) of int(0..m) .
        Cz subsequence Cs

as does this:

given m : int(1..)
find Cz : sequence (size m) of int(0..m)
such that
    exists Cs : sequence (size m) of int(0..m) .
        Cz subsequence Cs

but this one is fine:

given m : int(1..)
find Cs : sequence (size m) of int(0..m)
find Cz : sequence (size m) of int(0..m)
such that
    Cz subsequence Cs

I would expect the semantics of all three to be roughly equivalent.

[ott2]

This is blocking several different attempts to write an improved nonogram spec, using collections of sequences and the subsequence constraint. :-(

Concretely, I have a matrix of sequence as input, and I want to create a new matrix of sequences that is computed from the input matrix by some simple manipulation. I can do this trivially by means of a preprocessing script that interpolates zero entries between the existing entries for the use case I have, and writing the output as a new parameter file. IIRC, procedural preprocessing of this kind is what the MiniZinc models of Nonogram use. However, in the spirit of Essence, I'm trying to keep things purely declarative...

One option would be if the exists form for sequences (the first spec of the three in the original comment) worked correctly with subsequence, avoiding the issue that matrix types are atomic. Atomic matrix types make it impossible to define another matrix with a slightly different type for each entry, based on an existing matrix. With matrix indexed by [I] of D when D is a sequence type, then the type should really be a list of types, and ideally there should be a way to retrieve those types for each index and do something with them. Sequences can have different lengths and one may need to use this when defining a new matrix of sequences.

In the exists form of the spec, I'm avoiding having to dig inside the types of each entry in the input matrix of sequences to retrieve their attributes, by creating the sequence of interest on the fly for each entry. It seems plausible that this could be done reasonably easily, as each instance of the sequence should be rewritten at some stage of translation to depend on the quantified variable, thus creating what is in effect an internal matrix of sequences, with possibly different lengths for each.

Another option would be if Conjure/SR supported syntax along the following lines:

given X : matrix indexed by [I] of sequence of D
find Y : matrix [sequence (size |X[i]|) of D | i : I]

or even just

given X : matrix indexed by [I] of sequence of D
find Y : typeOf(X)

Right now there seems to be no way to transform a given matrix of sequences in any nontrivial way, because we have no syntax to define a matrix of sequences with lengths that depend on some input, not even if the new matrix of sequences are all the same length as the old one. Further, trying to use the attributes of a matrix of sequences in specifying the type of a new variable results in errors.

It would even be useful if we had a way of saying "copy the type of this variable to this other variable", such as a typeOf() function. The type of a matrix of sequences is then a matrix of sequences with possibly different attributes for each entry. Reusing the type of a complex object for another complex object would also allow terser specs in some cases.

Summary:

1. exists sequence should work with subsequence.
2. If not, then declaring a new matrix of sequences depending on a given matrix of sequences should be possible.
3. If not, then a mechanism like typeOf() to duplicate the complex type of a given variable should be possible.

(Pretty please?)

[ozgurakgun]

Hi @ott2 -

It's been a while a realise. I am trying to reproduce this but it seems with current Conjure the first two models work.

For reference, the following is the E' I get for the first one.

language ESSENCE' 1.0

given m: int(1..)
find Cs_ExplicitBounded_Length: int(m)
find Cs_ExplicitBounded_Values: matrix indexed by [int(1..m)] of int(0..m)
find conjure_aux1_ExplicitBounded_Length:
        matrix indexed by [int(m), matrix indexed by [int(1..m)] of int(0..m)] of int(m)
find conjure_aux1_ExplicitBounded_Values:
        matrix indexed by [int(m), matrix indexed by [int(1..m)] of int(0..m), int(1..m)] of int(1..m)
branching on [Cs_ExplicitBounded_Length, Cs_ExplicitBounded_Values]
such that
    and([and([conjure_aux1_ExplicitBounded_Values[q3 - 1] < conjure_aux1_ExplicitBounded_Values[q3] /\ q3 <= m /\
              q3 - 1 <= m
                  | q3 : int(2..m), q3 <= m])
             | Cz_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)]),
    and([true | Cz_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)]),
    or([and([Cz_ExplicitBounded_Values[q5] = Cs_ExplicitBounded_Values[conjure_aux1_ExplicitBounded_Values[q5]] /\
             q5 <= m
             /\ (conjure_aux1_ExplicitBounded_Values[q5] <= m /\ q5 <= m)
                 | q5 : int(1..m), q5 <= m])
            | Cz_ExplicitBounded_Values : matrix indexed by [int(1..m)] of int(0..m)])

[ott2]

I'm seeing SR dimension mismatch errors for the first two. This is with SR bundled with Conjure, as of a few days ago: 3d21a107b (2019-06-19 11:31:05 +0100)

[ozgurakgun]

I edited the test case to run each example (with m=3). For me 1 and 3 runs without any problems, but 2 hits the SR bug* you see.

It would be good if you can report please, yes. We should remember to edit this test case to run conjure solve on example 1 as well, once the bug* is fixed.

[*] Unless I am missing something...

[ott2]

Still seeing the same errors with the first two.

conjure solve -ac issue-conjure-395a.essence issue-conjure-395.param
Generating models for issue-conjure-395a.essence
Generated models: model000001.eprime
Saved under: conjure-output
Savile Row: model000001.eprime issue-conjure-395.param
Error:
    Savile Row stdout: ERROR: Dimension mismatch in matrix deref: conjure_aux1_ExplicitBounded_Values[(q3 - 1)]

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

    Savile Row exit-code: 1

and

Generating models for issue-conjure-395b.essence
Generated models: model000001.eprime
Saved under: conjure-output
Savile Row: model000001.eprime issue-conjure-395.param
Error:
    Savile Row stdout: ERROR: Dimension mismatch in matrix deref: conjure_aux1_ExplicitBounded_Values[q5]

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

    Savile Row exit-code: 1

issue-conjure-395.param:

letting m be 3

issue-conjure-395a.essence:

given m : int(1..)
find Cs : sequence (size m) of int(0..m)
such that
    exists Cz : sequence (size m) of int(0..m) .
        Cz subsequence Cs

issue-conjure-395b.essence:

given m : int(1..)
find Cz : sequence (size m) of int(0..m)
such that
    exists Cs : sequence (size m) of int(0..m) .
        Cz subsequence Cs

The third spec yields the solution (as expected):

language Essence 1.3

letting Cs be sequence(0, 0, 0)
letting Cz be sequence(0, 0, 0)

versions: Savile Row 1.7.0 (Repository Version: 13406b8e8 (2019-06-17 22:16:49 +0100)) as bundled with current conjure: Repository version 16c3e4ba9 (2019-06-28 11:36:06 +0100)

For reference, here are the eprime files also:

issue-conjure-395a-eprime.txt
issue-conjure-395b-eprime.txt

[ozgurakgun]

Oh I see now. I must have made a mistake when I copied the files over. You'll see if you look at the files in the test directory.

I'll fix the test cases. This should be raised with SR regardless.

[ozgurakgun]

Fixed now, we are in the same place. The commit above (d8d81ee) fixes the copy/paste error.

[ott2]

See https://github.com/savilerow/savilerow-main/issues/217

[pwn1]

Which SR files should I be using? I need a param file to go with 395a and 395b above.

[ott2]

The param file above is fine (issue-conjure-395.param), it just contains letting m be 3. The eprime-param file is just:

language ESSENCE' 1.0

letting m be 3

[pwn1]

Well that was easy to diagnose. Indexing a matrix with a matrix is only (currently) implemented when the inner matrix is the only index. I'll see what I can do.

[pwn1]

Are the two eprime files attached here out of date?
I have done some work on matrices-indexed-by-matrices to implement this case, but actually it seems the error is in the eprime file -- it is indexing a matrix with one integer when the matrix has several dimensions.

[ott2]

Pete, the versions were as above in the comment; SR was the one that Oz shipped and quite recent at the time. I don't have access right now to a newer environment to test. @ozgurakgun can you perhaps reproduce -- might be more a Conjure glitch than an SR one?

[ott2]

@ozgurakgun @pwn1 while I recompile my toolchain using a recent clang (this will take some days) so that I can natively compile conjure again, could either of you quickly check whether the latest conjure/SR combo now deals with these cases correctly?