tests/for_while_unsigned.scop

   1 start: 83
   2 end: 244
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 schedule: '{ domain: "[n] -> { S2[x1, x2] : exists (e0 = floor((x2)/3): 3e0 = x2 and
   6   x1 >= 0 and x1 <= -1 + n and x2 <= 9); S1[x1] : x1 >= 0 and x1 <= -1 + n; S_1[x1,
   7   x2] : exists (e0 = floor((x2)/3): 3e0 = x2 and x1 >= 0 and x1 <= -1 + n and x2 <=
   8   9); R[x1] : x1 >= 0 and x1 <= -1 + n }", child: { schedule: "[n] -> L_0[{ S1[x1]
   9   -> [(x1)]; R[x1] -> [(x1)]; S_1[x1, x2] -> [(x1)]; S2[x1, x2] -> [(x1)] }]", child:
  10   { sequence: [ { filter: "[n] -> { S1[x1] }" }, { filter: "[n] -> { S2[x1, x2]; S_1[x1,
  11   x2] }", child: { schedule: "[n] -> L_1[{ S_1[x1, x2] -> [(-x2)]; S2[x1, x2] -> [(-x2)]
  12   }]", child: { sequence: [ { filter: "[n] -> { S_1[x1, x2] }" }, { filter: "[n] ->
  13   { S2[x1, x2] }" } ] } } }, { filter: "[n] -> { R[x1] }" } ] } } }'
  14 arrays:
  15 - context: '{  :  }'
  16   extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  17     x1 <= -1 + n and x2 <= 9 and x1 >= 0) }'
  18   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  19   element_type: int
  20   element_size: 4
  21   uniquely_defined: 1
  22 - context: '{  :  }'
  23   extent: '[n] -> { s[] }'
  24   element_type: int
  25   element_size: 4
  26 statements:
  27 - line: 12
  28   domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }'
  29   body:
  30     type: expression
  31     expr:
  32       type: op
  33       operation: =
  34       arguments:
  35       - type: access
  36         index: '[n] -> { S1[x1] -> s[] }'
  37         reference: __pet_ref_0
  38         read: 0
  39         write: 1
  40       - type: call
  41         name: f
  42 - line: 13
  43   domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  44     x1 <= -1 + n and x2 <= 9 and x1 >= 0) }'
  45   body:
  46     type: expression
  47     expr:
  48       type: op
  49       operation: =
  50       arguments:
  51       - type: access
  52         index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), (x2)] }'
  53         reference: __pet_ref_2
  54         read: 0
  55         write: 1
  56       - type: call
  57         name: P
  58         arguments:
  59         - type: access
  60           index: '[n] -> { S_1[x1, x2] -> [(x1)] }'
  61           reference: __pet_ref_3
  62           read: 1
  63           write: 0
  64         - type: access
  65           index: '[n] -> { S_1[x1, x2] -> [(x2 - 256*floor((x2)/256))] }'
  66           reference: __pet_ref_4
  67           read: 1
  68           write: 0
  69   arguments:
  70   - type: access
  71     index: '[n] -> { S_1[x1, x2] -> __pet_test_0[(x1), ((3 + x2) : x2 <= 6)] }'
  72     reference: __pet_ref_1
  73     read: 1
  74     write: 0
  75 - line: 14
  76   domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = floor((x2)/3): 3e0 = x2 and
  77     x1 <= -1 + n and x2 <= 9 and x1 >= 0) }'
  78   body:
  79     type: expression
  80     expr:
  81       type: op
  82       operation: =
  83       arguments:
  84       - type: access
  85         index: '[n] -> { S2[x1, x2] -> s[] }'
  86         reference: __pet_ref_6
  87         read: 0
  88         write: 1
  89       - type: call
  90         name: g
  91         arguments:
  92         - type: access
  93           index: '[n] -> { S2[x1, x2] -> s[] }'
  94           reference: __pet_ref_7
  95           read: 1
  96           write: 0
  97   arguments:
  98   - type: access
  99     index: '[n] -> { S2[x1, x2] -> __pet_test_0[(x1), (x2)] }'
 100     reference: __pet_ref_5
 101     read: 1
 102     write: 0
 103 - line: 16
 104   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
 105   body:
 106     type: expression
 107     expr:
 108       type: call
 109       name: h
 110       arguments:
 111       - type: access
 112         index: '[n] -> { R[x1] -> s[] }'
 113         reference: __pet_ref_8
 114         read: 1
 115         write: 0
 116 implications:
 117 - satisfied: 1
 118   extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
 119     = floor((x2'')/3): 3e0 = x2'' and x2'' >= x2 and x1 >= 0 and x1 <= -1 + n and
 120     x2'' <= 9) }'