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