tests/for_while_init.scop

   1 start: 83
   2 end: 231
   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: int
 155         value: 1
 156   arguments:
 157   - type: access
 158     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 159     reference: __pet_ref_11
 160     read: 1
 161     write: 0
 162 - line: 13
 163   domain: '[n] -> { S_6[x1] : 0 <= x1 < n }'
 164   body:
 165     type: expression
 166     expr:
 167       type: op
 168       operation: kill
 169       arguments:
 170       - type: access
 171         killed: '[n] -> { S_6[x1] -> x2[] }'
 172         index: '[n] -> { S_6[x1] -> x2[] }'
 173         reference: __pet_ref_13
 174         kill: 1
 175 - line: 16
 176   domain: '[n] -> { R[x1] : 0 <= x1 < n }'
 177   body:
 178     type: expression
 179     expr:
 180       type: call
 181       name: h
 182       arguments:
 183       - type: access
 184         index: '[n] -> { R[x1] -> s[] }'
 185         reference: __pet_ref_14
 186         read: 1
 187         write: 0
 188 - line: -1
 189   domain: '[n] -> { S_8[] }'
 190   body:
 191     type: expression
 192     expr:
 193       type: op
 194       operation: kill
 195       arguments:
 196       - type: access
 197         killed: '[n] -> { S_8[] -> s[] }'
 198         index: '[n] -> { S_8[] -> s[] }'
 199         reference: __pet_ref_15
 200         kill: 1
 201 implications:
 202 - satisfied: 1
 203   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1'' = x1, t''] : 0 <=
 204     x1 < n and 0 <= t'' <= t }'