tests/inc5.scop

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