tests/while.scop

   1 start: 83
   2 end: 210
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 schedule: '{ domain: "[n] -> { S2[x, t] : x >= 0 and x <= -1 + n and t >= 0; S1[x]
   6   : x >= 0 and x <= -1 + n; S_1[x, t] : x >= 0 and x <= -1 + n and t >= 0; R[x] :
   7   x >= 0 and x <= -1 + n }", child: { schedule: "[n] -> L_0[{ S1[x] -> [(x)]; R[x]
   8   -> [(x)]; S_1[x, t] -> [(x)]; S2[x, t] -> [(x)] }]", child: { sequence: [ { filter:
   9   "[n] -> { S1[x] }" }, { filter: "[n] -> { S2[x, t]; S_1[x, t] }", child: { schedule:
  10   "[n] -> L_1[{ S_1[x, t] -> [(t)]; S2[x, t] -> [(t)] }]", child: { sequence: [ {
  11   filter: "[n] -> { S_1[x, t] }" }, { filter: "[n] -> { S2[x, t] }" } ] } } }, { filter:
  12   "[n] -> { R[x] }" } ] } } }'
  13 arrays:
  14 - context: '{  :  }'
  15   extent: '[n] -> { __pet_test_0[x, t] : x <= -1 + n and t >= 0 and x >= 0 }'
  16   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  17   element_type: int
  18   element_size: 4
  19   uniquely_defined: 1
  20 - context: '{  :  }'
  21   extent: '[n] -> { s[] }'
  22   element_type: int
  23   element_size: 4
  24 statements:
  25 - line: 12
  26   domain: '[n] -> { S1[x] : x >= 0 and x <= -1 + n }'
  27   schedule: '[n] -> { S1[x] -> [0, x, 0] }'
  28   body:
  29     type: expression
  30     expr:
  31       type: op
  32       operation: =
  33       arguments:
  34       - type: access
  35         index: '[n] -> { S1[x] -> s[] }'
  36         reference: __pet_ref_0
  37         read: 0
  38         write: 1
  39       - type: call
  40         name: f
  41 - line: 13
  42   domain: '[n] -> { [S_1[x, t] -> [1]] : x <= -1 + n and t >= 0 and x >= 0 }'
  43   schedule: '[n] -> { S_1[x, t] -> [0, x, 1, t, 0] }'
  44   body:
  45     type: expression
  46     expr:
  47       type: op
  48       operation: =
  49       arguments:
  50       - type: access
  51         index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), (t)] }'
  52         reference: __pet_ref_2
  53         read: 0
  54         write: 1
  55       - type: call
  56         name: P
  57         arguments:
  58         - type: access
  59           index: '[n] -> { S_1[x, t] -> [(x)] }'
  60           reference: __pet_ref_3
  61           read: 1
  62           write: 0
  63         - type: access
  64           index: '[n] -> { S_1[x, t] -> s[] }'
  65           reference: __pet_ref_4
  66           read: 1
  67           write: 0
  68   arguments:
  69   - type: access
  70     index: '[n] -> { S_1[x, t] -> __pet_test_0[(x), ((-1 + t) : t >= 1)] }'
  71     reference: __pet_ref_1
  72     read: 1
  73     write: 0
  74 - line: 14
  75   domain: '[n] -> { [S2[x, t] -> [1]] : x <= -1 + n and t >= 0 and x >= 0 }'
  76   schedule: '[n] -> { S2[x, t] -> [0, x, 1, t, 1, 0] }'
  77   body:
  78     type: expression
  79     expr:
  80       type: op
  81       operation: =
  82       arguments:
  83       - type: access
  84         index: '[n] -> { S2[x, t] -> s[] }'
  85         reference: __pet_ref_6
  86         read: 0
  87         write: 1
  88       - type: call
  89         name: g
  90         arguments:
  91         - type: access
  92           index: '[n] -> { S2[x, t] -> s[] }'
  93           reference: __pet_ref_7
  94           read: 1
  95           write: 0
  96   arguments:
  97   - type: access
  98     index: '[n] -> { S2[x, t] -> __pet_test_0[(x), (t)] }'
  99     reference: __pet_ref_5
 100     read: 1
 101     write: 0
 102 - line: 16
 103   domain: '[n] -> { R[x] : x >= 0 and x <= -1 + n }'
 104   schedule: '[n] -> { R[x] -> [0, x, 2] }'
 105   body:
 106     type: expression
 107     expr:
 108       type: call
 109       name: h
 110       arguments:
 111       - type: access
 112         index: '[n] -> { R[x] -> s[] }'
 113         reference: __pet_ref_8
 114         read: 1
 115         write: 0
 116 implications:
 117 - satisfied: 1
 118   extension: '[n] -> { __pet_test_0[x, t] -> __pet_test_0[x, t''] : t'' <= t and x
 119     >= 0 and x <= -1 + n and t'' >= 0 }'