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         index: '[n] -> { S_0[] -> s[] }'
  37         reference: __pet_ref_0
  38         read: 0
  39         write: 1
  40       - type: int
  41         value: 0
  42 - line: 8
  43   domain: '[n] -> { S_5[i] : i <= -1 + n and i >= 0 }'
  44   schedule: '[n] -> { S_5[i] -> [1, i, 0] }'
  45   body:
  46     type: expression
  47     expr:
  48       type: op
  49       operation: kill
  50       arguments:
  51       - type: access
  52         relation: '[n] -> { S_5[i] -> j[] }'
  53         index: '[n] -> { S_5[i] -> j[] }'
  54         reference: __pet_ref_1
  55         kill: 1
  56 - line: 8
  57   domain: '[n] -> { S_1[i] : i <= -1 + n and i >= 0 }'
  58   schedule: '[n] -> { S_1[i] -> [1, i, 1] }'
  59   body:
  60     type: expression
  61     expr:
  62       type: op
  63       operation: =
  64       arguments:
  65       - type: access
  66         index: '[n] -> { S_1[i] -> j[] }'
  67         reference: __pet_ref_2
  68         read: 0
  69         write: 1
  70       - type: access
  71         index: '[n] -> { S_1[i] -> A[(i)] }'
  72         reference: __pet_ref_3
  73         read: 1
  74         write: 0
  75 - line: 8
  76   domain: '[n] -> { [S_2[i, t] -> [1]] : i <= -1 + n and i >= 0 and t >= 0 }'
  77   schedule: '[n] -> { S_2[i, t] -> [1, i, 2, t, 0] }'
  78   body:
  79     type: expression
  80     expr:
  81       type: op
  82       operation: =
  83       arguments:
  84       - type: access
  85         index: '[n] -> { S_2[i, t] -> __pet_test_0[(i), (t)] }'
  86         reference: __pet_ref_5
  87         read: 0
  88         write: 1
  89       - type: op
  90         operation: <
  91         arguments:
  92         - type: access
  93           index: '[n] -> { S_2[i, t] -> j[] }'
  94           reference: __pet_ref_6
  95           read: 1
  96           write: 0
  97         - type: int
  98           value: 10
  99   arguments:
 100   - type: access
 101     index: '[n] -> { S_2[i, t] -> __pet_test_0[(i), ((-1 + t) : t >= 1)] }'
 102     reference: __pet_ref_4
 103     read: 1
 104     write: 0
 105 - line: 9
 106   domain: '[n] -> { [S_3[i, t] -> [1]] : i <= -1 + n and i >= 0 and t >= 0 }'
 107   schedule: '[n] -> { S_3[i, t] -> [1, i, 2, t, 1] }'
 108   body:
 109     type: expression
 110     expr:
 111       type: op
 112       operation: ++
 113       arguments:
 114       - type: access
 115         index: '[n] -> { S_3[i, t] -> s[] }'
 116         reference: __pet_ref_8
 117         read: 1
 118         write: 1
 119   arguments:
 120   - type: access
 121     index: '[n] -> { S_3[i, t] -> __pet_test_0[(i), (t)] }'
 122     reference: __pet_ref_7
 123     read: 1
 124     write: 0
 125 - line: 8
 126   domain: '[n] -> { [S_4[i, t] -> [1]] : i <= -1 + n and i >= 0 and t >= 0 }'
 127   schedule: '[n] -> { S_4[i, t] -> [1, i, 2, t, 2] }'
 128   body:
 129     type: expression
 130     expr:
 131       type: op
 132       operation: +=
 133       arguments:
 134       - type: access
 135         index: '[n] -> { S_4[i, t] -> j[] }'
 136         reference: __pet_ref_10
 137         read: 0
 138         write: 1
 139       - type: int
 140         value: 1
 141   arguments:
 142   - type: access
 143     index: '[n] -> { S_4[i, t] -> __pet_test_0[(i), (t)] }'
 144     reference: __pet_ref_9
 145     read: 1
 146     write: 0
 147 - line: 8
 148   domain: '[n] -> { S_6[i] : i <= -1 + n and i >= 0 }'
 149   schedule: '[n] -> { S_6[i] -> [1, i, 3] }'
 150   body:
 151     type: expression
 152     expr:
 153       type: op
 154       operation: kill
 155       arguments:
 156       - type: access
 157         relation: '[n] -> { S_6[i] -> j[] }'
 158         index: '[n] -> { S_6[i] -> j[] }'
 159         reference: __pet_ref_11
 160         kill: 1
 161 implications:
 162 - satisfied: 1
 163   extension: '[n] -> { __pet_test_0[i, t] -> __pet_test_0[i, t''] : t'' <= t and i
 164     >= 0 and i <= -1 + n and t'' >= 0 }'