tests/inc5.scop

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