tests/for_while_inc2.scop

   1 start: 83
   2 end: 234
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 schedule: '{ domain: "[n] -> { S_6[x1] : x1 >= 0 and x1 <= -1 + n; S_2[x1, t] : x1
   6   >= 0 and x1 <= -1 + n and t >= 0; S2[x1, t] : x1 >= 0 and x1 <= -1 + n and t >=
   7   0; S1[x1] : x1 >= 0 and x1 <= -1 + n; S_5[x1] : x1 >= 0 and x1 <= -1 + n; S_1[x1]
   8   : x1 >= 0 and x1 <= -1 + n; R[x1] : x1 >= 0 and x1 <= -1 + n; S_4[x1, t] : x1 >=
   9   0 and x1 <= -1 + n and t >= 0 }", child: { schedule: "[n] -> L_0[{ S1[x1] -> [(x1)];
  10   S_4[x1, t] -> [(x1)]; R[x1] -> [(x1)]; S_6[x1] -> [(x1)]; S_5[x1] -> [(x1)]; S2[x1,
  11   t] -> [(x1)]; S_2[x1, t] -> [(x1)]; S_1[x1] -> [(x1)] }]", child: { sequence: [
  12   { filter: "[n] -> { S1[x1] }" }, { filter: "[n] -> { S_5[x1] }" }, { filter: "[n]
  13   -> { S_1[x1] }" }, { filter: "[n] -> { S_2[x1, t]; S2[x1, t]; S_4[x1, t] }", child:
  14   { schedule: "[n] -> L_1[{ S_4[x1, t] -> [(t)]; S2[x1, t] -> [(t)]; S_2[x1, t] ->
  15   [(t)] }]", child: { sequence: [ { filter: "[n] -> { S_2[x1, t] }" }, { filter: "[n]
  16   -> { S2[x1, t] }" }, { filter: "[n] -> { S_4[x1, t] }" } ] } } }, { filter: "[n]
  17   -> { S_6[x1] }" }, { filter: "[n] -> { R[x1] }" } ] } } }'
  18 arrays:
  19 - context: '{  :  }'
  20   extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and t >= 0 and x1 >= 0 }'
  21   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  22   element_type: int
  23   element_size: 4
  24   uniquely_defined: 1
  25 - context: '{  :  }'
  26   extent: '[n] -> { x2[] }'
  27   element_type: int
  28   element_size: 4
  29   declared: 1
  30 - context: '{  :  }'
  31   extent: '[n] -> { s[] }'
  32   element_type: int
  33   element_size: 4
  34 statements:
  35 - line: 12
  36   domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }'
  37   schedule: '[n] -> { S1[x1] -> [0, x1, 0] }'
  38   body:
  39     type: expression
  40     expr:
  41       type: op
  42       operation: =
  43       arguments:
  44       - type: access
  45         index: '[n] -> { S1[x1] -> s[] }'
  46         reference: __pet_ref_0
  47         read: 0
  48         write: 1
  49       - type: call
  50         name: f
  51 - line: 13
  52   domain: '[n] -> { S_5[x1] : x1 >= 0 and x1 <= -1 + n }'
  53   schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }'
  54   body:
  55     type: expression
  56     expr:
  57       type: op
  58       operation: kill
  59       arguments:
  60       - type: access
  61         killed: '[n] -> { S_5[x1] -> x2[] }'
  62         index: '[n] -> { S_5[x1] -> x2[] }'
  63         reference: __pet_ref_1
  64         kill: 1
  65 - line: 13
  66   domain: '[n] -> { S_1[x1] : x1 >= 0 and x1 <= -1 + n }'
  67   schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }'
  68   body:
  69     type: expression
  70     expr:
  71       type: op
  72       operation: =
  73       arguments:
  74       - type: access
  75         index: '[n] -> { S_1[x1] -> x2[] }'
  76         reference: __pet_ref_2
  77         read: 0
  78         write: 1
  79       - type: int
  80         value: 0
  81 - line: 13
  82   domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and t >= 0 and x1 >= 0 }'
  83   schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }'
  84   body:
  85     type: expression
  86     expr:
  87       type: op
  88       operation: =
  89       arguments:
  90       - type: access
  91         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  92         reference: __pet_ref_4
  93         read: 0
  94         write: 1
  95       - type: call
  96         name: P
  97         arguments:
  98         - type: access
  99           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
 100           reference: __pet_ref_5
 101           read: 1
 102           write: 0
 103         - type: access
 104           index: '[n] -> { S_2[x1, t] -> x2[] }'
 105           reference: __pet_ref_6
 106           read: 1
 107           write: 0
 108   arguments:
 109   - type: access
 110     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
 111     reference: __pet_ref_3
 112     read: 1
 113     write: 0
 114 - line: 14
 115   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and t >= 0 and x1 >= 0 }'
 116   schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }'
 117   body:
 118     type: expression
 119     expr:
 120       type: op
 121       operation: =
 122       arguments:
 123       - type: access
 124         index: '[n] -> { S2[x1, t] -> s[] }'
 125         reference: __pet_ref_8
 126         read: 0
 127         write: 1
 128       - type: call
 129         name: g
 130         arguments:
 131         - type: access
 132           index: '[n] -> { S2[x1, t] -> s[] }'
 133           reference: __pet_ref_9
 134           read: 1
 135           write: 0
 136   arguments:
 137   - type: access
 138     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 139     reference: __pet_ref_7
 140     read: 1
 141     write: 0
 142 - line: 13
 143   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and t >= 0 and x1 >= 0 }'
 144   schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }'
 145   body:
 146     type: expression
 147     expr:
 148       type: op
 149       operation: +=
 150       arguments:
 151       - type: access
 152         index: '[n] -> { S_4[x1, t] -> x2[] }'
 153         reference: __pet_ref_11
 154         read: 0
 155         write: 1
 156       - type: access
 157         index: '[n] -> { S_4[x1, t] -> s[] }'
 158         reference: __pet_ref_12
 159         read: 1
 160         write: 0
 161   arguments:
 162   - type: access
 163     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 164     reference: __pet_ref_10
 165     read: 1
 166     write: 0
 167 - line: 13
 168   domain: '[n] -> { S_6[x1] : x1 >= 0 and x1 <= -1 + n }'
 169   schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }'
 170   body:
 171     type: expression
 172     expr:
 173       type: op
 174       operation: kill
 175       arguments:
 176       - type: access
 177         killed: '[n] -> { S_6[x1] -> x2[] }'
 178         index: '[n] -> { S_6[x1] -> x2[] }'
 179         reference: __pet_ref_13
 180         kill: 1
 181 - line: 16
 182   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
 183   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 184   body:
 185     type: expression
 186     expr:
 187       type: call
 188       name: h
 189       arguments:
 190       - type: access
 191         index: '[n] -> { R[x1] -> s[] }'
 192         reference: __pet_ref_14
 193         read: 1
 194         write: 0
 195 implications:
 196 - satisfied: 1
 197   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
 198     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'