Numerical operation order causes problems
Issue #334
invalid
{ diag1(x,y) = x-(y+4). }
causes problems when { diag1(x,y) = (x-y)+4. diag2(x,y) = (x+y)-1. }
doesn't
Also, the resulting structure is not detected to be two-valued.
Comments (2)
-
reporter -
reporter - changed status to invalid
Please ignore the horrible arithmetics in this issue.
x-y+3 is not the same as x-(y+3)
- Log in to comment
Problems arise from faulty range generation.
Normal theory:
{ diag1(x,y) = x-y+3. }
{ diag2(x,y) = x+y-1. }
idpxsb_diag1(IDPXSB_x, IDPXSB_y, IDPXSB_var12) :- idpxsb_addr0x7fbad0150fb0(IDPXSB_x, IDPXSB_y, IDPXSB_var12), idpxsb_index(IDPXSB_x), idpxsb_index(IDPXSB_y), idpxsb_s15(IDPXSB_var12).
idpxsb_addr0x7fbad0150fb0(IDPXSB_x, IDPXSB_y, IDPXSB_var12) :- idpxsb_index(IDPXSB_x), idpxsb_index(IDPXSB_y), IDPXSB_var12 is IDPXSB_x-IDPXSB_y + 3.
idpxsb_s15(X) :- var(X), between(1,5,X).
idpxsb_s15(X) :- nonvar(X), X >= 1, X =< 5.
Changing diag1's definition to: { diag1(x,y) = x-(y+3). } leads to generation of the following rules and ranges:
idpxsb_diag1(IDPXSB_x, IDPXSB_y, IDPXSB_var12) :- idpxsb_addr0x7fab101518a0(IDPXSB_x, IDPXSB_y, IDPXSB_var12), idpxsb_index(IDPXSB_x), idpxsb_index(IDPXSB_y), idpxsb_s51(IDPXSB_var12).
idpxsb_addr0x7fab101518a0(IDPXSB_x, IDPXSB_y, IDPXSB_var12) :- idpxsb_index(IDPXSB_x), idpxsb_index(IDPXSB_y), IDPXSB_var12 is IDPXSB_x - IDPXSB_y+3.
idpxsb_s51(X) :- var(X), between(-5,-1,X).
idpxsb_s51(X) :- nonvar(X), X >= -5, X =< -1.
Manipulating diag2's definition in a similar fashing doesn't impact correctness.