tests/for_while_init3.scop

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