[cutsolver] failing tests

[ranjitjhala]

@bmcfluff I have tweaked the make test so that all the .fq tests are run with -e (and also the ones particular to --eliminate). There are a couple of tests that fail with --eliminate, namely:

• tests/pos/test3.fq
• tests/elim/test2.fq

Can you take a look?

[BenjaminCosman]

For the first of these at least, the problem is that renameAll performs the following transformation:

bind 0 x ... $k0[x := e]

to

bind 0 lq_rnm_x ... $k0[x := e][x := lq_rnm_x]

when in fact we need either

bind 0 lq_rnm_x ... $k0[lq_rnm_x := x][x := e][x := lq_rnm_x]

or

bind 0 lq_rnm_x ... $k0[lq_rnm_x := e]

On Sun, 7 Jun 2015 at 11:43 Ranjit Jhala notifications@github.com wrote:

@bmcfluff https://github.com/bmcfluff I have tweaked the make test so that all the .fq tests are run with -e (and also the ones particular to --eliminate). There are a couple of tests that fail with --eliminate, namely:

• tests/pos/test3.fq
• tests/elim/test2.fq

Can you take a look?

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/76.

[BenjaminCosman]

tests/pos/test3.fq: addressed by ad590659505cb4c1a4a21b7875ae98cc9237d344

tests/elim/test2.fq: I think the circular dependencies in this test may make it unsolvable by the eliminate algorithm alone?

[ranjitjhala]

​the 'tests/elim' are just those fq files that are to be run with -e​ (in short, its ok if it cannot be solved be elim alone but requires qualifiers after the eliminate phase.)

does that make sense? (or were you worried about something else?)

On Wed, Jun 10, 2015 at 11:18 AM, bmcfluff notifications@github.com wrote:

tests/pos/test3.fq: addressed by ad59065 https://github.com/ucsd-progsys/liquid-fixpoint/commit/ad590659505cb4c1a4a21b7875ae98cc9237d344

tests/elim/test2.fq: I think the circular dependencies in this test may make it unsolvable by the eliminate algorithm alone?

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/76#issuecomment-110862225 .

Ranjit.

[BenjaminCosman]

In that case, should this issue be closed? The first test passed and the second isn't expected to pass in its current state (i.e. without qualifiers).

On Wed, 10 Jun 2015 at 11:37 Ranjit Jhala notifications@github.com wrote:

​the 'tests/elim' are just those fq files that are to be run with -e​ (in short, its ok if it cannot be solved be elim alone but requires qualifiers after the eliminate phase.)

does that make sense? (or were you worried about something else?)

On Wed, Jun 10, 2015 at 11:18 AM, bmcfluff notifications@github.com wrote:

tests/pos/test3.fq: addressed by ad59065 < https://github.com/ucsd-progsys/liquid-fixpoint/commit/ad590659505cb4c1a4a21b7875ae98cc9237d344

tests/elim/test2.fq: I think the circular dependencies in this test may make it unsolvable by the eliminate algorithm alone?

— Reply to this email directly or view it on GitHub < https://github.com/ucsd-progsys/liquid-fixpoint/issues/76#issuecomment-110862225

.

Ranjit.

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/76#issuecomment-110870149 .

[ranjitjhala]

Hang on, I believe the test is there because it passes with -n but fails with -n -e which should never happen.

On Jun 10, 2015, at 2:39 PM, bmcfluff notifications@github.com wrote:

In that case, should this issue be closed? The first test passed and the second isn't expected to pass in its current state (i.e. without qualifiers).

On Wed, 10 Jun 2015 at 11:37 Ranjit Jhala notifications@github.com wrote:

​the 'tests/elim' are just those fq files that are to be run with -e​ (in short, its ok if it cannot be solved be elim alone but requires qualifiers after the eliminate phase.)

does that make sense? (or were you worried about something else?)

On Wed, Jun 10, 2015 at 11:18 AM, bmcfluff notifications@github.com wrote:

tests/pos/test3.fq: addressed by ad59065 < https://github.com/ucsd-progsys/liquid-fixpoint/commit/ad590659505cb4c1a4a21b7875ae98cc9237d344

tests/elim/test2.fq: I think the circular dependencies in this test may make it unsolvable by the eliminate algorithm alone?

— Reply to this email directly or view it on GitHub < https://github.com/ucsd-progsys/liquid-fixpoint/issues/76#issuecomment-110862225

.

Ranjit.

— Reply to this email directly or view it on GitHub https://github.com/ucsd-progsys/liquid-fixpoint/issues/76#issuecomment-110870149 .

— Reply to this email directly or view it on GitHub.

[BenjaminCosman]

At present it fails with both -n and -ne

[ranjitjhala]

ok, interesting because i "wanted" k0 to be eliminated and not k1. I modified the test to add a

cut $k1

and now it works with -n -e (but not -n).