tests/for_while_inc4.scop

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