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