tests/for_while_init3.scop

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