tests/for_while_init3.scop

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