tests/for_while_inc2.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: int
  78         value: 0
  79 - line: 13
  80   domain: '[n] -> { [S_2[x1, t] -> [__pet_test_0 = 1]] : 0 <= x1 < n and t >= 0 }'
  81   body:
  82     type: expression
  83     expr:
  84       type: op
  85       operation: =
  86       arguments:
  87       - type: access
  88         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  89         reference: __pet_ref_4
  90         read: 0
  91         write: 1
  92       - type: call
  93         name: P
  94         arguments:
  95         - type: access
  96           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
  97           reference: __pet_ref_5
  98           read: 1
  99           write: 0
 100         - type: access
 101           index: '[n] -> { S_2[x1, t] -> x2[] }'
 102           reference: __pet_ref_6
 103           read: 1
 104           write: 0
 105   arguments:
 106   - type: access
 107     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t > 0)] }'
 108     reference: __pet_ref_3
 109     read: 1
 110     write: 0
 111 - line: 14
 112   domain: '[n] -> { [S2[x1, t] -> [__pet_test_0 = 1]] : 0 <= x1 < n and t >= 0 }'
 113   body:
 114     type: expression
 115     expr:
 116       type: op
 117       operation: =
 118       arguments:
 119       - type: access
 120         index: '[n] -> { S2[x1, t] -> s[] }'
 121         reference: __pet_ref_8
 122         read: 0
 123         write: 1
 124       - type: call
 125         name: g
 126         arguments:
 127         - type: access
 128           index: '[n] -> { S2[x1, t] -> s[] }'
 129           reference: __pet_ref_9
 130           read: 1
 131           write: 0
 132   arguments:
 133   - type: access
 134     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 135     reference: __pet_ref_7
 136     read: 1
 137     write: 0
 138 - line: 13
 139   domain: '[n] -> { [S_4[x1, t] -> [__pet_test_0 = 1]] : 0 <= x1 < n and t >= 0 }'
 140   body:
 141     type: expression
 142     expr:
 143       type: op
 144       operation: +=
 145       arguments:
 146       - type: access
 147         index: '[n] -> { S_4[x1, t] -> x2[] }'
 148         reference: __pet_ref_11
 149         read: 0
 150         write: 1
 151       - type: access
 152         index: '[n] -> { S_4[x1, t] -> s[] }'
 153         reference: __pet_ref_12
 154         read: 1
 155         write: 0
 156   arguments:
 157   - type: access
 158     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 159     reference: __pet_ref_10
 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 }'