Variable mismatch / ignored

[aubertc]

The following program:

int main(){
    x2 = x3 + x1;
    x4 = x2;
}

gives

--- Affiche <relation_list.RelationList object at 0x7f54084e7ef0> ---
1:
x2    |     +o  +o  +o
x3    |     +o+w.delta(0,0)+m.delta(1,0)+p.delta(2,0)  +m  +o
x1    |     +o+w.delta(0,0)+p.delta(1,0)+m.delta(2,0)  +o  +m
--- FIN ---
[[0], [1], [2]]

As we can see, x4 is simply not accounted for.

[ThomasRuby]

I've changed the assertions of test_analyze_if_with|out_braces since y = x3 generates [ o, o | m, m] now. Can someone check that it's normal that we have now combinations ? It didn't chock me since we have if statement them sum of Polynomials…

[nkrusch]

The analysis now gives this output. We will need to check if this is the correct matrix:

x2    |     +o  +o  +o  +o
x3    |     +o+w.delta(0,0)+m.delta(1,0)+p.delta(2,0)  +m  +o  +o+w.delta(0,0)+m.delta(1,0)+p.delta(2,0)
x1    |     +o+w.delta(0,0)+p.delta(1,0)+m.delta(2,0)  +o  +m  +o+w.delta(0,0)+p.delta(1,0)+m.delta(2,0)
x4    |     +o  +o  +o  +o

I computed it by hand (there is a choice E3/E4 for X3+X1):

(C rule) after multiplying the two matrices I get:

Choosing E4 earlier in X3+X1, I get result

1. Can you check what I wrote above? If I made some mistake I'd like to know how to do it correctly.
2. Does it match the implementation output? Apart from X2,X4 I'm not sure how to read the deltas.

Other comments:

