tests/for_while_init2.scop

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