• The X4 variable is being picked up now which is good.
• The two separate unit tests for if with braces vs. without braces is to check we get the same answer in both cases (#7).
• I'm an idiot because I worked out this example and I now realize that the test is for different input... let me analyze that also (please check what I wrote earlier regardless!)
• We should use branches for all code changes. I am moving these changes to own branch called issue-11.

EDIT: These changes are in a branch now, Thomas, run git checkout issue-11 to switch to it.

[nkrusch]

The input is

int main() {
     int x;
     int y;
     x = 1;
     int x1;
     int x2;
     int x3;
     x1 = 1;
     x2 = 2;
     if (x > 0) x3 = 1;
     else x3 = x2;
     y = x3;
}

before this change, we get

x   |     +o  +o  +o  +o
x1  |     +o  +o  +o  +o
x2  |     +o  +o  +o  +o
x3  |     +o  +o  +o  +m

after this change, we get

x  |     +o  +o  +o  +o  +o
x1 |     +o  +o  +o  +o  +o
x2 |     +o  +o  +o  +o  +o
x3 |     +o  +o  +o  +o  +o
y  |     +o  +o  +o  +o  +o

so the question is what is the correct scalar for X3?

(Side note, we could rewrite this test to use a different input, because the goal here is to check that presence/absence of braces around the if body does not change analysis result. This input was based on #7 but it is not a very interesting input, because it gives 0 matrix. Some small 2x2 example with different scalars would seem like a more useful test case.)

[seiller]

I believe both outputs are incorrect. I think we should have 0s everywhere except for an m showing a dependency of x3 w.r.t. x2, and an m showing a dependency of y w.r.t. x3.

[ThomasRuby]

I believe both outputs are incorrect. I think we should have 0s everywhere except for an m showing a dependency of x3 w.r.t. x2, and an m showing a dependency of y w.r.t. x3.

I'm not sure of that since we have x2 = 2 and y = x3 = ((x2 = 2) | 1) constant (then 0s) should be propagated, isn't it ?

[ThomasRuby]

EDIT: These changes are in a branch now, Thomas, run git checkout issue-11 to switch to it.

I thought it would be a minor change… you're right I should have created a branch for this issue ^^'

[ThomasRuby]

I computed it by hand (there is a choice E3/E4 for X3+X1):

(C rule) after multiplying the two matrices I get:

Choosing E4 earlier in X3+X1, I get result

1. Can you check what I wrote above? If I made some mistake I'd like to know how to do it correctly.

2. Does it match the implementation output? Apart from X2,X4 I'm not sure how to read the deltas.

Thank you for doing it by hand ! To me it seems to be ok (this is why I didn't mention it in the commit) but you're right it's good to have another test checked by hand to put in our UT. If we swap column/row we get :

x1    |     +m  +o+w.delta(0,0)+p.delta(1,0)+m.delta(2,0)  +o  +o+w.delta(0,0)+p.delta(1,0)+m.delta(2,0)
x2    |     +o  +o  +o  +o
x3    |     +o  +o+w.delta(0,0)+m.delta(1,0)+p.delta(2,0)  +m  +o+w.delta(0,0)+m.delta(1,0)+p.delta(2,0)
x4    |     +o  +o  +o  +o

@seiller can you confirm that ? I'm also never sure about deltas index order ^^'

[aubertc]

A couple of comments:

• My example was not the best, it is uselessly complicated, we could have picked a simpler one. But ok.

• Can you check what I wrote above? If I made some mistake I'd like to know how to do it correctly.

I believe it is correct, but using E2 we can also get X3 + X1 being (w / o / w / o), since this rule simply says "put w on every variable occurring in that expression".

With that respect, I believe @ThomasRuby 's output in the post above is correct.

• For the

   if (x > 0) x3 = 1;
   else x3 = x2;
   y = x3;

  program, I'm blanking on how "x3 = 1" should be interpreted: As "put the vector for 0 (which is just 0s) at x3", so as

x1    |     m +o +o +o 
x2    |     +o  m  +o +o 
x3    |     +o +o +o +o 
x4    |      +o +o +o m 

?

[aubertc]

So, the second example is weirdly written (not all the assignment at the same place, i.e., they are mixed with declaration), which makes it hard to parse by hand, and it's not too interesting either because everything gets cancelled in the end, I believe.

In any case, the second example should be all 0's, indeed.

You can use the following python helper to check some calculation:

from pymwp import Polynomial, Monomial
from pymwp.matrix import identity_matrix, matrix_prod, matrix_sum, show
from typing import Any, Optional, List
from functools import reduce

# First example of https://github.com/seiller/pymwp/issues/11
#     x2 = x3 + x1;
l1=identity_matrix(4)
l1[0][1] = Polynomial([Monomial('m')])
l1[1][1] = Polynomial([Monomial('o')])
l1[2][1] = Polynomial([Monomial('p')])
show(l1, prefix="[   x1 ,    x2   , x3   ,     x4 ]")

#     x4 = x2;
l2=identity_matrix(4)
l2[1][3] = Polynomial([Monomial('m')])
l2[3][3] = Polynomial([Monomial('o')])
show(l2, prefix="[   x1 ,    x2   , x3   ,     x4 ]")

# Result:
show(matrix_prod(l1, l2))

print("Second example\n")

# Second example of https://github.com/seiller/pymwp/issues/11
#      x = 1;
l1=identity_matrix(5)
l1[0][0] = Polynomial([Monomial('o')])
show(l1, prefix="[   x  ,    x1   ,   x2  ,   x3  ,   y ]")

#      x1 = 1;
l2=identity_matrix(5)
l2[1][1] = Polynomial([Monomial('o')])
show(l2, prefix="[   x  ,    x1   ,   x2  ,   x3  ,   y ]")

#      x2 = 2;
l3=identity_matrix(5)
l3[2][2] = Polynomial([Monomial('o')])
show(l3, prefix="[   x  ,    x1   ,   x2  ,   x3  ,   y ]")

#      if (x > 0) x3 = 1;
#      else x3 = x2;
l4=identity_matrix(5)
l4[3][3] = Polynomial([Monomial('o')])
l4[2][3] = Polynomial([Monomial('m')])
show(l4, prefix="[   x  ,    x1   ,   x2  ,   x3  ,   y ]")

#      y = x3;
l5=identity_matrix(5)
l5[4][4] = Polynomial([Monomial('o')])
l5[3][4] = Polynomial([Monomial('m')])
show(l5, prefix="[   x  ,    x1   ,   x2  ,   x3  ,   y ]")

# Putting it all together:

show(matrix_prod(matrix_prod(matrix_prod(matrix_prod(l1, l2), l3), l4), l5), prefix="[   x  ,    x1   ,   x2  ,   x3  ,   y ]")

[aubertc]

I believe both outputs are incorrect. I think we should have 0s everywhere except for an m showing a dependency of x3 w.r.t. x2, and an m showing a dependency of y w.r.t. x3.

I think that all of that get canceled because

• x2 = 2; makes that x2's dependency w.r.t. itself is now 0,
• x3 = 1; + x3 = x2; makes that in one case, x3 is dependend on x2 (which has no dependencies, since x2 = 2;), and on the other it's just 0.

So I believe everything gets canceled in the end, when all of that get multiplied.

[seiller]

The conditional is computed as the max (the sum) of the two branches, so it should not be 0s everywhere.

[aubertc]

Yes, but it's not just an if: the

 x = 1;
…
 x1 = 1;
 x2 = 2;
…
 y = x3;

nullify most of the values, and then the product does the rest…

[seiller]

Right, the constant value of x_2 is propagated to x_3. Sorry for overlooking that.

[aubertc]

It's easy to overlook it with this weird statement order (declaration / assignment / declaration).

[ThomasRuby]

I believe both outputs are incorrect. I think we should have 0s everywhere except for an m showing a dependency of x3 w.r.t. x2, and an m showing a dependency of y w.r.t. x3.

I'm not sure of that since we have x2 = 2 and y = x3 = ((x2 = 2) | 1) constant (then 0s) should be propagated, isn't it ?

↑ I thought we agreed 2 days ago ^^' ↑

Well I think it would be good to put their results (of the two examples we agreed to be good) into a unit test. Then I will close the issue.